Denisa Diaconescu
University of Bucharest, Bucharest, Romania

Formally modeling and reasoning about (asynchronous, message passing) distributed systems with faults is a challenging task. Depending on the system model, an execution of a distributed protocol may be subject to many kinds of faults, from simple recoverable component crashes to Byzantine adversarial actions.

We recently proposed the theory of Validating Labeled State transition and Message production systems (VLSMs) as a general approach to modeling and reasoning about distributed protocols executing in the presence of faults. In particular, VLSM executions can be subject to equivocation behavior. Equivocation refers to claiming different beliefs about the state of the protocol to different parts of the system in order to steer the protocol-abiding components into making inconsistent decisions. A key issue is the fact that messages received from equivocating components seem to be valid messages. For example, if a system tries to come to a consensus about the value of a bit, an equivocating component may claim the bit is $0$ to one part of the system, and $1$ to the other. Equivocation behavior cannot be produced by a single protocol execution, but only by multiple protocol executions, i.e., an equivocating component behaves as if running multiple copies of the protocol.

In consensus protocols, it is common for components to "validate" received messages in order to ensure that malformed messages are not received. We formalize this idea into a general notion of validator for a system. We show that the effect that Byzantine components can have on honest validators is no different than the effect equivocating components can have on non-equivocating validators. By this, we point out that equivocation fault tolerance analysis is a viable alternative to Byzantine fault tolerance analysis.

The talk will be self-contained and is based on joint work with Vlad Zamfir, Wojciech Kolowski, Brandon Moore, Karl Palmskog, and Traian Florin Şerbănuţă.