[Cryptography] Security proofs prove non-failproof

[Perry E. Metzger]

On Wed, 22 Feb 2017 14:13:35 +1000
"James A. Donald" <jamesd at echeque.com> wrote:
> On 2/22/2017 1:03 AM, Perry E. Metzger wrote:
> > We can prove that code has no buffer
> > overflows, integer overflows, stack overflows, etc., and those
> > proofs mean something.
>
> That would be handy.  Are you telling me that there is a system that
> can digest a suitably prepared C++ program and tell me it cannot have
> a buffer overflow, memory leak, signed integer overflow etc, and
> complain to me if there is potential for these things?

Not C++ yet (because producing a formal semantics for C++ is a
nightmare), but for C, you can use techniques like those that were
used for programs like seL4 and CertiKOS, or packages like the
Verified Software Toolchain (VST), and prove that a chunk of code has
no such issues.

Currently this involves quite a lot of work, though the amount of work
involved keeps rapidly dropping. What you basically do is prove
properties of the code, and there can be no algorithm that finds
proofs in bounded time. However, there are large bits of automation
that can assist along the way.

I recommend looking in to VST if you're interested in doing this for C
specifically. It's not the only available tool but it's the best
packaged at the moment.

(You can also, at some runtime cost and sometimes at very serious
runtime cost, use mechanisms that will detect any such failure at
runtime and abort the program, but that's of much less interest if
you're trying to build a reliable, maximum performance system that
does not fail. The most thorough system I know of for this is
tis-interpreter, which is very slow but detects most forms of
undefined behavior.)

> Obviously there is no mechanical or automated method that can tell
> whether or not an arbitrary program can develop such errors.

Not as a static analyzer, no. The halting problem is a thorn in the
side of many such dreams. However, you can *manually* verify that no
such conditions exist using a proof system.

Perry