Making Byzantine Consensus Live (Extended Version)

TL;DR

This paper introduces a view synchronizer abstraction that simplifies the design and analysis of Byzantine consensus protocols, ensuring liveness and enabling uniform comparison of protocols like HotStuff, Tendermint, PBFT, and SBFT.

Contribution

The paper proposes a formal view synchronizer abstraction for Byzantine consensus, providing a unified framework for analysis and comparison of multiple protocols under partial synchrony.

Findings

Guarantees liveness for several protocols using the synchronizer

Provides latency bounds for protocols with the synchronizer

Facilitates uniform analysis and comparison of protocols

Abstract

Partially synchronous Byzantine consensus protocols typically structure their execution into a sequence of views, each with a designated leader process. The key to guaranteeing liveness in these protocols is to ensure that all correct processes eventually overlap in a view with a correct leader for long enough to reach a decision. We propose a simple view synchronizer abstraction that encapsulates the corresponding functionality for Byzantine consensus protocols, thus simplifying their design. We present a formal specification of a view synchronizer and its implementation under partial synchrony, which runs in bounded space despite tolerating message loss during asynchronous periods. We show that our synchronizer specification is strong enough to guarantee liveness for single-shot versions of several well-known Byzantine consensus protocols, including HotStuff, Tendermint, PBFT and SBFT. We furthermore give precise latency bounds for these protocols when using our synchronizer. By factoring out the functionality of view synchronization we are able to specify and analyze the protocols in a uniform framework, which allows comparing them and highlights trade-offs.