[Cryptography] Security proofs prove non-failproof

[Perry E. Metzger]

On Fri, 24 Feb 2017 12:36:46 +1000
"James A. Donald" <jamesd at echeque.com> wrote:

> On 2/23/2017 12:33 AM, Perry E. Metzger wrote:
> > 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
>
> C++ however can substantially automate memory management through
> C++11 smart pointers.

Sure, but formal verification is much more extensive than that.

For example, say that you want to show not only that the scheduler in
your operating system will not access past the end of an array,
but also that it will faithfully schedule things.

Or say that you want to show that your sorting function is not only
free of buffer overflows and integer overflows but also actually
returns a sorted version of its input.

Or say that you want not only the assurance that your program won't
unknowingly exhaust its stack but the assurance that it will never
even try to do so, and thus will not crash from stack exhaustion.

Or, at a much larger scale, say you want to know not merely that your
compiler won't crash, but that it compiles code _correctly_.

Formal verification will do that, while smart pointers and the like
will not.

The point of formal verification isn't to merely assure that you have
a safe language (in the sense that C is not safe but OCaml is) in
which you won't get things like array bounds violations, but to prove
that the program meets a logical specification of its behavior.

For example, to take the sorting example, without knowing anything
about how the sort function works internally, I can specify that its
output must be a non-decreasing ordered permutation of the input. If I
can prove that this is true, I know the sorting function will _always_
do what I expect.

In the case of CompCert, there is a mathematical theorem, mechanically
checked in Coq, that the output machine language program behaves in a
way that's observationally indistinguishable from the input C language
program. This of course requires a detailed specification in formal
logic for how a C program is supposed to behave, and one objection
might be that *this* might have bugs, but so far, no one has found
such a bug* in the released CompCert compiler, likely because of the
care taken with the formal specification.

Regardless, though, the knowledge that the compiler's output is very
very likely faithful is a much higher standard than knowing it does
not leak memory.

(*In fact, as I mentioned in a previous message, that's not strictly
true. Two bugs have been found to my knowledge, but one was in an
include file and not in CompCert, and the other was in a previously
unverified property of separate compilation. This is still an enormous
contrast to the number of bugs routinely found in GCC and other
compilers.)

Perry