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

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

Computer Science and Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014
Publisher	USENIX Association
Pages	165-181
Number of pages	17
ISBN (Electronic)	9781931971164
State	Published - 2014
Event	11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014 - Broomfield, United States Duration: Oct 6 2014 → Oct 8 2014

Publication series

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

Conference

Conference	11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014
Country	United States
City	Broomfield
Period	10/6/14 → 10/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

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). (Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014). USENIX Association.

Hawblitzel, Chris ; Howell, Jon ; Lorch, Jacob R. ; Narayan, Arjun ; Parno, Bryan ; Zhang, Danfeng ; Zill, Brian. / 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. USENIX Association, 2014. pp. 165-181 (Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014).

@inproceedings{c7d580917bf64e398493fbda8167fed9,

title = "Ironclad apps: End-to-end security via automated full-system verification",

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.",

author = "Chris Hawblitzel and Jon Howell and Lorch, {Jacob R.} and Arjun Narayan and Bryan Parno and Danfeng Zhang and Brian Zill",

note = "Funding Information: We thank Jeremy Elson, Cedric Fournet, Shuvendu Lahiri, Rustan Leino, Nikhil Swamy, Valentin Wuestholz, Santiago Zanella Beguelin, and the anonymous reviewers for their generous help, guidance, and feedback. We are especially grateful to our shepherd Gernot Heiser, whose insightful feedback improved the paper.; 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014 ; Conference date: 06-10-2014 Through 08-10-2014",

year = "2014",

language = "English (US)",

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

publisher = "USENIX Association",

pages = "165--181",

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

}

Hawblitzel, C, Howell, J, Lorch, JR, 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. Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014, USENIX Association, pp. 165-181, 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014, Broomfield, United States, 10/6/14.

Ironclad apps : End-to-end security via automated full-system verification. / Hawblitzel, Chris; Howell, Jon; Lorch, Jacob R.; Narayan, Arjun; Parno, Bryan; Zhang, Danfeng; Zill, Brian.

Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014. USENIX Association, 2014. p. 165-181 (Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Ironclad apps

T2 - 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014

AU - Hawblitzel, Chris

AU - Howell, Jon

AU - Lorch, Jacob R.

AU - Narayan, Arjun

AU - Parno, Bryan

AU - Zhang, Danfeng

AU - Zill, Brian

N1 - Funding Information: We thank Jeremy Elson, Cedric Fournet, Shuvendu Lahiri, Rustan Leino, Nikhil Swamy, Valentin Wuestholz, Santiago Zanella Beguelin, and the anonymous reviewers for their generous help, guidance, and feedback. We are especially grateful to our shepherd Gernot Heiser, whose insightful feedback improved the paper.

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85076877276&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85076877276&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:85076877276

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

SP - 165

EP - 181

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

PB - USENIX Association

Y2 - 6 October 2014 through 8 October 2014

ER -

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. USENIX Association. 2014. p. 165-181. (Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014).