Validating Labelled State Transition and Message Production Systems: A Theory for Modelling Faulty Distributed Systems

TL;DR

This paper introduces VLSMs, a formal framework for modeling and verifying faulty distributed systems, focusing on equivocation, and demonstrates how equivocating components can replace Byzantine ones without changing system analysis.

Contribution

The paper develops a formal theory of VLSMs for modeling faults, especially equivocation, and shows their equivalence to Byzantine faults in validator systems, validated in Coq.

Findings

Equivocation can be formally modeled and reasoned about in distributed systems.

Replacing Byzantine components with equivocating ones does not alter fault analysis.

All results are formalized and verified in the Coq proof assistant.

Abstract

Modeling and formally reasoning about distributed systems with faults is a challenging task. To address this problem, we propose the theory of Validating Labeled State transition and Message production systems (VLSMs). The theory of VLSMs provides a general approach to describing and verifying properties of distributed protocols whose executions are subject to faults, supporting a correct-by-construction system development methodology. The central focus of our investigation is equivocation, a mode of faulty behavior that we formally model, reason about, and then show how to detect from durable evidence that may be available locally to system components. Equivocating components exhibit behavior that is inconsistent with single-trace system executions, while also only interacting with other components by sending and receiving valid messages. Components of system are called validators for that system if their validity constraints validate that the messages they receive are producible by the system. Our main result shows that for systems of validators, the effect that Byzantine components can have on honest validators is precisely identical to the effect that equivocating components can have on non-equivocating validators. Therefore, for distributed systems of potentially faulty validators, replacing Byzantine components with equivocating components has no material analytical consequences, and forms the basis of a sound alternative foundation to Byzantine fault tolerance analysis. All of the results and examples in the paper have been formalised and checked in the Coq proof assistant.