[Cryptography] Security proofs prove non-failproof

Ilya Levin ilevin at gmail.com
Wed Feb 22 10:50:03 EST 2017


On Wed, Feb 22, 2017 at 11:10 PM, Perry E. Metzger <perry at piermont.com> wrote:
>
> I believe (correct me if I'm wrong) that CMBC is oriented towards
> proving the safety of things like pointer operations.

Yes, pointer operations, memory leaks. It also covers bounds and
division by zero checks together with signed/unsigned and float
overflows.

> 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

Thanks for reminding about this one. I saw it once few years ago,
postponed looking closer until some other time and successfully forgot
about it :)

Ilya


More information about the cryptography mailing list