[Cryptography] Formal Verification

Perry E. Metzger perry at piermont.com
Fri Mar 18 12:04:27 EDT 2016


On Fri, 18 Mar 2016 08:37:15 -0700 Henry Baker <hbaker1 at pipeline.com>
wrote:
> At 10:07 PM 3/16/2016, Christian Huitema wrote:
> >Adding ASSERT statements liberally expresses a lot about code
> >intent, and will catch potential issues during a debug break.
> >
> >Of course, true formal development if applicable will be somewhat
> >better than C + SAL + ASSERT.
> >
> >ASSERT are too costly to be compiled in the production code.
> >
> >They are only activated in special debug builds, and thus can only
> >detect issues encountered during debug runs.
> 
> IMHO, this is completely backwards.
>
> ASSERT's should always be sprinkled *extremely liberally* all over
> your code.
>
> The job of a theorem prover is merely to remove ASSERT's that it
> can prove are *always satisfied.*  I.e., a "theorem prover" is just
> a really good compiler optimizer for dead code elimination.

That is one way to look at things, but I'd say that it
isn't necessarily the way that leads to the most immediate
understanding of the methods that are currently under most intense
development.

The state of the art on formal verification is dependently typed
lambda calculi (like pCIC which is the basis of Coq) coupled with
various sorts of tactic engines to help a human verifier out. We're
also now getting all sorts of interesting new technologies on the side
of this -- constraint solvers like Z3 may prove crucial in making
these technologies more useful.

> (*) This brings up the need for easy ways to add ad hoc, but
> provably correct, compiler "peephole" (?) optimizations, since no
> compiler will ever be able to prove -- thanks to Goedel & Turing --
> without the programmer's help -- all the lemmas and theorems it
> will need for every program.  I need to be able to enter into a
> dialog with my compiler, suggesting that such-and-such should be
> replace by such&other under certain conditions.

Coq is very good at a version of this sort of thing, since the tactic
language is (in a real sense) a dialog conducted with the system to
help construct proof terms. I'm not aware of a system that
specifically allows you to add compiler optimizations by providing
proofs to the system but that would be a straightforward (though not
low labor) thing to do in some of the new systems out there.

> The compiler will
> ask me to prove that my optimization is correct, which may involve
> inserting additional ASSERT statements into the compiler
> optimization.
>
> This type of compiler extension is *easy* (or at least easiER) in
> introspective languages like Lisp.

Lisp is, of course, pretty close to the untyped lambda calculus. The
advantage of typed lambda calculi for this sort of thing is that one
can take advantage of the Curry-Howard isomorphism and have a single
language in which both proofs and programs are written. Indeed, Coq,
Agda, F*, Lean (which is brand new) and other systems that are under
active development all seem to follow this pattern of unifying a
constructive logic and a programming language through the use of
dependent types and Curry-Howard.

Perry
-- 
Perry E. Metzger		perry at piermont.com


More information about the cryptography mailing list