The last time Hackerfall tried to access this page, it returned a not found error. A cached version of the page is below, or click here to continue anyway

hypotext - Verified Correctness and Security of OpenSSL HMAC

Verified Correctness and Security of OpenSSL HMAC

I’m a co-author on this paper, which will appear in USENIX Security ‘15 in the excellently-named session “Sock It To Me: TLS No Less.”


Lennart Beringer, Princeton University; Adam Petcher, Harvard University and MIT Lincoln Laboratory; Katherine Q. Ye and Andrew W. Appel, Princeton University


We have proved, with machine-checked proofs in Coq, that an OpenSSL implementation of HMAC with SHA-256 correctly implements its FIPS functional specification and that its functional specification guarantees the expected cryptographic properties. This is the first machine-checked cryptographic proof that combines a source program implementation proof, a compiler-correctness proof, and a cryptographic-security proof, with no gaps at the specification interfaces.

The verification was done using three systems within the Coq proof assistant: the Foundational Cryptography Framework, to verify crypto properties of functional specs; the Verified Software Toolchain, to verify C programs w.r.t. functional specs; and CompCert, for verified compilation of C to assembly language.

You can find the full paper here.

  1. funwithlanguages liked this

  2. mwgamera liked this

  3. quasidot reblogged this from katherineye

  4. katherineye posted this

Continue reading on