Abstract We present a case study on proof-driven software understanding of mature, security-critical infrastructure. While formal methods are traditionally applied during the design phase, we present our experience applying formal reasoning onto a mature industrial C++ codebase. We focus on a formal analysis of the core algorithm that implements the Stellar blockchain’s order book. By combining large language models (LLMs), Prototype Verification System (PVS), and Seahorn , we are able to prove core properties of the production codebase. Our approach also identified an inconsistency in documentation related to the reachability of an exception location. Most importantly, however, we produce artifacts that make it easy for code changes to be checked against established invariants. This work demonstrates how the strategic combination of theorem proving and model checking provides a path for delivering robust assurance to legacy systems.

Reliable broadcast (RBC) is a key primitive in fault-tolerant distributed systems, and improving its efficiency can benefit a wide range of applications. This work focuses on signature-free RBC protocols, which are particularly attractive due to their computational efficiency. Existing protocols in this setting incur an optimal 3 steps to reach a decision while tolerating up to ƒ < n/3 Byzantine faults, where n is the number of parties. In this work, we propose an optimistic RBC protocol that maintains the ƒ < n/3 fault tolerance but achieves termination in just 2 steps under certain optimistic conditions—when at least ⌉n+2 ƒ-2 over -2 ⌈ non-broadcaster parties behave honestly. We also prove a matching lower bound on the number of honest parties required for 2-step termination.

This paper studies distributed-computing tasks through the lens of space complexity in the read/write wait-free model, defined as the number of multi-reader-multi-writer atomic read/write registers needed to solve a task using a wait-free algorithm. Surprisingly, even though the read/write wait-free model is at the foundation of distributed computing, previous work on space complexity has focused on synchronization primitives stronger than read/write registers or on weaker progress conditions. The paper reveals that the read/write wait-free model offers a rich space-complexity landscape: (1) assuming non-anonymous processes, it shows that there is an infinite hierarchy of tasks of increasing space complexity; (2) it shows that space complexity separates anonymous from non-anonymous memory; (3) regardless of process or register anonymity, it exhibits a task of space complexity two, which is the minimal non-trivial space complexity; (4) finally, it shows that subcases of the adopt-commit task have different space complexity in non-anonymous memory under bounded wait-freedom.

Delporte-Gallet et al. show that, in a system of n processes, it is both necessary and sufficient to use n multi-writer multi-reader (MWMR) registers, that are not pre-allocated, to emulate with non-blocking progress n single-writer multi-reader (SWMR) registers that are uniquely pre-allocated. They conclude with the significant result that n MWMR registers are sufficient to solve any task solvable read-write wait-free. However, they mistakenly claim—likely inadvertently—that n MWMR registers are also necessary to solve any task solvable read-write wait-free (a counterexample is the splitter task, which is solvable for any number of processes with just 2 MWMR registers).

Dynamically available total-order broadcast (TOB) protocols tolerate fluctuating participation, e.g., as high as 99% of their participants going offline, which is especially useful in permissionless blockchain environments. However, dynamically available TOB protocols are synchronous protocols, and they lose their safety guarantees during periods of asynchrony. This is a major issue in practice.

In the fully-anonymous (shared-memory) model, inspired by a biological setting, processors have no identifiers and memory locations are anonymous, meaning there is no pre-existing agreement among processors on any naming of the memory locations. In this work, we ask fundamental questions about the fully-anonymous model in the hope to obtain a better understanding of the role of naming and anonymity in distributed computing.

This paper presents TetraBFT, a novel unauthenticated Byzantine fault tolerant protocol for solving consensus in partial synchrony, eliminating the need for public key cryptography and ensuring resilience against computationally unbounded adversaries.

In a permissionless system like Ethereum, participation may fluctuate dynamically as some participants unpredictably go offline and some others come back online. In such an environment, traditional Byzantine fault-tolerant consensus algorithms may stall - even in the absence of failures - because they rely on the availability of fixed-sized quorums. The sleepy model formally captures the main requirements for solving consensus under dynamic participation, and several algorithms solve consensus with probabilistic safety in this model assuming that, at any time, more than half of the online participants are well behaved. However, whether safety can be ensured deterministically under these assumptions, especially with constant latency, remained an open question. Assuming a constant adversary, we answer in the positive by presenting a consensus algorithm that achieves deterministic safety and constant latency in expectation. In the full version of this paper, we also present a second algorithm which obtains both deterministic safety and liveness, but is likely only of theoretical interest because of its high round and message complexity. Both algorithms are striking in their simplicity.

