[Cryptography] Security proofs prove non-failproof

[Perry E. Metzger]

On Thu, 16 Feb 2017 20:54:56 -0800 Bill Frantz
<frantz at pwpconsult.com> wrote:
> On 2/16/17 at 5:58 PM, perry at piermont.com (Perry E. Metzger) wrote:
> 
> >The big change in formal methods happened only in the last decade.
> >We now have several formally verified microkernels, a formally
> >verified C compiler that also doubles as a proof tool, we nearly
> >have a formally verified TLS stack (Project Everest), etc.,
> >etc. ...
> 
> It will be interesting to see what kind of bugs show up in these
> formally verified systems over years of use.

So we already have some sense on that, believe it or not.

John Regehr's research group at Utah built some C compiler torture
devices a while back -- automated systems capable of generating and
testing huge numbers of code snippets that are specifically designed
to find bugs in C compilers.

Regehr's group found hundreds and hundreds of bugs in each of gcc,
clang, icc, etc. (which were all subsequently fixed.)  They found only
one in CompCert, and arguably it wasn't a CompCert bug at all but
rather a bug in a Linux .h file.

A second bug was also found in CompCert. If I recall correctly, there
hadn't been much verified about the separate compilation facility, and
a South Korean research group (I think it was South Korean) found a
bug in it, fixed it, and extended the verified properties to cover it.

Note that this is the sum total of bugs ever found in CompCert, and
neither was a property that was formally verified but turned out not
to hold.

Compilers are, however, sort of an ideal case for formal
verification. What you're doing in a compiler verification is

1) providing a formal semantics for the input and output languages
and
2) demonstrating the equivalence of what goes in to the compiler and
what comes out with respect to those formal semantics.

Finding an all-encompassing description of other sorts of systems can
be more challenging to say the least.

BTW, note also the interesting feature of that second CompCert bug. This
demonstrates what I referred to in my earlier email as
"ratcheting".

Bugs _will_ be found in formally verified systems if only because one
can't always think of everything one wants to verify, but, once a bug
is found and the new property is added to the set of verified
properties, that bug will _never_ reoccur.

Contrast this with what usually happens when a bug is found in
non-verified code. The single instance of the bug is patched, perhaps
some regression tests that may or may not fully exercise all the
involved cases is put into the test suite, and one hopes that the
thing doesn't show up again in another form.

The "ratchet" provided by formal verification is substantially more
powerful than ordinary testing in this regard. It provides assurance
that a bug will not re-appear rather than the hope that you thought of
strong enough test cases.

> It is clear there may still be bugs in the verification
> methodology as well as in the choice of what to verify.

I think the latter is the big problem right now, and will remain so
permanently. Bugs in fully formal verification are likely to be rare
but will happen -- they can occur only if there are bugs in Coq (or
the equivalent) which have tended to be rare.

If they start happening more often, I suspect that the problem of the
shoemaker's children going shoeless will get more attention and those
systems will themselves get a lot more formalization. One cannot, of
course, prove the consistency of those systems (at least not within
themselves), but you can do a lot short of that.

> >You can run Coverity over a program every day and not find serious
> >problems in it that a formal verification will utterly
> >eliminate. Static analysis simply isn't able to do a lot of this
> >stuff. Yes, static analysis is great, but it isn't the same
> >thing.
>
> The real value today of formal methods is that they force people
> to take a different view of their programs. Looking at things
> from a different viewpoint frequently shows things you didn't
> see before. This feature alone makes them worthwhile. Making
> them easier to use will spread this advantage.

I've noted that merely learning how formal verification works changes
your view of programming as well. You start thinking in terms of
things like pre and post conditions in a way you simply didn't before.

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