Master Thesis
Analyzing a modern Byzantine consensus protocol and its primitives
In a permissoned setting, a Byzantine fault-tolerant state machine replication (BFT-SMR) protocol implements a distributed log of operations. A recent breakthrough in this area was the development of HotStuff [1]; a leader-based consensus protocol that uses threshold signatures. Besides threshold signatures, HotStuff relies on an array of powerful primitives such as authenticated links, quorums, special broadcasts and leader-detectors (see [2] and [3] for further explanations on these primitives).
In this work, we will epistemically analyse two of the core primitives of HotStuff; Byzantine eventual leader detectors and quorum systems. Here, epistemically means that we will analyse what an agents knows. For example, an honest agent should only trust a new leader, if she knows that at least one honest agent has complained about the current leader (putsch-resistance). Or in the case of quorums; if an agent receives two quorums, then she knows that they intersect in an honest agent. Summarised, we will explore the theory of knowledge in distributed systems [4] and model a Byzantine eventual leader detector as well as quorum systems.
Requirements: Distributed algorithms, some graph-theory and propositional logic.
References
[1] HotStuff
[2] Introduction to Reliable and Secure Distributed Programming
[3] Distributed Algorithms FS2022
[4] Reasoning about Knowledge in distributed systems