SMT-driven techniques for verifying distributed systems

Abstract

Distributed systems, that is, networks of real or virtual components that collaborate in solving an algorithmic task underpin many of our modern technologies. The correctness of these systems is often critical; unpredictable system behavior can, in the worst cases, result in major financial loss, confidential data breaches, or even physical harm. Because of this, formal verification of these systems has been an active area of research for many decades. With the advent of cloud services and cryptocurrencies, there has also been an increase in demand, for newer, better, and more robust verification techniques. The primary contribution of this thesis is a set of techniques for designing a symbolic model checker for TLA+, with which one can verify properties of distributed algorithms. We focus particularly on specifications of distributed algorithms, as the use of TLA+ has recently been seeing rapid growth in the development of distributed systems. Specifically, we: 1. Formalize the notion of a symbolic transition, an equivalence class of transitions in the state-space defined by an algorithm specification. This is both a necessary prerequisite for symbolic verification, as well as a finite abstraction, reducing a potentially infinite number of real transitions, to a finite family of symbolic ones. 2. Define an encoding of constructs in the kernel of TLA+ to first-order logic, suitable for SMT solvers. This allows us to symbolically encode a bounded execution of the algorithm specification, and the properties we wish to verify, as an SMT formula, which can be passed to an off-the-shelf SMT solver. 3. Design a type system for TLA+, as well as a technique for automatic type inference. Types are both necessary, to bridge the gap between conventionally untyped TLA+ and typed SMT, and helpful, because algorithm designers are typically familiar with types and their uses in programming languages, and many errors, especially in the incremental design of an algorithm, can already be caught by type analysis.