[Cryptography] Security proofs prove non-failproof

[Patrick]

James A. Donald wrote on 02/21/2017 11:13 PM:

> What I have found useful is making sure a program does not in fact
> develop memory leaks when actually run.  Profiling is also handy when
> one wants to optimize a program.  But these are ancient tools.

I wrap malloc and free inside routines which count the number of blocks
and bytes allocated, and then I check that those values are precisely
zero at the end of the program run:

https://github.com/chkoreff/Fexl/blob/master/src/memory.c

I also do quasi-formal verification of my code, certainly not to the
level that Perry Metzger talks about, but I do try to prove within my
own mind that mallocs and frees are balanced.  Then, if I refactor code,
I use only correctness-preserving transformations, which if applied
correctly, should give me the "ratchet effect" Perry describes.

As for other properties of my code, I do have an extensive regression
test suite, which also should give me some ratchet effect.  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.

That's as far as I've applied formal verification concepts, as yet.  The
particular project linked above is a functional language interpreter, so
I'm not sure I'm capable of specifying a formal model of it.  I have
considered writing a Fexl program which generates all the C code for
Fexl itself.  It wouldn't be that difficult, and the resulting
compression could facilitate an analysis of its correctness.


-- Patrick