[Cryptography] Security proofs prove non-failproof

Ilya Levin ilevin at gmail.com
Wed Feb 22 09:48:43 EST 2017


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.

Ilya


More information about the cryptography mailing list