Reference. Finding Invariants of Distributed Systems: It’s a Small (Enough) World After All
Today’s distributed systems are increasingly complex, leading to subtle bugs that are difficult to detect with standard testing methods. Formal verification can provably rule out such bugs, but historically it has been excessively labor intensive. For distributed systems, recent work shows that, given a correct inductive invariant, nearly all other proof work can be automated; however, the construction of such invariants is still a difficult manual task. In this paper, we demonstrate a new methodology for automating the construction of inductive invariants, given as input a (formal) description of the distributed system and a desired safety condition. Our system performs an exhaustive search within a given space of candidate invariants in order to find and verify inductive invariants which suffice to prove the safety condition. Central to our ability to search efficiently is our algorithm’s ability to learn from counterexamples whenever a candidate fails to be invariant, allowing us to check the remaining candidates more efficiently. We hypothesize that many distributed systems, even complex ones, may have concise invariants that make this approach practical, and in support of this, we show that our system is able to identify and verify inductive invariants for the Paxos protocol, which proved too complex for previous work.
Cite
Cited by (6)
Verus: A Practical Foundation for Systems Verification lattuada-2024-verus
SAT-based quantified symmetric minimization of the reachable states of distributed protocols: An update LuoSatBasedQuantifiedSymmetric
In prior work [13], we introduced a procedure for deriving minimum formulas in first-order logic (FOL) for the reachable states of a restricted class of multi-sorted distributed protocol specifications: protocols with sorts representing unbounded sets of symmetric (indistinguishable) elements. This paper provides a deeper analysis of this idea that yields additional insights about the oft-cited observation that the behavior of such protocols can be inferred from analyzing relatively small finite instances whereby a protocol’s behavior becomes invariant, i.e. saturates [24], beyond certain cutoff sizes of its sorts. The paper discusses several issues in previous work [13] and provides more succinct FOL formulas of the reachable states for a collection of common protocols.
Formally verified asymptotic consensus in robust networks tekriwal-2024-formally
Distributed architectures are used to improve performance and reliability of various systems. Examples include drone swarms and load-balancing servers. An important capability of a distributed architecture is the ability to reach consensus among all its nodes. Several consensus algorithms have been proposed, and many of these algorithms come with intricate proofs of correctness, that are not mechanically checked. In the controls community, algorithms often achieve consensus asymptotically , e.g., for problems such as the design of human control systems, or the analysis of natural systems like bird flocking. This is in contrast to exact consensus algorithm such as Paxos, which have received much more recent attention in the formal methods community. This paper presents the first formal proof of an asymptotic consensus algorithm, and addresses various challenges in its formalization. Using the Coq proof assistant, we verify the correctness of a widely used consensus algorithm in the distributed controls community, the Weighted-Mean Subsequence Reduced (W-MSR) algorithm . We formalize the necessary and sufficient conditions required to achieve resilient asymptotic consensus under the assumed attacker model. During the formalization, we clarify several imprecisions in the paper proof, including an imprecision on quantifiers in the main theorem.
Performal: Formal Verification of Latency Properties for Distributed Systems zhang-2023-performal
Understanding and debugging the performance of distributed systems is a notoriously hard task, but a critical one. Traditional techniques like logging, tracing, and benchmarking represent a best-effort way to find performance bugs, but they either require a full deployment to be effective or can only find bugs after they manifest. Even with such techniques in place, real deployments often exhibit performance bugs that cause unwanted behavior. In this paper, we present Performal, a novel methodology that leverages the recent advances in formal verification to provide rigorous latency guarantees for real, complex distributed systems. The task is not an easy one: it requires carefully decoupling the formal proofs from the execution environment, formally defining latency properties, and proving them on real, distributed implementations. We used Performal to prove rigorous upper bounds for the latency of three applications: a distributed lock, ZooKeeper and a MultiPaxos-based State Machine Replication system. Our experimental evaluation shows that these bounds are a good proxy for the behavior of the deployed system and can be used to identify performance bugs in real-world systems.
Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems maSiftUsingRefinementguided
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.
DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols yaoDistAIDataDrivenAutomated
Distributed systems are notoriously hard to implement correctly due to non-determinism. Finding the inductive invariant of the distributed protocol is a critical step in verifying the correctness of distributed systems, but takes a long time to do even for simple protocols. We present DistAI, a data-driven automated system for learning inductive invariants for distributed protocols. DistAI generates data by simulating the distributed protocol at different instance sizes and recording states as samples. Based on the observation that invariants are often concise in practice, DistAI starts with small invariant formulas and enumerates all strongest possible invariants that hold for all samples. It then feeds those invariants and the desired safety properties to an SMT solver to check if the conjunction of the invariants and the safety properties is inductive. Starting with small invariant formulas and strongest possible invariants avoids large SMT queries, improving SMT solver performance. Because DistAI starts with the strongest possible invariants, if the SMT solver fails, DistAI does not need to discard failed invariants, but knows to monotonically weaken them and try again with the solver, repeating the process until it eventually succeeds. We prove that DistAI is guaranteed to find the ∃-free inductive invariant that proves the desired safety properties in finite time, if one exists. Our evaluation shows that DistAI successfully verifies 13 common distributed protocols automatically and outperforms alternative methods both in the number of protocols it verifies and the speed at which it does so, in some cases by more than two orders of magnitude.
Cites 54 works (4 here)
With notes (4)
I4: Incremental inference of inductive invariants for verification of distributed protocols maI4IncrementalInference2019
Designing and implementing distributed systems correctly is a very challenging task. Recently, formal verification has been successfully used to prove the correctness of distributed systems. At the heart of formal verification lies a computerchecked 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 paper, we present 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.
Ivy: Safety verification by interactive generalization padonIvySafetyVerification
Despite several decades of research, the problem of formal verification of infinite-state systems has resisted effective automation. We describe a system — Ivy — for interactively verifying safety of infinite-state systems. Ivy’s key principle is that whenever verification fails, Ivy graphically displays a concrete counterexample to induction. The user then interactively guides generalization from this counterexample. This process continues until an inductive invariant is found. Ivy searches for universally quantified invariants, and uses a restricted modeling language. This ensures that all verification conditions can be checked algorithmically. All user interactions are performed using graphical models, easing the user’s task. We describe our initial experience with verifying several distributed protocols.
Decidability of inferring inductive invariants padonDecidabilityInferringInductive2016
Induction is a successful approach for verification of hardware and software systems. A common practice is to model a system using logical formulas, and then use a decision procedure to verify that some logical formula is an inductive safety invariant for the system. A key ingredient in this approach is coming up with the inductive invariant, which is known as invariant inference. This is a major difficulty, and it is often left for humans or addressed by sound but incomplete abstract interpretation. This paper is motivated by the problem of inductive invariants in shape analysis and in distributed protocols. This paper approaches the general problem of inferring first-order inductive invariants by restricting the language L of candidate invariants. Notice that the problem of invariant inference in a restricted language L differs from the safety problem, since a system may be safe and still not have any inductive invariant in L that proves safety. Clearly, if L is finite (and if testing an inductive invariant is decidable), then inferring invariants in L is decidable. This paper presents some interesting cases when inferring inductive invariants in L is decidable even when L is an infinite language of universal formulas. Decidability is obtained by restricting L and defining a suitable well-quasi-order on the state space. We also present some undecidability results that show that our restrictions are necessary. We further present a framework for systematically constructing infinite languages while keeping the invariant inference problem decidable. We illustrate our approach by showing the decidability of inferring invariants for programs manipulating linked-lists, and for distributed protocols.
SAT-Based Model Checking without Unrolling bradleySATBasedModelChecking2011
A new form of SAT-based symbolic model checking is described. Instead of unrolling the transition relation, it incrementally generates clauses that are inductive relative to (and augment) stepwise approximate reachability information. In this way, the algorithm gradually refines the property, eventually producing either an inductive strengthening of the property or a counterexample trace. Our experimental studies show that induction is a powerful tool for generalizing the unreachability of given error states: it can refine away many states at once, and it is effective at focusing the proof search on aspects of the transition system relevant to the property. Furthermore, the incremental structure of the algorithm lends itself to a parallel implementation.
External (50)
- First-order quantified separators (2020)
- Code2Inv: A deep learning framework for program verification (2020)
- Learning nonlinear loop invariants with gated continuous logic networks (2020)
- Model checking of verilog RTL using IC3 with syntax-guided abstraction (2019)
- Pretend synchrony: Synchronous verification of asynchronous distributed programs (2019)
- Search-based program synthesis (2018)
- Horn-ICE learning for synthesizing invariants and contracts (2018)
- Learning loop invariants for program verification (2018)
- Synthesizing memory models from framework sketches and litmus tests (2017)
- IronFleet: Proving safety and liveness of practical distributed systems (2017)
- Cutoff bounds for consensus algorithms (2017)
- Counterexample-guided approach to finding numerical invariants (2017)
- Paxos made EPR: Decidable reasoning about distributed protocols (2017)
- PSync: A partially synchronous language for fault-tolerant distributed algorithms (2016)
- Learning invariants using decision trees and implication counterexamples (2016)
- Flexible Paxos: Quorum intersection revisited (2016)
- Planning for change in a formal verification of the raft consensus protocol (2016)
- A parallelizable approach for mining likely invariants (2015)
- How Amazon web services uses formal methods (2015)
- Verdi: A framework for implementing and formally verifying distributed systems (2015)
- A logic-based framework for verifying consensus algorithms (2014)
- ICE: A robust framework for learning invariants (2014)
- Developing correctly replicated databases using formal tools (2014)
- Developing correctly replicated databases using formal tools (2014)
- Finite model finding in SMT (2013)
- A data driven approach for algebraic loop invariants (2013)
- Efficient implementation of property directed reachability (2011)
- Byzantizing Paxos by refinement (2011)
- InvGen: An efficient invariant generator (2009)
- Model checking a Paxos implementation (2009)
- Vertical paxos and primary-backup replication (2009)
- MODIST: Transparent model checking of unmodified distributed systems (2009)
- Z3: An efficient SMT solver (2008)
- Quantified invariant generation using an interpolating saturation prover (2008)
- Deciding effectively propositional logic with equality (2008)
- The Farsite project: A retrospective (2007)
- The Farsite project: a retrospective (2007)
- The daikon system for dynamic detection of likely invariants (2007)
- Mace: Language support for building distributed systems (2007)
- Combinatorial sketching for finite programs (2006)
- An annotated specification of the consensus protocol of Paxos using superposition in PVS (2004)
- Linear invariant generation using non-linear constraint solving (2003)
- Checking cache-coherence protocols with TLA+ (2003)
- Using formal specifications to monitor and guide simulation: Verifying the cache coherence engine of the Alpha 21364 microprocessor (2002)
- The part-time parliament (1998)
- The temporal logic of actions (1994)
- Complexity results for classes of quantificational formulas (1980)
- Automatic discovery of linear restraints among variables of a program (1978)
- File searching using variable length keys (1959)
- The impossibility of an algorithm for the decidability problem on finite classes (1950)