[Cryptography] Formal Verification

[Perry E. Metzger]

On Wed, 16 Mar 2016 22:07:33 -0700 "Christian Huitema"
<huitema at huitema.net> wrote:
> On Wednesday, March 16, 2016 7:01 PM, Perry wrote:
> > ...
> > Most, no, but I've become a convert to formal methods in the last
> > few years. Until quite recently it was impossible to do real
> > formal verification work on programs of significant size, but
> > that has completely changed.  
> 
> I am not sure that formal method are such a break from the current
> state of the art.
> 
> Formal methods end up declaring what the code should do, using
> pre-conditions for the input variables and statements of invariants
> for the outcome. That's good, but at some level it is comparable to
> what can be done with the combination of static code analyzers and
> real time assertions.

Certainly there are points of comparison to what can be done with
static analysis, but overall the method is vastly more powerful. At
the cost of very substantial increases in development effort, it
provides you with certainty that the properties you have verified
actually hold for your code. Static analyzers generally only give you
best efforts (because they often cannot determine if particular
properties hold), and run time checks only go so far as well.

You can get really dramatic improvements this way. As just one
example: John Regehr's group at Utah has found hundreds of bugs in
almost every C compiler out there through the use of automated test
case generators and analyzers, but they've only found one in
the fully verified CompCert compiler, and that was arguably a case of
a broken Linux include file and not a bug in the compiler itself.

That said, verification can only find out if the properties you asked
about hold -- it cannot tell you what properties to check. That means
that you can fail to ask the right question. However, the advantage
is this: if you later figure out that you made a mistake and failed
to check an important property, once you add that to the things you
are verifying the hole is closed forever. Verification gives you a
ratchet, where problems, once found, can be *permanently* eliminated.

> Formal development and "annotated analysis" are different. But
> there are enough similarities. It is probably a continuum.

I will not disagree, and there are also many levels of verification.
Verification inevitably depends on assuming that some parts of the
system are working -- at the very least, you have to assume the
verifier is working since it cannot verify itself. You also, in
practice, are going to have to assume that the hardware was correctly
fabricated even if it was verified, and these days it is unlikely to
be fully verified itself, etc.

Still, the tool is *extremely* powerful, and I think even
revolutionary.

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