Comment by lazaroclapp | Hacker News Reader

Comment by lazaroclapp | Hacker News Reader

Quick reminder that verified code is only hacker-proof provided that:

a) The specification correctly describes all correct behavior and correctly proscribes all incorrect behavior (basically, you trade a huge codebase for a smaller one in the form of the spec, which is a massive improvement, but as long as humans write the spec it is not clear it can ever be fully hacker-proof)

b) The trusted computing base works as modeled in the spec. Even on the limit, that means that the physical properties of the hardware are as we expect them to be and that our understanding of the laws of physics is correct. Slightly below this threshold there are things like Row Hammer attacks (https://en.wikipedia.org/wiki/Row_hammer ). Before even this: microcode bugs, proof-verifier bugs, etc.

That said, formal methods do provide a huge improvement over the state of the art of completely unspecified software, and have been shown to work in practice to greatly reduce the number of vulnerabilities of important large systems such as compilers, kernels and now remote controlled helicopters. They might not be appropriate for every piece of software quite yet, but I would greatly like to see this stuff for things like self-driving cars, airplane autopilots, smart grids and smart factories and in general all of the rapidly approaching "heavy" IoT applications. Also, some verified properties of commodity OS would be very nice to have (say container isolation in a cloud environment or non-leaking of keys for a smart wallet process).

> 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.

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.

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.

Reply on news.ycombinator.com