BG: A Modular Treatment of BFT Consensus Toward a Unified Theory of BFT Replication

We provide an expressive framework that allows analyzing and generating provably secure, state-of-the-art Byzantine fault-tolerant (BFT) protocols over graph of nodes, a notion formalized in the HotStuff protocol. Our framework is hierarchical, including three layers. The top layer is used to model the message pattern and abstract core functions on which BFT algorithms can be built. The intermediate layer provides the core functions with high-level properties sufficient to prove the security of the top-layer algorithms. The bottom layer presents operational realizations for the core functions. Using our framework, designing a BFT protocol is reduced to instantiating two core functions together with their specific properties. Unlike prior BFT frameworks, our framework can analyze and recast BFT protocols in an exceedingly fine-grained manner. More importantly, our framework can readily generate new BFT protocols. In this paper, we show that the framework allows us to fully specify and formally prove the security for a family of BFT protocols, including known protocols such as HotStuff, Fast-HotStuff, and SBFT. Additionally, we show that our framework can generate four new protocols outperforming existing ones, including 1) two protocols with 5f+1 replicas achieving optimal message complexity; 2) the first BFT protocol achieving optimal message complexity with 4f+1 replicas; and 3) a two-phase protocol with 3f+1 replicas achieving linear authenticator complexity in the fast path.