Ironclad: Full Verification of Complex Systems
Bryan Parno
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've also recently expanded the scope of our verification efforts to distributed systems, which are notorious for harboring subtle bugs. We developed IronFleet, a methodology for building practical and provably correct distributed systems, and demonstrated it 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, I will 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".