[Cryptography] Security proofs prove non-failproof

[Patrick Chkoreff]

Perry E. Metzger wrote on 02/22/2017 10:07 AM:

>> In addition to empirical testing, I often think in terms of pre- and
>> post-conditions and loop invariants, which in conjunction with
>> correctness-preserving code transformations, are in effect a
>> quasi-formal proof.
> 
> One popular technique in formal verification is the use of Hoare logic
> and its descendants, which is where the notion of pre and
> postconditions comes from.

Yes, I learned the technique by reading Tony Hoare back in the 80s.

Basically what I've done is, instead of maintaining a *separate* entity
called a "proof", I have aimed to make my code itself an ongoing sort of
proof.  By that I mean whenever I transform the code, I do it in a
systematic way which, if applied correctly, is guaranteed either to (1)
maintain the original correct behavior of the code, or (2) alter the
behavior of the code in a way which is also correct.

Back in the 80s when working at HP, an old friend of mine named Byron
Jennings was asked how you write good code.  He replied, "Start with the
null program, and then debug it until it does what you want."  Now
before anyone rips his shirt at this heresy, keep in mind that he meant
it tongue-in-cheek, though I think there is a grain of truth in it.

Consider this program, which is guaranteed not to have any memory bugs,
including leaks or use after free:

int main(void)
    {
    return 0;
    }

Definitely no memory problems there.

Now I can "evolve" that program one step in a way which guarantees
correctness:

#include <stdlib.h>

int main(void)
    {
    char *p = malloc(30);
    free(p);
    return 0;
    }

Definitely no memory problems there, assuming I did the transformation
correctly, which I'm pretty sure I did.

One can then imagine continuing to evolve this program one correct step
at a time until it does what you want, for example:

#include <stdlib.h>

char *new_thing(void)
    {
    return malloc(30);
    }

int main(void)
    {
    char *p = new_thing();
    free(p);
    return 0;
    }


Recall that each transformation step must either:

1. Maintain the original correct behavior of the code.

2. Alter the behavior of the code in a way which is also correct.

Clearly in Formal Verification, "correct" is defined in reference to
some logical model apart from the code itself.

In my own "Formally Guided" Verification, "correct" is typically defined
in terms of some new regression test case which I devise specifically to
exercise the altered behavior in a type-2 step.  In practice, when I
alter the behavior, I typically insert a call like die("TODO") in the
code where the new behavior will occur.  Then if necessary I add a new
case to the regression test to force it to hit the die call.  Then I
replace the die call with the actual code to handle the new behavior,
and ensure that the new case in the regression test is handled in a way
which appears sane and correct.

If I were doing actual Formal Verification, I would probably still alter
the regression test after every alteration step, because as Knuth says,
"Beware of bugs in the above code:  I have only proved it correct, not
tried it."  However, I would also alter the formal model against which I
was verifying correctness, because as Perry says, the proof
infrastructure must be maintained in parallel with the code.


There are standard code transformations which are always correct, for
example:

if (condition)
  {
  do_true();
  do_other();
  }
else
  {
  do_false();
  do_other();
  }

Can be transformed to:

if (condition)
  {
  do_true();
  }
else
  {
  do_false();
  }
do_other();


And vice-versa.  Both directions are useful.  The forward direction is
used to unify repeated code into a single place.  The reverse direction
is used to replicate code into two separate places, in preparation for a
behavior-altering transformation to one of the places.

Note that if do_other() occurs *before* the condition test, it cannot
always be replicated before the do_true and do_false calls, because the
call to do_other might alter variables which affect the truth of the
condition.  However, with suitable data flow analysis it can often be done.

There are similar correct transformations involving loops, folding code
into procedures, lifting hard-coded values into parameters, etc.

The techniques I describe have proven to be Far Better than Nothing, and
I have turned them into a pretty good living.  I am certainly amenable
to more formal methods, but honestly when someone requests something
like a report which shows how realized gains were allocated to
investors, I immediately start hacking code which spews out HTML,
without reference to a formal model of correctness.  However, I DO still
apply the "Formally Guided" Verification techniques described above.


-- Patrick