Ironclad apps: End-to-end security via automated full-system verification

Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, Brian Zill

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

125 Citations (SciVal)

Abstract

An Ironclad App lets a user securely transmit her data to a remote machine with the guarantee that every instruction executed on that machine adheres to a formal abstract specification of the app's behavior. This does more than eliminate implementation vulnerabilities such as buffer overflows, parsing errors, or data leaks; it tells the user exactly how the app will behave at all times. We provide these guarantees via complete, low-level software verification. We then use cryptography and secure hardware to enable secure channels from the verified software to remote users. To achieve such complete verification, we developed a set of new and modified tools, a collection of techniques and engineering disciplines, and a methodology focused on rapid development of verified systems software. We describe our methodology, formal results, and lessons we learned from building a full stack of verified software. That software includes a verified kernel; verified drivers; verified system and crypto libraries including SHA, HMAC, and RSA; and four Ironclad Apps.

Original languageEnglish (US)
Title of host publicationProceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014
PublisherUSENIX Association
Pages165-181
Number of pages17
ISBN (Electronic)9781931971164
StatePublished - 2014
Event11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014 - Broomfield, United States
Duration: Oct 6 2014Oct 8 2014

Publication series

NameProceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014

Conference

Conference11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014
Country/TerritoryUnited States
CityBroomfield
Period10/6/1410/8/14

All Science Journal Classification (ASJC) codes

  • Information Systems
  • Computer Networks and Communications
  • Hardware and Architecture

Fingerprint

Dive into the research topics of 'Ironclad apps: End-to-end security via automated full-system verification'. Together they form a unique fingerprint.

Cite this