Verification of the Chord protocol in TLA+

Abstract

In traditional software engineering methodologies, software correctness is established through testing and progressive fault mitigation. Safety properties are established by demonstrating that a sufficiently large number of test cases fail to violate them.

In contrast, formal verification methods permit a systems design process where desired safety properties are stated outright in the system specification, and enforced by automated analysis tools. This is of particular interest in designing distributed systems, where safety properties may be easy to formally define and specify, yet hard to implement in practice.

Despite this promise, the use of formal methods has largely been confined to academia and certain classes of safety-critical systems. Recently, however, companies like Amazon and Microsoft have adopted formal verification tools to verify distributed system designs. In this thesis, we present a formal specification of the Chord distributed hash table protocol, using the TLA+ specification language. We specify the protocol at a coarse level with a relaxed failure model, and then increase the granularity and introduce fail-stop failures, yielding a formal specification of Chord with asynchronous messaging and fault-tolerance mechanisms.

We first model-check the specification under the constraint that no failures occur, and show that it satisfies critical safety properties. We then show that the introduction of failures leads the specification to admit several behaviors which break the safety properties Chord promises, potentially leading to permanent partitions in the network and performance degradation.

As part of this work, we provide an overview of formal verification methods; we discuss certain formalisms and logics involved in modelling and proving algorithms, show potential advantages of applying formal methods to distributed systems design, and identify barriers keeping formal methods from widespread use.