[Cryptography] Security proofs prove non-failproof

[Peter Gutmann]

Perry E. Metzger <perry at piermont.com> writes:

>I'm a very big fan of proofs. 

I'm a fan of proofs of mathematical theorems and algorithms in the
mathematical sense (meaning things like "O( n ^ 2/3 ) worst-case"), proofs of
correctness less so.  The problem in that case is that you're not proving a
mathematical property but possibly proving (E&OE) that the algorithm
corresponds to some model that's defined by the defender/algorithm designer.
In other words the designer gets to define (or choose) whatever abstract model
they feel like, and then possibly proves that their design is OK within that
model.  The poor attacker, who doesn't even know that the model exists, also
doesn't know that they're supposed to be stopped by the provably-secure
security system and bypasses it after two beers' worth of analysis.

That was what I meant with the final comment, it was an allusion to making
something so simple there are obviously no holes or making it so complex there
are no obvious holes, requiring an even more complex proof that it's OK to
use.

>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.

I guess we'll have to disagree on this... I've been hearing this since the
1970s (well, reading about it after the event in the case of the 1970s), any
minute now formal methods will magically start working and all our code will
be a lot better.  We've certainly come a long way since Ina Jo/Ina Mod and
Gypsy and the Boyer-Moore theorem prover (whose use was famously described as
"like trying to make a string go in a certain direction by pushing it"), but
in 40 years we've only managed to go from "near-impossible to use" to "very
difficult to use".  Extrapolating from 40 years of previous work, at this rate
it's going to be centuries before they're ready to go mainstream.  And given
that tools like PREfast and Coverity and Fortify haven't sat still in the
meantime, they've got pretty stiff competition to deal with.

It's also illustrative to look at the relative progress of static analysers,
they've gone from glorified greps 15 years ago (some of them were literally
glorified greps, "I found a call to gets(), this is dangerous") to extremely
powerful tools that ship as standard with compilers (clang, Visual Studio,
Misra compilers) and in many shops are part of the default build process.
PREfast was usable - not great, but usable - by about VS 2005, and the clang
analyser was about 2007?, so that's 5-7 years to general use, rather than 40
and counting for formal methods.

Peter.