TY - GEN

T1 - Verified correctness and security of OpenSSL HMAC

AU - Beringer, Lennart

AU - Petcher, Adam

AU - Ye, Katherine Q.

AU - Appel, Andrew W.

PY - 2015/1/1

Y1 - 2015/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84985950431&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84985950431&partnerID=8YFLogxK

M3 - Conference contribution

T3 - Proceedings of the 24th USENIX Security Symposium

SP - 207

EP - 221

BT - Proceedings of the 24th USENIX Security Symposium

PB - USENIX Association

T2 - 24th USENIX Security Symposium

Y2 - 12 August 2015 through 14 August 2015

ER -