[Cryptography] Security proofs prove non-failproof

Perry E. Metzger perry at piermont.com
Wed Feb 22 10:07:55 EST 2017


On Wed, 22 Feb 2017 09:34:51 -0500
Patrick <patrick at rayservers.net> wrote:

> 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

There are tools like Valgrind, of course, that do much of this sort of
thing at runtime while debugging that help with finding the precise
location of a memory leak.

Note that while checking that all allocs and frees match is useful, it
doesn't point out the biggest potential source of error in allocated
memory, which is use after free. Valgrind does do that IIRC.

And, as has been previously discussed, there are much more modern
tools, including the various LLVM sanitizers (like LeakSanitizer and
AddressSanitizer) that are built in to clang.

However, all such mechanisms are fairly weak compared to what true
formal verification can do.

> 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.

That's much more of a paper and pencil sort of proof than "quasi" formal
verification. In the real thing, you use an automated proof assistant
like Coq that mechanically checks the proofs involved, and which is
not subject to getting tired or otherwise making a mistake. (After
all, the whole reason you have bugs in your code is that humans are
fallible.)

> As for other properties of my code, I do have an extensive regression
> test suite, which also should give me some ratchet effect.

Unfortunately, even the best regression test suites, though vastly
better than not testing, are still nowhere near as good as what formal
verification can do for you. The problem is, of course, that you
cannot know that you've covered all possible cases without a proof.

> 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.

Perry


More information about the cryptography mailing list