The Coq mailing list

["Andrew W. Appel" <appel AT cs.Princeton.EDU>]

My paper covers only one component of OpenSSL: cryptographic hashing with
the 256-bit Secure Hash Algorithm (SHA-256).  In fact I found no bugs in
SHA-256; but as the paper explains, OpenSSL's implementation of SHA-256
does many "clever" things that make the specification and proof interesting.

I make no guarantee about other components of OpenSSL; there is no
contradiction between my verification of SHA-256 and the existence of
the CCS-Injection or Heartbleed vulnerabilities in other components.

-- Andrew Appel


On 6/6/2014 7:34 AM, Pierre Courtieu wrote:
> 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