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

103 Scopus citations

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
CountryUnited 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