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 produced the first complete stack of verified-secure software. We also developed the first methodology for verifying both the safety and liveness of complex distributed systems implementations. Most recently, we have embarked on a long-term effort to build and deploy a full replacement for the HTTPS ecosystem.

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