The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hello Andrew,

I want to be the first to ask: as it is a certified implementation of
openssl, it is immune to the injection attack mentioned this morning
on the present list, right :) ?

All the best


2014-06-05 16:20 GMT+02:00 Andrew W. Appel 
<appel AT cs.princeton.edu>:
> Coq-Club members may be interested in this recent result:
>
> Verification of a Cryptographic Primitive: SHA-256
>   by Andrew W. Appel
>   May 9, 2014
>
> ABSTRACT:
> A full formal machine-checked verification of a C program: the
> OpenSSL implementation of SHA-256. This is an interactive proof
> of functional correctness in the Coq proof assistant, using the
> Verifiable C program logic. Verifiable C is a separation logic for the
> C language, proved sound w.r.t. the operational semantics for C,
> connected to the CompCert verified optimizing C compiler.
>
> www.cs.princeton.edu/~appel/papers/verif-sha.pdf
>