Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill
To eliminate possible bugs in a distributed system, verification techniques have been used by previous research works, but it is difficult to apply verification at full-program scale, much less distributed-system scale. On the other hand, thorough testing is considered best practice, but its efficacy is limited. Due to the complexity of distributed systems, previous works only apply formal verification in a simplified form without extending to the implementation verification. Although model checking can be used for both protocols and implementations, it is incomplete and does not scale.
In this paper, the authors present IronFleet, the first methodology for automated machine-checked verification of the safety and liveness. IronFleet ensures that the implementation of a distributed system meets a high-level specification. Furthermore, it supports complex, feature-rich implementations with reasonable performance and a tolerable proof burden. To comprehensively verify a complex distributed systems, the authors design several essential building blocks for IronFleet: (1) a methodology for structuring and writing proofs about distributed systems, (2) a collection of generic verified libraries useful for implementing such systems. IronFleet uses TLA-style state-machine refinement to reason about protocol-level concurrency, ignoring implementation complexities. Then, it uses Floyd-Hoare-style imperative verification to reason about those complexities while ignoring concurrency. To demonstrate the effectiveness of IronFleet, the authors build two different distributed systems: (1) IronRSL, a Paxos-based replicated-state-machine library and (2) IronKV, a sharded key-value store, for verification testing.
- The authors show that it is possible to mechanically verify a practical distributed implementations with reasonable performance and a tolerable proof burden.
- The authors present IronFleet, the first verification framework for both safety and liveness, which combines TLA-style state-machine refinement with Floyd-Hoare logic verification.
- IronFleet provides the first machine-verified liveness proofs of non-trivial distributed systems.
- Apart from the design details of IronFleet, the authors also describe engineering disciplines and lessons for verifying distributed systems. They also build several verified libraries to help developers for common tasks, like packet parsing and marshaling, etc.
- IronFleet supports proving both safety and liveness properties of distributed system implementations. Especially for the liveness properties, IronFleet is the first system to verify liveness of a practical protocol as well as implementation.
- For the verification of safety properties, IronFleet verifies not just the protocols at the design level but also the actual imperative implementations that achieve good performance.
- By applying the IronFleet methodology, the system is sliced into specific layers, which makes verification of practical distributed system implementations feasible.
- Although IronFleet automatically finishes many low-level proof works, it still requires assistance from the developers.
- IronFleet is based on the assumption that the network does not tamper with packets. However, active attacks to modify packets in the wide-area network are feasible.