The 12th Workshop on Formal Reasoning in Distributed Algorithms

Where the number of trials of a mechanism is bounded, it is sensible to engineer that mechanism to have such a small probability ϵ of failure that over all time we can discount the probability δ of it ever going wrong. So if there are at most 10⁹ trials and we are prepared to accept a δ=10⁻⁹ probability of failure over all time, this would suggest ϵ=10⁻¹⁸. If a blockchain has a good source of random numbers, this allows us to create many efficient mechanisms, including consensus, that are stochastically certain to work. A number of interesting challenges in formal reasoning arise.

Game-theoretic security analysis of blockchain technologies has proven highly valuable. Such analysis examines protocols from an economic perspective, specifically by exploring the economic incentives that drive user behavior. Thus, it ensures that deviating from the intended, honest behavior of a protocol is not financially beneficial: as long as users follow the protocol, they cannot be financially harmed, regardless of how others behave. Such an economic analysis of blockchain protocols can be encoded as an automated reasoning problem in the first-order theory of real arithmetic, thereby reducing game-theoretic reasoning to satisfiability modulo theories (SMT) solving. We conduct a divide-and-conquer security analysis based on compositional reasoning over games. Our compositional analysis is incremental: we divide games into subgames such that changes to one subgame do not necessitate re-analyzing the entire game, but only the ancestor nodes. Our approach is sound, complete, and effective: combining the security properties of subgames yields security of the entire game. Experimental results show that compositional reasoning scales well to games with millions of nodes, enabling security analysis of large real-life protocols.

In distributed systems with asymmetric trust, each participant is free to make its own trust assumptions about others, captured by an asymmetric quorum system. This contrasts with ordinary, symmetric quorum systems and threshold models, where trust assumptions are uniformly shared among participants. In the symmetric setting, quorum systems must satisfy the consistency and availability properties to solve key problems like reliable broadcast and consensus. But what properties are needed in the asymmetric setting to solve these problems? We examine this question in both the crash-fault and Byzantine models. In the crash-fault setting, any quorum system satisfying consistency and availability can be transformed into a symmetric one, removing any benefit from asymmetric trust. In the Byzantine model, consistency and availability are not enough to solve reliable broadcast and consensus. Existing approaches overcome this by introducing stronger assumptions. We show that some of these assumptions are overly restrictive, so much so that they effectively eliminate the benefits of asymmetric trust. We introduce a new way to characterize asymmetric problems and, based on this, present protocols for reliable broadcast and consensus that work under weaker assumptions than existing solutions.

Communication networks have become a critical infrastructure of our digital society. The resulting stringent reliability requirements however stand in stark contrast to today’s manual and error-prone approach to operate networks. In this talk, I will present opportunities for using formal methods to build highly dependable communication networks. In particular, we show how the policy-compliance of important network protocols can be verified in polynomial time, and explore synthesis approaches to efficiently generate and update network configurations. We will also discuss opportunities of AI/ML methodologies in this context.

Reasoning about consistency models for replicated objects is a challenging task that requires a deep understanding of both the consistency models themselves and a large part of human inputs in mechanized verification approaches.

In this work, we introduce a fully automated approach to reasoning about consistency models for replicated objects. We explore the monadic second-order logic (MSO) representation of consistency properties, with the aim of extending the well-known MSO-to-automata translation to traces of executions.

Thus, this talk focuses on reducing MSO over execution traces to MSO over finite words, so as to match the input requirements of the MONA tool, which performs satisfiability in this setting by translating such formulas into automata.

Binding requires a distributed protocol to limit the possible outputs of processes, in a manner that is unknown to the processes themselves. Commitment fixes the output to a value that remains hidden from almost all processes. Both are hyperproperties since they consider possible extensions of a trace.

Specifying these properties is cumbersome, and arguing about them is even more so.

This talk explores how these properties can be captured by enforcing strong refinement of abstract modules that produce ghost outputs, which are not observed by the processes invoking the protocol implementing the module. We will discuss how ghost outputs may facilitate the composition and verification of such modules.

Examples will include binding crusader agreement and gather, random secret draw and verifiable secret sharing.