Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Verification of OpenSSL SHA-256

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Verification of OpenSSL SHA-256


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page