[Cryptography] Security proofs prove non-failproof

[Perry E. Metzger]

On Thu, 16 Feb 2017 08:33:49 +0000 Peter Gutmann
<pgut001 at cs.auckland.ac.nz> wrote:
> The IACR ePrint archive has just published a paper, "Attacks on
> Secure Logging Schemes", http://eprint.iacr.org/2017/095, that
> breaks three secure logging schemes.  What makes this one
> particularly interesting is that all of the schemes that were
> broken came with security proofs.
> 
> Peter (who's a big fan of schemes that can be handled with "two
> beers' worth of analysis", uh, proofs).

I'm a very big fan of proofs. However, one has to recognize that
proofs do not demonstrate perfection. You can always have tried to
prove the wrong thing, and (especially for paper and pencil proofs)
there can be flaws in proofs just like there are bugs in programs.

In a related (but not exactly the same) case: it is especially
important to remember this when formally verifying code using modern
tools like Coq or F* or what have you. There's a temptation to think
that if you formally verify a piece of code that it is perfect and
bug-free. Not so. What you've done is demonstrate some set of
properties "almost certainly*" hold for the code, but those might
only be a subset of the properties you need to hold, or might be the
wrong properties entirely.

What formal verification gives you is a ratchet. You know that, if
you ask the right question, you will not backslide, and future
versions of your code will continue to have the property hold. This is
a very, very powerful tool, and one that I think is going to
revolutionize our field, but it is still a tool, not a panacea,
and you have to remain vigilant.

This will bite people a lot as formal verification becomes more and
more widely used, but I still think formal verification is worthwhile
in spite of it.

[*"Almost certainly" rather than "certainly" because (a) you may have
stated the properties you wanted incorrectly and (b) because there
can be no proof that your underlying logic is consistent, at least if
it is a useful underlying logic. (b) is especially troublesome in
systems where there's a lot of active development done on the formal
verification tools with relatively little use of formal tools to
assure the quality of the tools themselves -- ironically, for some of
these systems, there isn't even a formal description of the underlying
logic and the shoemaker's children still go shoeless. But that's
another discussion for another day.]

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