News & Events

---

Special CS Seminar: IronFleet: Proving Practical Distributed Systems Correct

Speaker: Jay Lorch

Location: 715/719 Broadway 1221

Date: Feb. 1, 2016, 2 p.m.

Distributed systems are notorious for harboring subtle bugs. Verification can, in principle, eliminate these bugs a priori, but verification has historically been difficult to apply at full-program scale, much less distributed-system scale. This talk will describe IronFleet, our methodology for building practical and provably correct distributed systems based on a unique blend of TLA-style state-machine refinement and Hoare-logic verification. We demonstrate this methodology on a complex implementation of a Paxos-based replicated state machine library and a lease-based sharded key-value store. We prove that each obeys a concise safety specification, as well as desirable liveness requirements. Each implementation achieves performance competitive with a reference system. With our methodology and lessons learned, we aim to raise the standard for distributed systems from "tested" to "correct."

The talk will also briefly discuss the broader Ironclad project, of which IronFleet is part, including its past successes and future plans. The goal of the Ironclad project is to realize the power of automated software verification to build verifiable, secure, and practical system software. We've open-sourced our code, and made it available at https://github.com/Microsoft/Ironclad, to encourage other researchers to further extend the state of the art in systems verification.