Reference. DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols
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.
Cite
Cited by (5)
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.
Cites 35 works (4 here)
With notes (4)
Finding Invariants of Distributed Systems: It’s a Small (Enough) World After All hanceFindingInvariantsDistributed
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.
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.
IronFleet: proving practical distributed systems correct hawblitzel-2015-ironfleet
External (31)
- First-order quantified separators (2020)
- Data-driven inference of representation invariants (2020)
- AFLNET: A greybox fuzzer for network protocols (2020)
- CLN2INV: Learning loop invariants with continuous logic networks (2020)
- Learning nonlinear loop invariants with gated continuous logic networks (2020)
- Quantified invariants via syntax-guided synthesis (2019)
- Inferring inductive invariants from phase structures (2019)
- Essentials of Blockchain Technology (2019)
- Loop-invgen: A loop invariant generator based on precondition inference (2019)
- Solving constrained Horn clauses using syntax and data (2018)
- Inferring and asserting distributed system invariants (2018)
- Programming and proving with distributed protocols (2018)
- Modularity for decidability of deductive verification with applications to distributed systems (2018)
- A data-driven CHC solver (2018)
- Counterexample-guided approach to finding numerical invariants (2017)
- Paxos made EPR: Decidable reasoning about distributed protocols (2017)
- HVLearn: Automated black-box analysis of hostname verification in SSL/TLS implementations (2017)
- Learning invariants using decision trees and implication counterexamples (2016)
- Chapar: Certified causally consistent distributed key-value stores (2016)
- Data-driven precondition inference with learned features (2016)
- Planning for change in a formal verification of the Raft consensus protocol (2016)
- Protocol state fuzzing of TLS implementations (2015)
- Verdi: A framework for implementing and formally verifying distributed systems (2015)
- Learning universally quantified invariants of linear data structures (2013)
- A data driven approach for algebraic loop invariants (2013)
- Byzantizing Paxos by refinement (2011)
- Automatically inferring quantified loop invariants by algorithmic learning from simple templates (2010)
- The Daikon system for dynamic detection of likely invariants (2007)
- Paxos made simple (2001)
- The part-time parliament (1998)
- An optimal algorithm for mutual exclusion in computer networks (1981)