[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