Skip to main content

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

Publication ,  Conference
Hawblitzel, C; Howell, J; Lorch, JR; Narayan, A; Parno, B; Zhang, D; Zill, B
Published in: Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014
January 1, 2014

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.

Duke Scholars

Published In

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

Publication Date

January 1, 2014

Start / End Page

165 / 181
 

Citation

APA
Chicago
ICMJE
MLA
NLM
Hawblitzel, C., Howell, J., Lorch, J. R., Narayan, A., Parno, B., Zhang, D., & Zill, B. (2014). Ironclad apps: End-to-end security via automated full-system verification. In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014 (pp. 165–181).
Hawblitzel, C., J. Howell, J. R. Lorch, A. Narayan, B. Parno, D. Zhang, and B. Zill. “Ironclad apps: End-to-end security via automated full-system verification.” In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014, 165–81, 2014.
Hawblitzel C, Howell J, Lorch JR, Narayan A, Parno B, Zhang D, et al. Ironclad apps: End-to-end security via automated full-system verification. In: Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014. 2014. p. 165–81.
Hawblitzel, C., et al. “Ironclad apps: End-to-end security via automated full-system verification.” Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014, 2014, pp. 165–81.
Hawblitzel C, Howell J, Lorch JR, Narayan A, Parno B, Zhang D, Zill B. Ironclad apps: End-to-end security via automated full-system verification. Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014. 2014. p. 165–181.

Published In

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

Publication Date

January 1, 2014

Start / End Page

165 / 181