[Cryptography] Security proofs prove non-failproof

[Perry E. Metzger]

On Sat, 18 Feb 2017 12:49:51 -0500
Jon Callas <jon at callas.org> wrote:

> As a mathematical logician, I'm a huge fan of proofs, and yet sneer
> at a lot of security proofs.
> 
> We don't have formal definitions of what security even means.

I disagree. I think we don't know what the complete set of things that
constitutes security would mean (and we probably can't know), but we
have learned from experience a lot of things that mean *insecurity* and
we can establish that they aren't present.

We can prove that code takes the same amount of time and/or power to do
every cryptographic operation (or that otherwise those particular side
channels can't leak information). We can prove that code has no buffer
overflows, integer overflows, stack overflows, etc., and those proofs
mean something. We can show that particular attacks we know about that
have been used against cryptographic protocols in the past can't be
used against a particular protocol that is under consideration. We can
prove that particular parts of a system are well isolated from each
other. With time, we learn more and more things that we want to know
about our systems, and we can incorporate these into the set of
properties we want to verify.

Does this prove that code or a protocol is secure, let alone
absolutely secure? Hell no. Is it still very, very useful? Hell yes!

I think there's been a lot of time spent convincing ourselves, as a
community, that formal verification isn't very useful because for so
long it was impossible. So, it was psychologically nice to say "well,
we can't do it, but if we could do it it wouldn't be useful, so there's
no reason to fret over it."

Now, however, it is possible, and people are finding and stopping real
bugs with these techniques.

It *is* very important not to see them as magical panaceas. For too
long people have regarded formal verification as a way to show that
a system is perfect, and that is not what it does. Rather, it is a
way of showing that specific properties hold in the code, and as you
point out, we often don't even know what property we need to verify.
However, for properties you want to assure, proofs are an amazingly
strong "ratchet" that allows you to demonstrate that your code cannot
backslide against a given property you need it to have.

Perry