Skip to main content
USENIX
  • Conferences
  • Students
Sign in
  • Home
  • Attend
    • Venue, Hotel, and Travel
    • Students and Grants
    • Co-Located Workshops
  • Program
    • At a Glance
    • Technical Sessions
    • Poster Session
  • Activities
    • Birds-of-a-Feather Sessions
    • Poster Session
    • WiPs
  • Participate
    • Call for Papers
      • Important Dates
      • Symposium Organizers
      • Symposium Topics
      • Refereed Papers
      • Shadow PC
      • Symposium Activities
      • Submitting Papers
    • Instructions for Participants
  • Sponsorship
  • About
    • Symposium Organizers
    • Services
    • Questions
    • Help Promote!
    • Past Symposia
  • Home
  • Attend
    • Venue, Hotel, and Travel
    • Students and Grants
    • Co-Located Workshops
  • Program
  • Activities
  • Participate
    • Call for Papers
    • Instructions for Participants
  • Sponsorship
  • About
    • Symposium Organizers
    • Services
    • Questions
    • Help Promote!
    • Past Symposia

sponsors

Platinum Sponsor
Gold Sponsor
Gold Sponsor
Silver Sponsor
Silver Sponsor
Silver Sponsor
Bronze Sponsor
Bronze Sponsor
General Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Industry Partner
Industry Partner

help promote

USENIX Security '16 button

Get more
Help Promote graphics!

connect with usenix


  •  Twitter
  •  Facebook
  •  LinkedIn
  •  Google+
  •  YouTube

twitter

Tweets by USENIXSecurity

usenix conference policies

  • Event Code of Conduct
  • Conference Network Policy
  • Statement on Environmental Responsibility Policy

You are here

Home ยป Verified Correctness and Security of OpenSSL HMAC
Tweet

connect with us

Verified Correctness and Security of OpenSSL HMAC

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.

Lennart Beringer, Princeton University

Adam Petcher, Harvard University and MIT Lincoln Laboratory

Katherine Q. Ye, Princeton University

Andrew W. Appel, Princeton University

Open Access Media

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-939133-11-3},
address = {Washington, D.C.},
pages = {207--221},
url = {https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/beringer},
publisher = {USENIX Association},
month = aug,
}
Download
Beringer PDF
View the slides

Presentation Video 

Presentation Audio

MP3 Download

Download Audio

  • Log in or    Register to post comments

Open access to the USENIX Security '15 videos sponsored by Symantec.

Platinum Sponsors

Gold Sponsors

Silver Sponsors

Bronze Sponsors

General Sponsors

Media Sponsors & Industry Partners

Open Access Publishing Partner

© USENIX

  • Privacy Policy
  • Contact Us