Fail-prone systems, and their quorum systems, are useful tools for the design of distributed algorithms. However, fail-prone systems as studied so far require every process to know the full system membership in order to guarantee safety through globally intersecting quorums. Thus, they are of little help in an open, permissionless setting, where such knowledge may not be available. We propose to generalize the theory of fail-prone systems to make it applicable to permissionless systems. We do so by enabling processes not only to make assumptions about failures, but also to make assumptions about the assumptions of other processes. Thus, by transitivity, processes that do not even know of any common process may nevertheless have intersecting quorums and solve, for example, reliable broadcast. Our model generalizes existing models such as the classic fail-prone system model [Malkhi and Reiter, 1998] and the asymmetric fail-prone system model [Cachin and Tackmann, OPODIS 2019]. Moreover, it gives a characterization with standard formalism of the model used by the Stellar blockchain.

Contention plays a crucial role in the design of consensus protocols. State-of-the-art solutions optimize their performance for either very low or high contention situations. We proposeCaesar, a novel multi-leader Generalized Consensus protocol, most suitable for geographical replication, that is optimized for low-to-moderate contention. With an evaluation study, we show thatCaesaroutperforms other multi-leader (e.g., EPaxos) and single-leader (e.g., Multi-Paxos) competitors by up to 1.7x and 3.5x, respectively, in the presence of 30 percent conflicting requests, in a geo-replicated setting. Furthermore, we acknowledge that there is no one-size-fits- all consensus solution, especially for all levels of contentious workloads. Thus, we also proposeSpectrum, a consensus framework that is able to switch consensus protocols at runtime to enable a dynamic reaction to changes in the workload and deployment characteristics. We show empirically thatSpectrumcan guarantee high availability even during periods of transition between consensus protocols.

Verification of fault-tolerant distributed protocols is an immensely difficult task. Often, in these protocols, thresholds on set cardinalities are used both in the process code and in its correctness proof, e.g., a process can perform an action only if it has received an acknowledgment from at least half of its peers. Verification of threshold-based protocols is extremely challenging as it involves two kinds of reasoning: first-order reasoning about the unbounded state of the protocol, together with reasoning about sets and cardinalities. In this work, we develop a new methodology for decomposing the verification task of such protocols into two decidable logics: EPR and BAPA. Our key insight is that such protocols use thresholds in a restricted way as a means to obtain certain properties of “intersection” between sets. We define a language for expressing such properties, and present two translations: to EPR and BAPA. The EPR translation allows verifying the protocol while assuming these properties, and the BAPA translation allows verifying the correctness of the properties. We further develop an algorithm for automatically generating the properties needed for verifying a given protocol, facilitating fully automated deductive verification. Using this technique we have verified several challenging protocols, including Byzantine one-step consensus, hybrid reliable broadcast and fast Byzantine Paxos.

International payments are slow and expensive, in part because of multi-hop payment routing through heterogeneous banking systems. Stellar is a new global payment network that can directly transfer digital money anywhere in the world in seconds. The key innovation is a secure transaction mechanism across untrusted intermediaries, using a new Byzantine agreement protocol called SCP. With SCP, each institution specifies other institutions with which to remain in agreement; through the global interconnectedness of the financial system, the whole network then agrees on atomic transactions spanning arbitrary institutions, with no solvency or exchange-rate risk from intermediary asset issuers or market makers. We present SCP's model, protocol, and formal verification; describe the Stellar payment network; and finally evaluate Stellar empirically through benchmarks and our experience with several years of production use.

In a previous note (arXiv:1712.01367 [cs.DC]) , we observed a safety violation in Zyzzyva and a liveness violation in FaB. In this manuscript, we sketch fixes to both. The same view-change core is applied in the two schemes, and additionally, applied to combine them and create a single, enhanced scheme that has the benefits of both approaches.

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.

