Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols

Distributed protocols are challenging to design correctly. One promising approach to improve their reliability uses formal verification to prove that a protocol satisfies a desired safety property. These proofs require finding an inductive invariant that holds initially, implies safety, and is inductive. Devising an inductive invariant is a difficult task that prior work has either automated by requiring the protocol to be expressed in a decidable but restrictive fragment of logic, or required the developer to find by a painful search process.

In this work we aim to automatically find inductive invariants without restricting the logic. We do so using two key insights. Our first insight is that many of the complex inter-host properties that prior work required the developer to provide can instead be derived using Provenance Invariants, a class of invariants that relate a local variable in a host to its provenance, i.e., the protocol step that caused it to have its current value. By tracing the provenance of one host variable back to another host, we can derive an invariant relating the two hosts' states. Second, we develop an algorithm called Atomic Sharding to derive Provenance Invariants automatically by statically analyzing the protocol's steps.

We implement these ideas in a tool called Basilisk and apply it to 16 distributed protocols. Basilisk automatically finds a set of invariants and proves their inductiveness, with little or no developer assistance. In all cases, these generated invariants are sufficient for us to prove safety without needing to identify any new inductive invariants.