# Verified correctness and security of OpenSSL HMAC

## Author(s): Beringer, L; Petcher, A; Ye, K; Appel, Andrew W.

To refer to this page use: http://arks.princeton.edu/ark:/88435/pr1k596
 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. Publication Date: 2015 Citation: Beringer, L, Petcher, A, Ye, K, Appel, A. "Verified correctness and security of OpenSSL HMAC" Proceedings of the 24th USENIX Conference on Security Symposium, 207 - 221 Pages: 207 - 221 Type of Material: Conference Article Journal/Proceeding Title: Proceedings of the 24th USENIX Conference on Security Symposium, August 12-14, 2015, Washington, D.C. Version: This is the author’s final manuscript. All rights reserved to author(s).