Practical Analysis of the Giskard Consensus Protoco

Abstract: Consensus protocols are the core of modern blockchain systems, such as the Bitcoin, Ethereum, and Algorand networks. Thanks to these protocols, participants in a blockchain network can reach consensus on which blocks to add to a blockchain, to have a consistent chain of blocks in the whole network. Blocks are typically collections of transactions, e.g., transferring currency between participants, but can contain other data depending on the use case. Consensus protocols are difficult to design, test, and implement. Problems may only manifest in rare cases but can have disastrous consequences. Formal protocol models allow exhaustive analysis and formal verification. However, formal verification is only as good as the specification of the protocol. For example, specification properties could be vacuously true, or the specification may omit to mention liveness properties that are crucial for progress in a system implementation. This thesis describes the practical validation of a formal specification of Giskard, a consensus protocol used in the PlatON network. We translated key aspects of a formal model of Giskard in the Coq proof assistant to executable Python code, and integrated them into the Sawtooth blockchain framework. Then, we ran simulations of a blockchain network executing Giskard using Sawtooth, checking network node state properties of Giskard as well as its global safety properties. Automated clients from the Sawtooth network provided randomly generated transactions as input for the network. The implementation with the test results are available for reproducibility. Both consensus safety and liveness issues were found in the formal specification of Giskard during the simulations. Based on the previous informal English specification of Giskard, we propose a new formal specification which was validated to reach consensus on blocks in the simulated blockchain network and uphold the protocol’s crash and Byzantine failure tolerance to a certain degree. The improved formal model can serve as a new basis for verifying and implementing Giskard in the future.