coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Andrew W. Appel" <appel AT cs.Princeton.EDU>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Verification of OpenSSL SHA-256
- Date: Thu, 05 Jun 2014 10:20:29 -0400
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
- [Coq-Club] Verification of OpenSSL SHA-256, Andrew W. Appel, 06/05/2014
- Re: [Coq-Club] Verification of OpenSSL SHA-256, Pierre Courtieu, 06/06/2014
- Re: [Coq-Club] Verification of OpenSSL SHA-256, Andrew W. Appel, 06/06/2014
- Re: [Coq-Club] Verification of OpenSSL SHA-256, Pierre Courtieu, 06/06/2014
Archive powered by MHonArc 2.6.18.