CS 371D – Distributed Computing

Spring 2024

Distributed protocols are at the foundation of modern cloud computing services but are notoriously difficult to define and implement correctly. In this class, we will survey some important methods and concepts in distributed computing, including logical clocks, consistency models, fault tolerance, consensus, sharding, peer-to-peer protocols, cache coherence and distributed transactions, as well as important systems applying these ideas. The class will be divided roughly into one half theory and one half practical application.

An overview of the concepts covered in the class can be found in the introductory slides from Spring 2023.

The class will consist of lecture and a series of lab assignments. The labs are protocol design and implementation exercises that build from simple replicated stores to a scalable fault-tolerant system using distributed consensus. The labs will be implemented in Java. We will test our systems in a simulated distributed environment and use model checking, a technique of systematic state space exploration, to help us find subtle concurrency bugs that are difficult to find by testing alone. Grading will be based on the labs. There will be no final exam.

CS 395T: The Model Checking Paradigm

Spring 2021

Course Description

Model checking and related techniques of automatic formal verification emerged in the early 1980’s. These methods present a cost and a benefit: we must model our system and write our specification in very restricted forms, but in exchange for this we obtain proofs and counterexamples automatically. Despite early successes, this approach immediately led to difficult problems, for example, how to extend the expressiveness of the models to allow the verification of real systems, while keeping the proofs tractable. The model checking paradigm is the collection of strategies that researchers developed for resolving these problems.

The class will survey a sampling of research topics within the model checking paradigm, with a view to elucidating the high-level strategies, while disregarding algorithmic details. In this way, we will try to make some sense of the diverse and not always coherent literature in the field. The goal is for students to be able to read critically and put into context recent papers in areas such as software model checking, cyber-physical systems or neural network verification.

Modularity for decidability of deductive verification with applications to distributed systems

Proof automation can substantially increase productivity in formal verification of complex systems. However, unpredictablility of automated provers in handling quantified formulas presents a major hurdle to usability of these tools. We propose to solve this problem not by improving the provers, but by using a modular proof methodology that allows us to produce decidable verification conditions. Decidability greatly improves predictability of proof automation, resulting in a more practical verification approach. We apply this methodology to develop verified implementations of distributed protocols, demonstrating its effectiveness.

Paper

Modularity for decidability of deductive verification with applications to distributed systems (Marcelo Taube and Giuliano Losa and Kenneth L. McMillan and Oded Padon and Mooly Sagiv and Sharon Shoham and James R. Wilcox and Doug Woos), In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, 2018. [bibtex] [pdf] [doi]

Duality

Duality is a solver for Constrained Horn Clauses based on Craig Interpolation and Lazy Annotation. A CHC solver can be used for many purposes, including the verification of recursive programs.

Lazy Annotation is a method of software model checking that performs a backtracking search for a symbolic counterexample. When the search backtracks, the program is annotated with a learned fact, derived as a Craig interpolant, that constrains future search. In this sense, the method is closely analogous to conflict-driven clause learning in SAT solvers.

Getting Duality

Duality was integrated as a Horn Logic solver in the Z3 theorem prover up to version 4.7.1. Releases of Z3 containing Duality can be obtained from the Z3 Github site. To use Duality for a Horn logic problem in the SMTLIB2 format, use the Z3 command-line option engine=duality.

Paper

Lazy Annotation Revisited (Kenneth L. McMillan), In Computer Aided Verification – 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, 2014. [bibtex] [pdf] [doi]

Formal specification and testing of QUIC

QUIC is a new Internet secure transport protocol currently
in the process of IETF standardization. It is intended as a
replacement for the TLS/TCP stack and will be the basis of
HTTP/3, the next official version of the hypertext transfer
protocol. As a result, it is likely, in the near future, to carry
a substantial fraction of traffic on the Internet. We describe
our experience applying a methodology of compositional
specification-based testing to QUIC. We develop a formal
specification of the wire protocol, and use this specification
to generate automated randomized testers for implementations of QUIC. The testers effectively take one role of the
QUIC protocol, interacting with the other role to generate
full protocol executions, and verifying that the implementations conform to the formal specification. This form of testing
generates significantly more diverse stimuli and stronger correctness criteria than interoperability testing, the primary
method used to date to validate QUIC and its implementations. As a result, numerous implementation errors have
been found. These include some vulnerabilities at the protocol and implementation levels, such as an off-path denial
of service scenario and an information leak similar to the
“heartbleed” vulnerability in OpenSSL. TEST

Paper

Formal specification and testing of QUIC (Kenneth L. McMillan and Lenore D. Zuck), In Proceedings of ACM Special Interest Group on Data Communication (SIGCOMM’19), ACM, 2019. [bibtex] [pdf] [slides] video

Interpolating Z3

