ANAnimats·Dec 24, 2017
Having been down this road [1], a big problem is that the people doing this tend to be too much into the theory and not enough into wanting programs not to crash. That's some of the Coq world.
It doesn't have to be this way. Microsoft's work in this area led to the Static Driver Verifier [2], which was a huge success. Windows crashes due to kernel drivers breaking the rest of the kernel have pretty much disappeared. They were once (Windows XP and earlier) responsible for over half of Windows crashes.
Most of the things you want to prove about programs to make sure they don't crash are mathematically trivial. Detecting buffer overflows and off-by-one errors seldom requires elaborate proofs. If they do, your program design probably has a problem. Simple proofs can be handled by a prover which uses a Nelson-Oppen decision procedure. This i
Read the rest
s a complete decision procedure for formulas which contain only addition, subtraction, multiplication by constants, Boolean operators, structures, and arrays. This covers most data access operations. It's fully automatic and complete - the algorithm always succeeds within its problem space. You need one of those for the easy parts.
For the hard parts, we used the Boyer-Moore prover. (Sources are available and I brought it back to life on Github.[3] It runs 3000x faster than it did in 1982.)
The interface with the language is crucial to usability. Most efforts get this wrong. They put the verification stuff in separate files, or in comments. It should be part of the normal code. We built the verification language into the compiler, so you used the same source and the same syntax for compiling and verification. There were additional statements - ASSERT, ENTER, EXIT, etc. The same compiler front end was used for both compiling and verification. The verifier itself ran off the byte code from the compiler front end. All type and size issues had been decided at that point, so the verifier was looking at unambiguous operations such as "pop two operands from stack, add in 16-bit twos complement arithmetic, push on stack". This captured the semantics of the program the same way the compiler did.
The user never sees the easy stuff. Every subscript use generates a bounds check assertion which has to be proved. If the prover is able to prove the assertion true, the user doesn't see it. Only the errors are visible. Another trick is that you don't write "assert(a and b and and d)", you write "assert(a); assert(b);". Those generate separate proof goals, and if only one fails,the user gets error messages about only that one. Also, when you write "assert(a); assert(b);", the second one is proved under the assumption the first one is true. This prevents cascading errors.
A key point here is that verification is meaningless unless you prove all the theorems. If you write "assert(false)" other errors go away, and you're left with one simple error, which you cannot eliminate.
You don't get to dismiss it. It's possible to write an assertion that's equivalent to "assert(false);", such as "assert(0 > 1)"; This is why I'm so negative on the arguments from some of the Rust crowd that a little undefined behavior is OK. It can blow at any seam.
When you needed to prove something hard, you wrote
assert(a);
assert(b);
where a could be proved by the Nelson-Oppen prover from the code before it. B was chosen such that if you assumed b, the Nelson-Oppen prover could prove anything required past that point. Now you had one error message, that the system couldn't prove "a implies b". So then someone had to try to prove that with the Boyer-Moore prover. The Boyer-Moore prover is mostly automatic, but often someone had to provide intermediate theorems to get to a hard one. Those were all machine-checked. If this succeeded, the Boyer-Moore prover generated a theorem that a implies b for use by the verifier. Rerunning the program verifier would then succeed. Such theorems could be reused with different variable bindings, so if the same problem came up again, it didn't require more work with the Boyer-Moore system.
If you're generating vast amounts of user-visible proof work, something is wrong.
The whole system I'm describing is now on Github.[4] It's decades-old code, but I've ported about 80% of it to modern compilers. The Franz LISP to Common LISP port of the prover isn't working well, and the author of that code died years ago. If anyone wants to work on that, go ahead.
[1] http://www.animats.com/papers/verifier/verifiermanual.pdf
[2] https://docs.microsoft.com/en-us/windows-hardware/drivers/de...
[3] https://github.com/John-Nagle/nqthm
[4] https://github.com/John-Nagle/pasv