Compositional Verification of Composite Byzantine Protocols

Byzantine Fault-Tolerant (BFT) protocols are known to be difficult to design and to reason about. To address this challenge, on one hand, several approaches have been developed recently for computeraided formal verification of the desired correctness properties, both safety and liveness, of standalone BFT protocols. On the other hand, the distributed computing community has made attempts to reduce the conceptual complexity of constructing new such protocols by showing how to assemble them from simpler "building blocks". No methodology to date combines these two approaches for foundational verification of arbitrary BFT protocols. We present Bythos, the first foundational framework for compositional mechanised verification of both safety and liveness of composite BFT protocols. Bythos is implemented on top of the Coq proof assistant and uses Coq's higher-order logic to reuse proofs of common facts about knowledge and trust in BFT protocols. It allows for compact liveness specifications in the style of TLA+, and for their proofs using an embedding of TLA into Coq. Most importantly, Bythos provides a family of higher-order definitions that allow building composite BFT protocols from simpler ones, with their correctness proofs derived. We showcase Bythos by verifying in it safety and liveness properties of three basic BFT protocols: Reliable Broadcast, Provable Broadcast, and the recently proposed Accountable Byzantine Confirmer, as well as their compositions. CCS Concepts • Networks → Protocol testing and verification; Formal specifications; • Security and privacy → Distributed systems security.