[Cryptography] Security proofs prove non-failproof

[Perry E. Metzger]

On Wed, 22 Feb 2017 22:48:43 +0800
Ilya Levin <ilevin at gmail.com> wrote:
> On Wed, Feb 22, 2017 at 12:13 PM, James A. Donald
> <jamesd at echeque.com> wrote:
> >
> > That would be handy.  Are you telling me that there is a system
> > that can digest a suitably prepared C++ program and tell me it
> > cannot have a buffer overflow, memory leak, signed integer overflow
> > etc, and complain to me if there is potential for these things? 
> 
> Not sure about the ++ thing, but there are some such tools available
> to handle C. For example:
> * Frama-C, http://frama-c.com
> * The Software Analysis Workbench, http://saw.galois.com
> * CBMC, http://www.cprover.org/cbmc/
> 
> The last one is my personal favourite.

I believe (correct me if I'm wrong) that CMBC is oriented towards
proving the safety of things like pointer operations.

The Verified Software Toolchain is a very general tool for verifying C
programs for arbitrary properties. It's been used, for example, to
fully verify the correctness of cryptographic code.

 http://vst.cs.princeton.edu

Perry