[Cryptography] Security proofs prove non-failproof

[Jason Cooper]

Hi Perry, Jon,

On Tue, Feb 21, 2017 at 10:03:25AM -0500, Perry E. Metzger wrote:
> 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.

In a small attempt to address Jon's quoted point, I'd like to add two
terms.  "Security of the Primitive" and "Security of the System".  As
you say, Perry, formal proofs are very helpful in determining that a
given primitive has a property you need.  What I think Jon is
highlighting, and I'd like to as well, is that adding that primitive to
a system doesn't necessarily extend the property proof to the system.

As formal proofs improve, I'd like to see some work on building systems
from verified components; then deducing formal proofs of security
attributes for the *system*.

This would be very threat-model and environment dependent, but it would
be a start.  As an example, take the case of a nailed up VPN connection
between two physically secure facilities.  The connection goes over the
untrusted Internet.  The symmetric cipher, ephemeral session key
exchange, key signing, and session key derivation all have formal proofs
for their individual features.  Keeping it simple, let's say the KEX is
signed by static keys.  Is there a method to build on those individual
proofs to say something concrete about the system in a given environment
against a stated threat model?

Note that "environment" in this context includes the form, rate, and
patterns of the content carried within the encrypted connection.

thx,

Jason.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: Digital signature
URL: <http://www.metzdowd.com/pipermail/cryptography/attachments/20170221/d639ab7d/attachment.sig>