Hacker News new | ask | show | jobs
by hi-v-rocknroll 670 days ago
My wish is that FOSS software test engineering approaches and tools evolve to appropriately model and formally-verify code behavior in the spirit of what the seL4 project did and maybe further. Similarly, system behavior should also be formally-specified and provable. Until we get there, it's one removed from whipping up untested code ad-hoc and then YOLO'ing to hope it all works out. It's going to take a lot more work and a new way of defining constraints, relationships, and nonvariants but it's unavoidable to prove that code behaves as intended.

PS: Neither "Just rewrite everything in X where X = Rust", "just use fuzzing", or "just use MISRA coding standards" doesn't get us there. Holistic improvements help, but not with the fundamental deficiency above.
2 comments
MaxBarraclough 670 days ago
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/

link
hi-v-rocknroll 669 days ago
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.
link
MaxBarraclough 669 days ago
> 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%...

link
weinzierl 670 days ago
The important word is "just", when X facilitates formal verification by a considerable margin.
link