Hacker News Reader

Comment by andrewchambers | Hacker News Reader

> basically, you trade a huge codebase for a smaller one in the form of the spec

Most formally verified things i have seen require huge amounts of 'spec' code compared to the implementation.

The specs are often more abstract than the implementation. Rarely larger. When they're at that size or larger, it's usually one of two things: deficient spec tool that takes way too much syntax to express problem; more often the spec makes explicit contextual information that usually is just in developer's head. You want that stuff explicit when analyzing security or correctness, esp corner cases or integration errors.

You're confusing the specification with the equivalence proof. A spec is likely going to be about as simple as an implementation, with the benefit that it can be read more consistently.

All the specs for real world things I've seen are long and use fuzzy language. Making them formal enough to provide a basis for verification will only make them longer.

I wouldn't be so pessimistic about the possibility to produce useful specifications of real-world systems.

One recent successful large-scale verification is the CompCert C compiler. The compiler is verified relative to a formal specification of a large subset of C. This specification is in the order of <2000 lines of Coq code (see http://gallium.inria.fr/~xleroy/publi/Clight.pdf ). So it is an example of a specification that is much smaller than an implementation and that can be verified manually.

Also, there is good evidence that the specification is correct. From https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf :

> The striking thing about our CompCert results is that the middle- end bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task.

Here's a recent survey of some work:

https://courses.cs.washington.edu/courses/cse551/15sp/projec...

Let's look at numbers of some to see what happens:

1. Jitk. In-kernel interpreter for firewall rules. 2300 lines spec, 3510 lines code.

2. ExpressOS. Uses C# and verifiable Dafny language with annotations that feed into prover. The annotations were 2.8% of code.

3. seL4. This is kind of project that makes it seem like specs and proofs are huge. That's cuz people forget what they're specifying: an abstract CPU + imperative programming + kernel + safety/security properties + equivalence. Writing that in code also takes a lot of lines but they didn't have to in C past kernel. Anyway, this one is (a) for executable spec 5,700loc Haskell + 13,000loc Isabelle and (b) for implementation 8,700loc of C/ASM + 15,000loc Isabelle. They went full proof instead of code review. That added 200,000Kloc of proof steps with a good chunk automated.

4. VCC on Microsoft Hyper-V. Similar problem to 3 where this manages a CPU/machine. Total size was around 100,000loc last I checked. Verifying 20%... 20,000loc... took 13,500loc annotations. Verification automated.

5. Verdi protocol verifier. Spec/code reported is: Key-value store 41/138; Primary-backup 20/134; Raft algorithm 170/520; Verdi itself 148/220. Always smaller in its specs.

So, it's clear that the specs range from being tiny to smaller than code in most cases with heaviest, hardest efforts taking more specs. Proofs range from automated to manual.

Reply on news.ycombinator.com