Verified correctness and security of OpenSSL HMAC

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

Verified correctness and security of OpenSSL HMAC

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 language	English (US)
Title of host publication	Proceedings of the 24th USENIX Security Symposium
Publisher	USENIX Association
Pages	207-221
Number of pages	15
ISBN (Electronic)	9781931971232
State	Published - Jan 1 2015
Event	24th USENIX Security Symposium - Washington, United States Duration: Aug 12 2015 → Aug 14 2015

Publication series

Name	Proceedings of the 24th USENIX Security Symposium

Conference

Conference	24th USENIX Security Symposium
Country/Territory	United States
City	Washington
Period	8/12/15 → 8/14/15

All Science Journal Classification (ASJC) codes

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

Cite this

@inproceedings{a4923a86f52840cabecfc38337428996,

title = "Verified correctness and security of OpenSSL HMAC",

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.",

author = "Lennart Beringer and Adam Petcher and Ye, {Katherine Q.} and Appel, {Andrew W.}",

year = "2015",

month = jan,

day = "1",

language = "English (US)",

series = "Proceedings of the 24th USENIX Security Symposium",

publisher = "USENIX Association",

pages = "207--221",

booktitle = "Proceedings of the 24th USENIX Security Symposium",

note = "24th USENIX Security Symposium ; Conference date: 12-08-2015 Through 14-08-2015",

}

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 -

Verified correctness and security of OpenSSL HMAC

Abstract

Publication series

Conference

All Science Journal Classification (ASJC) codes

Other files and links

Fingerprint

Cite this