Reference. I4: Incremental inference of inductive invariants for verification of distributed protocols

Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, Karem A. Sakallah · SOSP · 2019 · distributed-systems inductive-invariants · DOI
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.

Cite
Cite as @maI4IncrementalInference2019 (helia, typst) · \cite{maI4IncrementalInference2019} (LaTeX)
BibTeX
bibtex · 17 lines
@inproceedings{maI4IncrementalInference2019,
 title = {I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols},
 author = {Ma, Haojun and Goel, Aman and Jeannin, Jean-Baptiste and Kapritsos, Manos and Kasikci, Baris and Sakallah, Karem A.},
 date = {2019-10-27},
 isbn = {978-1-4503-6873-5},
 doi = {10.1145/3341301.3359651},
 url = {https://dl.acm.org/doi/10.1145/3341301.3359651},
 urldate = {2023-01-10},
 booktitle = {Proceedings of the 27th {{ACM Symposium}} on {{Operating Systems Principles}}},
 pages = {370--384},
 publisher = {ACM},
 langid = {english},
 eventtitle = {{{SOSP}} '19: {{ACM SIGOPS}} 27th {{Symposium}} on {{Operating Systems Principles}}},
 abstract = {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.},
 location = {Huntsville Ontario Canada},
 shorttitle = {I4}
}
hayagriva YAML (typst)
yaml · 30 lines
maI4IncrementalInference2019:
  type: article
  title:
    value: 'I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols'
    short: I4
  author:
  - Ma, Haojun
  - Goel, Aman
  - Jeannin, Jean-Baptiste
  - Kapritsos, Manos
  - Kasikci, Baris
  - Sakallah, Karem A.
  date: 2019-10-27
  page-range: 370-384
  url:
    value: https://dl.acm.org/doi/10.1145/3341301.3359651
    date: 2023-01-10
  serial-number:
    doi: 10.1145/3341301.3359651
    isbn: 978-1-4503-6873-5
  language: en-US
  abstract: '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.'
  parent:
  - type: proceedings
    title: Proceedings of the 27th {ACM Symposium} on {Operating Systems Principles}
    publisher:
      name: ACM
      location: Huntsville Ontario Canada
  - type: conference
    title: '{SOSP} ''19: {ACM SIGOPS} 27th {Symposium} on {Operating Systems Principles}'
Download: maI4IncrementalInference2019.bib · maI4IncrementalInference2019.yml

Backlinks
Cited by (12)

TäKōFormal: Enabling Robust Software for Programmable Memory Hierarchies srinivasan-2026-takoformalISCA · 2026
DOI · arXiv

Verus: A Practical Foundation for Systems Verification lattuada-2024-verusSOSP · 2024
DOI

SAT-based quantified symmetric minimization of the reachable states of distributed protocols: An update LuoSatBasedQuantifiedSymmetricISoLA · 2024
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.
DOI

Formally verified asymptotic consensus in robust networks tekriwal-2024-formallyTACAS · 2024
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.
PDF · DOI · pldb

Grove: A Separation-Logic Library for Verifying Distributed Systems sharmaGroveSeparationLogicLibrary2023SOSP · 2023
Grove is a concurrent separation logic library for verifying distributed systems. Grove is the first to handle time-based leases, including their interaction with reconfiguration, crash recovery, thread-level concurrency, and unreliable networks. This paper uses Grove to verify several distributed system components written in Go, including vKV, a realistic distributed multi-threaded key-value store. vKV supports reconfiguration, primary/backup replication, and crash recovery, and uses leases to execute read-only requests on any replica. vKV achieves high performance (67–73% of Redis on a single core), scales with more cores and more backup replicas (achieving about 2× the throughput when going from 1 to 3 servers), and can safely execute reads while reconfiguring.
DOI

Performal: Formal Verification of Latency Properties for Distributed Systems zhang-2023-performalPLDI · 2023
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.
PDF · DOI · pldb

Regularity and Quantification: A New Approach to Verify Distributed Protocols goelRegularityQuantificationNewInnovations in Systems and Software Engineering · 2022
Proving that an unbounded distributed protocol satisfies a given safety property amounts to finding a quantified inductive invariant that implies the property for all possible instance sizes of the protocol. Existing methods for solving this problem can be described as search procedures for an invariant whose quantification prefix fits a particular template. We propose an alternative constructive approach that does not prescribe, a priori, a specific quantifier prefix. Instead, the required prefix is automatically inferred without any enumerative search by carefully analyzing the spatial and temporal regularity of the protocol. The key insight underlying this approach is that structural regularity and quantification are closely related concepts that express protocol invariance under different re-arrangements of its components and its unbounded evolution over time. We extended the finite-domain IC3/PDR algorithm to use these regularities and boost clause learning to automatically derive the required quantified inductive invariant by exploiting the connection between structural regularities and quantification. We also describe a procedure to automatically find a minimal finite size, the cutoff, that yields a quantified invariant proving safety for any size. Our approach is implemented in IC3PO, a new verifier for distributed protocols that significantly outperforms the state-of-the-art, scales orders of magnitude faster, and robustly derives compact inductive invariants fully automatically.
DOI

Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems maSiftUsingRefinementguidedUSENIX ATC · 2022
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.
Web

On Symmetry and Quantification: A New Approach to Verify Distributed Protocols goelSymmetryQuantificationNew2021NFM · 2021
Proving that an unbounded distributed protocol satisfies a given safety property amounts to finding a quantified inductive invariant that implies the property for all possible instance sizes of the protocol. Existing methods for solving this problem can be described as search procedures for an invariant whose quantification prefix fits a particular template. We propose an alternative constructive approach that does not prescribe, a priori, a specific quantifier prefix. Instead, the required prefix is automatically inferred without any search by carefully analyzing the structural symmetries of the protocol. The key insight underlying this approach is that symmetry and quantification are closely related concepts that express protocol invariance under different re-arrangements of its components. We propose symmetric incremental induction, an extension of the finite-domain IC3/PDR algorithm, that automatically derives the required quantified inductive invariant by exploiting the connection between symmetry and quantification. While various attempts have been made to exploit symmetry in verification applications, to our knowledge, this is the first demonstration of a direct link between symmetry and quantification in the context of clause learning during incremental induction. We also describe a procedure to automatically find a minimal finite size, the cutoff, that yields a quantified invariant proving safety for any size. Our approach is implemented in IC3PO, a new verifier for distributed protocols that significantly outperforms the state-of-the-art, scales orders of magnitude faster, and robustly derives compact inductive invariants fully automatically.
DOI · arXiv

Finding Invariants of Distributed Systems: It’s a Small (Enough) World After All hanceFindingInvariantsDistributedNSDI · 2021
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.
Web

DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols yaoDistAIDataDrivenAutomatedOSDI · 2021
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.
Web

AVR: Abstractly Verifying Reachability goelAVRAbstractlyVerifying2020TACAS · 2020
We present AVR, a push-button model checker for verifying state transition systems directly at the source-code level. AVR uses information embedded in the word-level syntax of the design representation to automatically perform scalable model checking by combining a novel syntax-guided abstraction-refinement technique with a word-level implementation of the IC3 algorithm. AVR provides independently-verifiable certificates that offer provable assurance and are easy to relate to the word-level system. Moreover, proof certificates can be further used in innovative ways to extract key design information and are useful in a growing number of applications.
PDF · DOI · pldb
Cites 57 works (3 here)
With notes (3)

Ivy: Safety verification by interactive generalization padonIvySafetyVerificationPLDI · 2016
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.
PDF · DOI · pldb

IronFleet: proving practical distributed systems correct hawblitzel-2015-ironfleetSOSP · 2015
DOI

SAT-Based Model Checking without Unrolling bradleySATBasedModelChecking2011VMCAI · 2011
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.
DOI · pldb
External (54)
maI4IncrementalInference2019 reference entries/refs/maI4IncrementalInference2019/maI4IncrementalInference2019.hel