<story><title>Formal Verification: The Gap Between Perfect Code and Reality</title><url>https://raywang.tech/2017/12/20/Formal-Verification:-The-Gap-between-Perfect-Code-and-Reality/</url></story><parent_chain></parent_chain><comment><author>Animats</author><text>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&amp;#x27;s some of the Coq world.&lt;p&gt;It doesn&amp;#x27;t have to be this way. Microsoft&amp;#x27;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.&lt;p&gt;Most of the things you want to prove about programs to make sure they don&amp;#x27;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 is 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&amp;#x27;s fully automatic and complete - the algorithm always succeeds within its problem space. You need one of those for the easy parts.&lt;p&gt;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.)&lt;p&gt;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 &amp;quot;pop two operands from stack, add in 16-bit twos complement arithmetic, push on stack&amp;quot;. This captured the semantics of the program the same way the compiler did.&lt;p&gt;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&amp;#x27;t see it.  Only the errors are visible.  Another trick is that you don&amp;#x27;t write &amp;quot;assert(a and b and and d)&amp;quot;, you write &amp;quot;assert(a); assert(b);&amp;quot;. Those generate separate proof goals, and if only one fails,the user gets error messages about only that one.  Also, when you write &amp;quot;assert(a); assert(b);&amp;quot;, the second one is proved under the assumption the first one is true.  This prevents cascading errors.&lt;p&gt;A key point here is that verification is meaningless unless you prove &lt;i&gt;all&lt;/i&gt; the theorems. If you write &amp;quot;assert(false)&amp;quot; other errors go away, and you&amp;#x27;re left with one simple error, which you cannot eliminate.
You don&amp;#x27;t get to dismiss it. It&amp;#x27;s possible to write an assertion that&amp;#x27;s equivalent to &amp;quot;assert(false);&amp;quot;, such as &amp;quot;assert(0 &amp;gt; 1)&amp;quot;; This is why I&amp;#x27;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.&lt;p&gt;When you needed to prove something hard, you wrote&lt;p&gt;&lt;pre&gt;&lt;code&gt;    assert(a);
    assert(b);
&lt;/code&gt;&lt;/pre&gt;
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&amp;#x27;t prove &amp;quot;a implies b&amp;quot;. 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&amp;#x27;t require more work with the Boyer-Moore system.&lt;p&gt;If you&amp;#x27;re generating vast amounts of user-visible proof work, something is wrong.&lt;p&gt;The whole system I&amp;#x27;m describing is now on Github.[4] It&amp;#x27;s decades-old code, but I&amp;#x27;ve ported about 80% of it to modern compilers. The Franz LISP to Common LISP port of the prover isn&amp;#x27;t working well, and the author of that code died years ago. If anyone wants to work on that, go ahead.&lt;p&gt;[1] &lt;a href=&quot;http:&amp;#x2F;&amp;#x2F;www.animats.com&amp;#x2F;papers&amp;#x2F;verifier&amp;#x2F;verifiermanual.pdf&quot; rel=&quot;nofollow&quot;&gt;http:&amp;#x2F;&amp;#x2F;www.animats.com&amp;#x2F;papers&amp;#x2F;verifier&amp;#x2F;verifiermanual.pdf&lt;/a&gt;
[2] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;docs.microsoft.com&amp;#x2F;en-us&amp;#x2F;windows-hardware&amp;#x2F;drivers&amp;#x2F;devtest&amp;#x2F;static-driver-verifier&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;docs.microsoft.com&amp;#x2F;en-us&amp;#x2F;windows-hardware&amp;#x2F;drivers&amp;#x2F;de...&lt;/a&gt;
[3] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;John-Nagle&amp;#x2F;nqthm&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;John-Nagle&amp;#x2F;nqthm&lt;/a&gt;
[4] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;John-Nagle&amp;#x2F;pasv&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;John-Nagle&amp;#x2F;pasv&lt;/a&gt;</text></comment>
<story><title>Formal Verification: The Gap Between Perfect Code and Reality</title><url>https://raywang.tech/2017/12/20/Formal-Verification:-The-Gap-between-Perfect-Code-and-Reality/</url></story><parent_chain></parent_chain><comment><author>gchadwick</author><text>All of my formal verification experience comes from using it in hardware, so the following comment may not apply so well to software where I have no experience of formal methods (beyond learning about it at university).&lt;p&gt;I think the mistake the author is making here is seeing formal verification as an all or nothing affair.  Either you formally prove your program to be correct or it&amp;#x27;s useless.  I would agree with them that doing this is a huge amount of effort and potentially just not feasible for real systems.&lt;p&gt;However there&amp;#x27;s a huge amount of value in formal verification as an extra tool to assist you in your verification efforts.  By combining traditional verification techniques (normal testing in software terms) with formal methods you have a whole new way to find bugs, one which works rather differently and hence tends to find different bugs.  You may not get anywhere near confidence you&amp;#x27;ve formally proved everything (for one I find the more interesting properties just never get proven, but leaving the tool to run for a while often throws up bugs that are tricky to find via other means) but it does accelerate your verification efforts.&lt;p&gt;It&amp;#x27;s also a useful tool for exploring certain scenarios you as the designer (or programmer) may be worried about.  You can overconstrain it to just look at certain behaviour and you can ask it to show you some specific execution that hits a particular property.  Maybe there&amp;#x27;s some code path that&amp;#x27;s very hard to stimulate for whatever reason and you want to check out it&amp;#x27;s functionality.  You can get the formal tool to hit it and then see what it does.</text></comment>