Skip to main content

Distinguished Seminar:  Ironclad - Full Verification of Complex Systems

Date:October 17, 2016 
Talk Title:Ironclad - Full Verification of Complex Systems
Speaker:Bryan Parno, Researcher, Security & Privacy Research Group, Microsoft Research
Time & Location:12:00pm - 1:00pm
DEC, CIC building, Pittsburgh

Abstract

The Ironclad project at Microsoft Research is using a set of new and modified tools based on automated theorem proving to build Ironclad services.  An Ironclad service guarantees to remote parties that every CPU instruction the service executes adheres to a high-level specification, convincing clients that the service will be worthy of their trust.  To provide such end-to-end guarantees, we built a full stack of verified software.  That software includes a verified kernel; verified drivers; verified system and cryptography libraries including SHA, HMAC, and RSA; and four Ironclad Apps.  As a concrete example, our Ironclad database provably provides differential privacy to its data contributors.  In other words, if a client encrypts her personal data with the database's public key, then it can only be decrypted by software that guarantees, down to the assembly level, that it preserves differential privacy when releasing aggregate statistics about the data. 

We then expanded the scope of our verification efforts to distributed systems, which are notorious for harboring subtle bugs.  We have developed IronFleet, a methodology for building practical and provably correct distributed systems.  We demonstrated the methodology on a complex implementation of a Paxos-based replicated state machine library and a lease-based sharded key-value store.  We proved that each obeys a concise safety specification, as well as desirable liveness requirements.  Each implementation achieves performance competitive with a reference system. 

In this talk, we describe our methodology, formal results, and lessons we learned from building large stacks of verified systems software.  In pushing automated verification tools to new scales (over 70K lines of code and proof so far), our team has both benefited from automated verification techniques and uncovered new challenges in using them.

By continuing to push verification tools to larger and more complex systems, Ironclad ultimately aims to raise the standard for security- and reliability-critical systems from "tested" to "correct".

Speaker Bio

Bryan Parno is a Researcher in the Security and Privacy Group at Microsoft Research.  After receiving a Bachelor's degree from Harvard College, he completed his PhD at Carnegie Mellon University, where his dissertation won the 2010 ACM Doctoral Dissertation Award.  In 2011, he was selected for Forbes' 30-Under-30 Science List.  He formalized and worked to optimize verifiable computation, receiving a Best Paper Award at the IEEE Symposium on Security and Privacy his advances.  He coauthored a book on Bootstrapping Trust in Modern Computers, and his work in that area has been incorporated into the latest security enhancements in Intel CPUs. His research into security for new application models was incorporated into Windows and received a Best Paper Awards at the IEEE Symposium on Security and Privacy and the USENIX Symposium on Networked Systems Design and Implementation.  He has recently extended his interest in bootstrapping trust to the problem of building practical, formally verified secure systems. His other research interests include user authentication, secure network protocols, and security in constrained environments (e.g., RFID tags, sensor networks, or vehicles).