Verified correctness and security of OpenSSL HMAC

Lennart Beringer, Adam Petcher, Katherine Q. Ye, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

47 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationProceedings of the 24th USENIX Security Symposium
PublisherUSENIX Association
Pages207-221
Number of pages15
ISBN (Electronic)9781931971232
StatePublished - Jan 1 2015
Event24th USENIX Security Symposium - Washington, United States
Duration: Aug 12 2015Aug 14 2015

Publication series

NameProceedings of the 24th USENIX Security Symposium

Conference

Conference24th USENIX Security Symposium
CountryUnited States
CityWashington
Period8/12/158/14/15

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Information Systems
  • Safety, Risk, Reliability and Quality

Fingerprint Dive into the research topics of 'Verified correctness and security of OpenSSL HMAC'. Together they form a unique fingerprint.

  • Cite this

    Beringer, L., Petcher, A., Ye, K. Q., & Appel, A. W. (2015). Verified correctness and security of OpenSSL HMAC. In Proceedings of the 24th USENIX Security Symposium (pp. 207-221). (Proceedings of the 24th USENIX Security Symposium). USENIX Association.