Cruiser: Automatically Extracting Verified, High-Performance Implementations of Distributed Systems
As the complexity of our distributed systems and our reliance on those systems increase, it becomes ever more critical for those systems to be correct. While, in principle, formal verification can help rid such systems of bugs, existing verification approaches either require vast amounts of manual effort or are too abstract to be practical, by verifying high-level protocols or greatly inefficient implementations.
In this paper we present Cruiser, the first approach that can produce high-performance, fully verified distributed system implementations, while relying on very little manual effort. Cruiser automatically extracts a high-performance implementation from a high-level protocol description and produces a proof that the implementation refines the protocol. We have used Cruiser to produce verified implementations of a number of distributed systems, including a Paxos-based replication library and our experiments show that these implementations perform competitively to hand-written implementations of the same systems.
Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems
Distributed systems are hard to design and implement correctly. Recent work has tried to use formal verification techniques to provide rigorous correctness guarantees. These works present a hard choice, though. One must either opt for the power of refinement-based approaches like IronFleet and Verdi, at the cost of large amounts of manual effort; or choose the more
automated approach of I4, IC3PO, SWISS and DistAI which give up the ability to prove refinement and the power and scalability that come with it.
We propose an alternative approach, Sift, that combines the power of refinement with the ability to automate proofs. Sift is a two-tier methodology that uses a new technique, refinement-guided automation, to leverage automation in a refinement proof and a divide-and-conquer technique to split a system into more refinement layers when necessary. This combination advances the frontier of what systems can be proven correct using a high degree of automation. Contrary to what was possible before, our evaluation shows that our novel approach allows us to prove the correctness of a number of systems with little manual effort, and to extend our proofs to include not just the protocols, but also an executable distributed implementation of these systems.
I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols
Designing and implementing distributed systems correctly is a very challenging task. Formal verification has been successfully used to prove the correctness of distributed systems. At the heart of formal verification lies a computer-checked proof with an inductive invariant. Finding this inductive invariant, however, is the most difficult part of the proof. Alas, current proof techniques require inductive invariants to be found manually—and painstakingly—by the developer. In this project we propose a new approach, Incremental Inference of Inductive Invariants (I4), to automatically generate inductive invariants for distributed protocols. The essence of our idea is simple: the inductive invariant of a finite instance of the protocol can be used to infer a general inductive invariant for the infinite distributed protocol. In I4, we create a finite instance of the protocol; use a model checking tool to automatically derive the inductive invariant for this finite instance; and generalize this invariant to an inductive invariant for the infinite protocol. Our experiments show that I4 can prove the correctness of several distributed protocols like Chord, 2PC, and Transaction Chains with little to no human effort.