[Cryptography] Security proofs prove non-failproof

[Perry E. Metzger]

On Wed, 22 Feb 2017 22:45:40 +0100
Florian Weimer <fw at deneb.enyo.de> wrote:
> 
> My main problem with formal methods (apart from odd things like Z3
> giving me an invalid solution for pretty much the first problem I
> threw at it) is that with the current tools, it's a one-time effort,
> just like an audit.

Not really. Or at least, projects like CompCert, seL4, etc., set
themselves up to do long term maintenance of the proof in parallel
with the code.

> You can't put production code through the proof tool.

Well, if you talk to Test Driven Develpment types, you also can't test
code that wasn't designed for test and didn't have tests built in
parallel with the code and maintained in parallel with the code. If
you do want to retrofit existing code for TDD, you have to go through
a large effort to refactor it and add tests everywhere, and it isn't a
small thing. (See books like Feathers, "Working with Legacy Code",
which defines "Legacy Code" as any code that doesn't already have a
complete test infrastructure.)

This is much the same situation as trying to bring a reasonable test
infrastructure to legacy code (see above definition). You have to
build a proof infrastructure that is maintained in parallel with your
code.

The correct paradigm isn't "build large system, then hope it works",
it is "build large system with test infrastructure in parallel" or, in
the proof world, "build large system with proof infrastructure in
parallel". If you don't have such an infrastructure and have a legacy
system, you need to go through a large engineering effort to add one,
and then you maintain it going forward.

> Few people say this explicitly, unfortunately, but it seems
> that there is always an expectation that you massage the code (i.e. go
> from Ada to SPARK, from C to ACSL, etc.), prove the basic properties
> you get for free (such as termination, bounded resource use, and lack
> of memory safety violations--all stuff that is relatively easy to
> specify in general, but can be quite hard to prove in specific cases,
> obviously).  After patching things up, you then go back to the
> original code to fix things there as well.

BTW, in the world of systems like VST, you most certainly do *not*
massage the code and prove things about the massaged code. You work
with the actual code.

> But now someone makes a change to the original code to implement a new
> feature, and you have to do all that source code massaging again from
> scratch.  That clearly does not work.

Correct. You can't plan to do this once, you have to build this as
part of your software engineering effort, and with the expectation
that the proof infrastructure gets maintained in parallel.


Perry