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.
Publisher Copyright:
© 2014 by The USENIX Association. All Rights Reserved.
Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.
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 -