The consensus hierarchy classifies shared an object according to its consensus number, which is the maximum number of processes that can solve consensus wait-free using the object. The question of whether this hierarchy is precise enough to fully characterize the synchronization power of deterministic shared objects was open until 2016, when Afek et al. showed that there is an infinite hierarchy of deterministic objects, each weaker than the next, which is strictly between i and i+1-processors consensus, for i >= 2. For i=1, the question whether there exist a deterministic object whose power is strictly between read-write and 2-processors consensus, remained open. We resolve the question positively by exhibiting an infinite hierarchy of simple deterministic objects which are equivalent to set-consensus tasks, and thus are stronger than read-write registers, but they cannot implement consensus for two processes. Still our paper leaves a gap with open questions.

We develop a new technique for verifying temporal properties of infinite-state (distributed) systems. The main idea is to reduce the temporal verification problem to the problem of verifying the safety of infinite-state systems expressed in first-order logic. This allows to leverage existing techniques for safety verification to verify temporal properties of interesting distributed protocols, including some that have not been mechanically verified before. We model infinite-state systems using first-order logic, and use first-order temporal logic (FO-LTL) to specify temporal properties. This general formalism allows to naturally model distributed systems, while supporting both unbounded-parallelism (where the system is allowed to dynamically create processes), and infinite-state per process. The traditional approach for verifying temporal properties of infinite-state systems employs well-founded relations (e.g. using linear arithmetic ranking functions). In contrast, our approach is based the idea of fair cycle detection. In finite-state systems, temporal verification can always be reduced to fair cycle detection (a system contains a fair cycle if it revisits a state after satisfying all fairness constraints). However, with both infinitely many states and infinitely many fairness constraints, a straightforward reduction to fair cycle detection is unsound. To regain soundness, we augment the infinite-state transition system by a dynamically computed finite set, that exploits the locality of transitions. This set lets us define a form of fair cycle detection that is sound in the presence of both infinitely many states, and infinitely many fairness constraints. Our approach allows a new style of temporal verification that does not explicitly involve ranking functions. This fits well with pure first-order verification which does not explicitly reason about numerical values. In particular, it can be used with effectively propositional first-order logic (EPR), in which case checking verification conditions is decidable. We applied our technique to verify temporal properties of several interesting protocols. To the best of our knowledge, we have obtained the first mechanized liveness proof for both TLB Shootdown, and Stoppable Paxos.

This paper proposes CAESAR, a novel multi-leader Generalized Consensus protocol for geographically replicated sites. The main goal of CAESAR is to overcome one of the major limitations of existing approaches, which is the significant performance degradation when application workload produces conflicting requests. CAESAR does that by changing the way a fast decision is taken: its ordering protocol does not reject a fast decision for a client request if a quorum of nodes reply with different dependency sets for that request. The effectiveness of CAESAR is demonstrated through an evaluation study performed on Amazon's EC2 infrastructure using 5 geo-replicated sites. CAESAR outperforms other multi-leader (e.g., EPaxos) competitors by as much as 1.7x in the presence of 30% conflicting requests, and single-leader (e.g., Multi-Paxos) by up to 3.5x.

As the number of processors and the size of the memory of computing systems keep increasing, the likelihood of CPU core failures, memory errors, and bus failures increases and can threaten system availability. Software components can be hardened against such failures by running several replicas of a component on hardware replicas that fail independently and that are coordinated by a State-Machine Replication protocol. One common solution is to replicate the physical machine to provide redundancy, and to rewrite the software to address coordination. However, a CPU core failure, a memory error, or a bus error is unlikely to always crash an entire machine. Thus, full machine replication may sometimes be an overkill, increasing resource costs. In this paper, we introduce full software stack replication within a single commodity machine. Our approach runs replicas on fault-independent hardware partitions (e.g., NUMA nodes), wherein each partition is software-isolated from the others and has its own CPU cores, memory, and full software stack. A hardware failure in one partition can be recovered by another partition taking over its functionality. We have realized this vision by implementing FT-Linux, a Linux-based operating system that transparently replicates race-free, multithreaded POSIX applications on different hardware partitions of a single machine. Our evaluations of FT-Linux on several popular Linux applications show a worst case slowdown (due to replication) by ≈20%.

