Hacker News Reader

Comment by galangalalgol | Hacker News Reader

I've worked on safety critical software, but we did not use formal methods. Lots of test and checking for coverage (at asm level). Oodles of static analysis and wading through false positives. Do formal methods usually supplement those or replace some of it? Can provers or formal methodologies scale to safety critical codebases of 100s of ksloc? Whether such codebases should exist, or be better partitioned is a separate issue.

View on HN

Formal methods seems to be perfect for verifying protocols, specially finding design flaws, here an example of an ongoing effort to verify TLS

https://www.mitls.org/

https://github.com/project-everest/mitls-fstar

The current crowning achievement of formal methods is, as I understand it, seL4. It is a formally proven microkernel of about 8500 LOC. There's still a while to go until they can scale to 100kLOCs, unfortunately.

CompCert is also very impressive. It's not, however, free software / open source (the source is available though)

https://www.absint.com/compcert/structure.htm

A problem with both seL4 and CompCert is that the code written to express the proofs is huge, much larger than code that actually does stuff. This puts a ceiling on the size of the projects we can verify.

F* is a language that tries to address that, by finding proofs with z3, a smt prover; z3 can't prove everything on its own but it cuts down proof code by orders of magnitude. They have written a verified cryptography stack and TLS stack, and want to write a whole verified http stack.

https://www.fstar-lang.org/

https://github.com/project-everest/hacl-star

https://www.mitls.org/

https://project-everest.github.io/

F* (through Low, a verified low-level subset of F) can extract verified code to C, which is kind of the inverse than the seL4 proof: seL4 begins with C code and enriches it with proofs of correctness; hacl* (a verified crypto F* lib) begins with a proven correct F* code and extracts C code (I gather the actual crypto primitives is compiled directly to asm code because C has some problems with constant time stuff). This enables hacl* to make bindings to other languages that can just call C code, like this Rust binding

https://github.com/franziskuskiefer/evercrypt-rust

Also this F* stuff is all free software / open source, so it might become a very prevalent crypto and TLS stack

I've never really worked on anything safety-critical, but I know that at least one real-time operating has been designed and verified with TLA+ [1]. The book is a bit pricey (and used copies don't pop up that often), so I haven't read it, but my understanding is that the developers felt that TLA+ did find bugs.

That said, TLA+ is written separately from the code. There could of course be bugs in the translation of TLA+ -> C...TLA+ is about checking the design itself, not the code.

[1] https://www.springer.com/gp/book/9781441997357

Not as a monolithic object. You might be able to do it with an almost microkernel approach (whatever you're implementing) with multiple small, well-defined objects with a well-defined protocol between them. That can be very useful. But I doubt you could formally verify their collective behaviour. The space and time complexity of the algorithms is explosive as the number of interacting objects increases.

Note that the specification (what you prove correctness of the implementation against) already grows with the number of interactions.

Yes, they are normally used in conjunction with testing. But they are also used in conjunction with careful systems engineering to minimise the amount of code that needs to go through the most rigerous processes and focus on what really mattered.

I'm curious which static analysis tool you were using. I used to work in SPARK Ada and false positives were not really a thing due to how it worked. But I've heard of others that were much less restrictive which ended up with lots of false positives, or "maybe" cases that then wasted everyone's time. I can see how systems like that would put people right off using them.

AWS have worked with Leslie Lamport of proving properties about S3.

See: Use of Formal Methods at Amazon Web Services

https://lamport.azurewebsites.net/tla/formal-methods-amazon....

Reply on news.ycombinator.com