Due to scheduled maintenance on Wednesday, October 16, from 10:30 am to 4:30 pm Pacific Daylight Time (UTC -7), parts of the USENIX website (e.g., conference registration, user account changes) may not be available. We apologize for the inconvenience.
If you are trying to register for LISA19, please complete your registration before or after this time period.
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 compilercorrectness 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.
USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.
BibTeX
@inproceedings {190894,
author = {Lennart Beringer and Adam Petcher and Katherine Q. Ye and Andrew W. Appel},
title = {Verified Correctness and Security of OpenSSL {HMAC}},
booktitle = {24th {USENIX} Security Symposium ({USENIX} Security 15)},
year = {2015},
isbn = {978-1-931971-232},
address = {Washington, D.C.},
pages = {207--221},
url = {https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/beringer},
publisher = {{USENIX} Association},
month = aug,
}
Twitter
Facebook
LinkedIn
Google+
YouTube
connect with us