Distributed protocols such as Paxos play an important role in many computer systems. Therefore, a bug in a distributed protocol may have tremendous effects. Accordingly, a lot of effort has been invested in verifying such protocols. However, checking invariants of such protocols is undecidable and hard in practice, as it requires reasoning about an unbounded number of nodes and messages. Moreover, protocol actions and invariants involve both quantifier alternations and higher-order concepts such as set cardinalities and arithmetic. This paper makes a step towards automatic verification of such protocols. We aim at a technique that can verify correct protocols and identify bugs in incorrect protocols. To this end, we develop a methodology for deductive verification based on effectively propositional logic (EPR)—a decidable fragment of first-order logic (also known as the Bernays-Schönfinkel-Ramsey class). In addition to decidability, EPR also enjoys the finite model property, allowing to display violations as finite structures which are intuitive for users. Our methodology involves modeling protocols using general (uninterpreted) first-order logic, and then systematically transforming the model to obtain a model and an inductive invariant that are decidable to check. The steps of the transformations are also mechanically checked, ensuring the soundness of the method. We have used our methodology to verify the safety of Paxos, and several of its variants, including Multi-Paxos, Vertical Paxos, Fast Paxos, Flexible Paxos and Stoppable Paxos. To the best of our knowledge, this work is the first to verify these protocols using a decidable logic, and the first formal verification of Vertical Paxos, Fast Paxos and Stoppable Paxos.

New multi-leader consensus protocols leverage the Generalized Consensus specification to enable low latency, even load balancing, and high parallelism. However, these protocols introduce inherent costs with significant performance impact: they need quorums bigger than the minimum required to solve consensus and need to track dependency relations among proposals. In this paper we present M2PAXOS, an implementation of Generalized Consensus that provides fast decisions (i.e., delivery of a command in two communication delays) by leveraging quorums composed of a majority of nodes and by exploiting workload locality. M2PAXOS does not establish command dependencies based on conflicts, instead mapping nodes to accessed objects and enforcing that commands accessing the same objects be ordered by the same node. Our experimental evaluation confirms the effectiveness of M2PAXOS, gaining up to 7X over state-of-the-art Consensus and Generalized Consensus algorithms under partitioned data accesses and up to 5.5× using the TPC-C workload.

Leaderless consensus algorithms in the vein of EPaxos have performance advantages, especially for geo-replication, but are also very intricate, making them hard to modify and adapt for specific use cases. In this paper we show that their core principle can be captured in a generic leaderless generalized-consensus algorithm that uses two new abstractions: a dependency-set algorithm, which suggests dependencies for commands, and a map-agreement algorithm, which ensures that, for each submitted command, processes agree on a dependency set. Our generic algorithm gives rise to a family of algorithms whose members are obtained by using concrete dependency-set and map-agreement algorithms. On top of enabling modular correctness proofs of leaderless consensus algorithms, we expect that the modular structure of our generic leaderless algorithm will allow a principled theoretical and empirical evaluation of the trade-offs that can be achieved by different implementations of our two abstractions.

Linearizability is a key design methodology for reasoning about implementations of concurrent abstract data types in both shared memory and message passing systems. It provides the illusion that operations execute sequentially and fault-free, despite the asynchrony and faults inherent to a concurrent system, especially a distributed one. A key property of linearizability is inter-object composability: a system composed of linearizable objects is itself linearizable. However, devising linearizable objects is very difficult, requiring complex algorithms to work correctly under general circumstances, and often resulting in bad average-case behavior. Concurrent algorithm designers therefore resort to speculation: optimizing algorithms to handle common scenarios more efficiently. The outcome are even more complex protocols, for which it is no longer tractable to prove their correctness.

Decades of research in distributed computing have led to a variety of perspectives on what it means for a concurrent algorithm to be efficient, depending on model assumptions, progress guarantees, and complexity metrics. It is therefore natural to ask whether one could compose algorithms that perform efficiently under different conditions, so that the composition preserves the performance of the original components when their conditions are met.