Hacker News Reader

Comment by AstralStorm | Hacker News Reader

Main lesson not learned: instead of testing, prove correctness in high assurance code like this. Rigorously and formally. Preferably even refine the proof to executable code.

(Yes, it would take somewhere on the order of 10k LOC to prove correctness of this 1k.)

View on HN

In this case 3 of the bugs would be caught when trying to prove the absense of undefined behaviour/use of uninitialized value. Can existing formal proof tools be used for that?

Proving correctness isn't enough. You have to test it too. It's perfectly possible for the proof to have errors (bugs). It's also possible for the proof to be incomplete: you can prove the algorithm is correct and implemented correctly to spec and still have vulnerabilities.

While 100% confidence is impossible (because I'm Bayesian), machine checked proofs do help. It's then a matter of cost/benefit.

"Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth

I'm sure you encounter "high assurance code" like this every day -- your operating system, the secure protocol used to post your comment, the controls for your Anti-Lock Breaking System in your car.

How much of those were formally proven?

TLS has been subject to lots of formal verification. The other things, probably not so much.

Verifying some (but not all) properties of crypto is relatively (but not absolutely) easy, because it's essentially just math with pure functions. Operating systems and physical controllers with real-time constraints have different requirements and more interacting state, which means that the desired properties are not easily expressed as a mathematical expression.

https://github.com/mitls/hacl-star

Reply on news.ycombinator.com