PRAVDA - Parametrized Verification of Fault-tolerant Distributed Algorithms

In the design of reliable computer systems, one has to address two challenges: on the one hand, we have to design means that tolerate partial failure that is outside the control of a system designer (e.g., power outages), and on the other hand, find design faults (bugs) in order to fix them. The former is addressed by means of replication and fault-tolerant distributed algorithms (FTDAs), while the latter is dealt with by rigorous system and software engineering methods, such as model checking. These two challenges have been studied by disjoint research communities. The distributed algorithm community has created a wealth of interesting FTDAs. While in the past these FTDAs were implemented only in safety-critical systems, we currently see more and more implementations of FTDAs for other application domains. The more implementations we will see, the more important it becomes to have effective methods to verify that these algorithms actually perform the task they were designed for. The classic approach to ascertain the correctness of FTDAs is paper-and-pencil proofs. Conducting such proofs is an error-prone task, because the reasoning required is actually quite different from arguments in mainstream computer science. As a result, even published distributed algorithms contain bugs. It is therefore questionable whether FTDAs that are designed to increase to reliability of computer systems actually reach this goal. Hence, we require additional means to increase the trust in the correctness of FTDAs. This project explores model checking for this purpose, because model checking promises a high degree and automation, and has been used successfully for software and hardware verification. In particular this project considers the issue of parametrization in FTDAs. FTDAs are classically parametrized by the number of processes n and the assumed maximal number of faults t, using resilience conditions that require, for instance, that a majority of the processes is correct, which is formalized using expressions such as n > 2t. This leads to the verification problem that a given FTDA should be verified for all combinations of n and t satisfying n > 2t, that is, an infinite family of system instances with fixed n and t has to be verified. The verification community has considered similar problems in the research area of parametrized model checking. Parametrized model checking is still considered a field that is full of open research questions. In particular, FTDAs have several features that introduce challenges that have not been considered in the literature so far, such as, the mentioned resilience conditions, process code that uses the parameters, faults, intricate timing assumptions, etc. Within the PRAVDA project, we will develop new parametrized model checking methods, that will allow us to ascertain the correctness of state-of-the-art FTDAs.

In the design of reliable computer systems, one has to address two challenges: on the one hand, we have to design means that tolerate partial failure that is outside the control of a system designer (e.g., power outages, or parts of a network being disconnected), and on the other hand, find design flaws (bugs) in order to fix them. The former is addressed by means of replication and fault-tolerant distributed algorithms (FTDAs), while the latter is dealt with by rigorous system and software engineering methods, such as model checking. While in the past these FTDAs were implemented only in safety-critical systems, we currently see more and more implementations of FTDAs for other application domains. The classic approach to ascertain the correctness of FTDAs is paper-and-pencil proofs. Conducting such proofs is an error-prone task, because the reasoning required is actually quite different from arguments in mainstream computer science. As a result, even published distributed algorithms contain bugs. It is therefore questionable whether FTDAs that are designed to increase the reliability of computer systems actually reach this goal. Hence, we require additional means to increase the trust in the correctness of FTDAs. The PRAVDA project developed new automated verification techniques for this purpose, e.g., new parameterized model checking or deductive verification methods. These methods promise a higher degree and automation, and are less error-prone than the classic approach. We made significant progress both towards automated verification of high-level protocols as well as towards deductive verification of code. While classic automated verification techniques focus on safety properties (nothing bad ever happens), fault-tolerant distributed algorithms motivated us to specifically also look into liveness properties (eventually something good happens). Another focus was to better understand the relationship between asynchronous semantics (that capture how a system behaves in reality) and synchronous semantics (that are more abstract and simpler to reason in). We adapted classic notions of reductions to the specifics of FTDAs, which allowed us to make several breakthroughs for their verification. In parallel, and out of scope of the PRAVDA proposal, proof-of-stake blockchain projects, such as Tendermint or Facebook's Libra, implemented Byzantine fault-tolerant distributed algorithms for the large scale, that is, for hundreds of participating processes. For such large systems, parameterized verification methods provide, in principle, a solid basis to ascertain the correctness of the systems. Indeed, given the amount of money that is managed in such blockchain systems, the automated verification of fault-tolerant distributed systems suddenly finds itself in the mainstream of computer science. Although the gap between verification of high-level protocols and implementations is still considerable (and warrants more research in this area), the research of PRAVDA builds a solid basis.