[MaxBarraclough]

That would be a great solution, but full formal verification is a very high bar.

The more realistic answer is to use safer languages than C for this sort of critical work. Rust and Ada spring to mind. They could even expose a C ABI/API. From a quick search, it looks like this has already been achieved for TLS, but it sees little real usage. [0] There are also Rust implementations of SSH (Russh and Thrussh), but I don't think they expose a C ABI/API.

I'm surprised this rather obvious solution doesn't seem to even receive serious consideration. I'd be surprised if performance was seriously impaired. This blog post [1] found Rustls to be faster than OpenSSL. I couldn't find a similar performance evaluation for Russh or Thrussh.

[0] https://github.com/rustls/rustls-ffi

[1] https://bencher.dev/learn/case-study/rustls/

[hi-v-rocknroll]

Well, the important things that run the world demand rigor. The "it's a hobby" defense rings hollow when decades of slip-shod processes have repeated led to a class of failures that repeated dozens and dozens of times.

[MaxBarraclough]

> The "it's a hobby" defense

That's not what I said, and it's not what we're talking about.

There's very little formally verified software out there, due to how challenging it is to use formal methods in large software solutions.

It makes little difference here whether the developer does it for a living. C codebases are prone to certain kinds of bugs that don't tend to arise when a safer language is used. We see a steady stream of these sorts of defects in FOSS C codebases and proprietary ones. Microsoft's closed-source TLS library has had similar issues, [0] as has Windows more broadly of course.

All that said, it would be great to see a serious and well-funded effort at a formally verified TLS implementation. Until then, we have the option of just using safer languages, but it's not getting much traction.

[0] https://signatures.juniper.net/documentation/signatures/SSL%...