A Craig interpolant is a formula that acts as an explanation for the unsatisfiability of a logical formula. Interpolating Z3 (iZ3) is a version of the Z3 theorem prover that can produce Craig interpolants from proofs. To be more specific, suppose “A” and “B” are logical formulas and we can prove “A implies B”. An interpolant for this implication is a formula I expressed only using symbols that are common to A and B that makes the following formulas valid:

“A implies I”
“I implies B”

The power of interpolants is that they put a proof in a syntactic form that allows it to be generalized. This ability can be applied, for example, to extract proofs about sequential circuits or programs from proofs about specific execution sequences, or to derive abstractions from counterexamples.

Capabilities of iZ3

iZ3 can derive Craig interpolants from proofs in first-order logic, modulo certain theories, including:

Integer linear arithmetic
The theory of arrays

iZ3 handles quantified formulas, but does not always produce a quantifier-free interpolant when a quantifier-free interpolant exists. iZ3 can also produce sequence interpolants and tree interpolants, which are useful for program verification and constraint Horn clause (CHC) solving, as in the Duality CHC solver.

For more information on using iZ3, see the iZ3 tutorial.

Obtaining iZ3

iZ3 was a part of Z3 up to version 4.7.1. Releases including iZ3 can be downloaded from the Z3 github repository. However iZ3 is not maintained in current releases of Z3.

Papers

The following paper describes an older version of iZ3 that used a method of decomposing Z3 proofs into lemmas and applying the FOCI interpolating prover to these lemmas. The current version constructs interpolants directly from Z3 proofs.

Interpolants from Z3 proofs (Kenneth L. McMillan), In International Conference on Formal Methods in Computer-Aided Design, FMCAD ’11, Austin, TX, USA, October 30 – November 02, 2011, 2011. [bibtex] [pdf]

Ivy

IVy is a tool for specifying, modeling, implementing and verifying protcols. IVy is intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.

IVy has two primary design goals: to be as transparent as possible, and to produce design artifacts that are useful even to engineers who may lack the skills or resources needed to construct formal proofs.

Transparency

The research community has developed many impressive automated tools for formal proof. For example, SMT solvers such as Microsoft’s Z3 can check the validity of formulas in various logics and can even generate inductive invariants. Because these tools are heuristic in nature, however, they fail in ways that are unpredictable and often not understandable by a human user. To reduce this problem, Ivy relies on interactive visualization, decidable logics and modularity

Interactive visualization

Ivy constructs inductive invariants interactively, using visualization techniques. When there is a problem in the proof, it searches for a simple scenario to explain the problem and displays it graphically, highlighting possibly relevant facts. Users can combine their intuition with automated generalization techniques to refine the proof. This approach can greatly reduce the human time needed to construct a proof.

Decidable logics and modularity

A logic is decidable if there is a algorithm that can determine the truth of any formula. In practice, using decidable logics makes proof automation more reliable and repeatable. It also makes it possible to give transparent explanations of proof failures.

IVy’s language is designed to make it practical to reduce all proof obligations to statements in decidable logics. It provides primitives to support modeling in decidable logics, and also modular refinement techniques the makes it possible to separate the verification effort into local, decidable problems. For example, we can verify a protocol at a high level assuming that a given abstract type is totally ordered, then implement that abstract type using bit vectors or integers.

Design artifacts

Another key focus of Ivy is to produce composable specifications that can be used as a reference by designers and for rigorous testing of designs. Ivy supports specifications that are both composable and temporal. This means that if all components locally satisfy their specifications, we know that the system as a whole correctly implements its high-level semantics. Moreover, each component’s specification can be used independently to test and verify that component.

From composable specifications, Ivy can generate test benches and tests oracles that can be used to test design components rigorously against their specifications. Such testers can reveal latent bugs in component implementations that do not appear in integration tests or ad-hoc unit testing.

Getting Ivy

Ivy is an open source tool. For more information on Ivy, see the Ivy github repository and the Ivy web site.

Papers

Deductive Verification in Decidable Fragments with Ivy (Kenneth L. McMillan and Oded Padon), In Static Analysis – 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings (Andreas Podelski, ed.), Springer, volume 11002, 2018. [bibtex] [pdf] [doi]

Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems (Oded Padon and Jochen Hoenicke and Kenneth L. McMillan and Andreas Podelski and Mooly Sagiv and Sharon Shoham), In 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 – November 2, 2018 (Nikolaj Bjørner, Arie Gurfinkel, eds.), IEEE, 2018. [bibtex] [pdf] [doi]

Ivy: safety verification by interactive generalization (Oded Padon and Kenneth L. McMillan and Aurojit Panda and Mooly Sagiv and Sharon Shoham), In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, 2016. [bibtex] [pdf] [doi]

Modular specification and verification of a cache-coherent interface (Kenneth L. McMillan), In 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, October 3-6, 2016, 2016. [bibtex] [pdf] [doi]