The last time Hackerfall tried to access this page, it returned a not found error. A cached version of the page is below, or clickhereto 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.”

Authors:

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

Abstract:

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 katherineye.com