In October 2022, after a thorough peer review process, the long version of the 'Holistic Verification of Blockchain Consensus' was accepted at the International Symposium on Distributed Computing (DISC 2022) in Augusta, Georgia. DISC is an international forum on the theory, design, analysis, implementation and application of distributed systems and networks. This scientific article was co-authored by our Founder and CTO Professor Vincent Gramoli and Redbelly Network made the official announcement via our social channels at the same time.
The article summarises how the Democratic BFT consensus, at the heart of Redbelly Network, has been the first blockchain consensus to be fully formally verified. Demonstrating the interest of the scientific community in reducing the human errors in distributed algorithms at the heart of blockchain technologies through the use of machine checked proofs.
Prof Vincent Gramoli talks specifically around the consensus protocol and how Redbelly Network uniquely solves the problem.
To implement a secure blockchain, one has to find a solution to make sure a distributed set of computers agree on a unique block at a given index of the chain. Such a solution is called a consensus protocol and the research community has been designing several consensus protocols for the last four decades for various applications. To our knowledge, prior to our work[1] no consensus protocols for blockchain applications had ever been fully verified.
The consensus problem consists of having multiple machines agreeing on a unique value or block. It is well known that solving the consensus problem is necessary in order to implement a blockchain. This is because the blockchain is an append-only ledger implemented in a distributed fashion that must guarantee that assets are not double spent. Many blockchains were designed without strictly solving the consensus problem. Hackers manage to fool different sets of correct participants that conflicting transactions were committed in these blockchains. This led to double spending attacks against Bitcoin in 2014 [2], Bitcoin Gold in 2018[3] and Ethereum Classic in 2020[4], just to cite a few that have been reported publicly. Our recommendations[5] on similar attacks against Ethereum have been, at least, partially addressed.
Other blockchains were designed on top of Byzantine fault tolerant consensus protocols that were manually proven correct by scientists. As these protocols tend to be extremely complex, further scrutinising the protocols and their manual proofs revealed some flaws contradicting that such protocols were truly solving consensus. This was the case of the Tendermint consensus protocol, the Ripple consensus protocol, HoneyBadger BFT, and Istanbul BFT (IBFT) impacting the robustness of the Tendermint blockchain, Cosmos, Quorum, xRapid[6]. Some patches have been proposed to fix these issues, however as far as we know the resulting protocols have never been formally verified.
Formal verification is the mathematical process of using a machine to verify that a proof is correct, hence minimising the error-prone human tasks. It requires scientists to first specify the protocol and the consensus problem in a language understandable by a computer and then ask the computer whether the problem is solved in all possible executions of the protocol. The reason why no blockchain protocols have been formally verified as far as we know, is likely due to the complexities of these protocols. Exploring all possible executions of the protocol with any number of distributed machines and any portion of hackers colluding with each other would require too much computational power than what is currently available.
To solve this approach, we focused on the binary consensus protocol at the heart of Redbelly Network. This consisted of replacing the partial synchrony assumption with a fairness assumption, which aimed to prove termination. A parameterized model was used to prove that all executions solve the consensus problem regardless of the size of the system and the coalition of hackers.
About the Author: Professor Vincent Gramoli is the founder and CTO of Redbelly Network. He is a researcher in the field of distributed systems and algorithms. His focus is on the design/analysis of distributed systems and algorithms for shared memory, as well as data-centric systems. This includes distributed hash tables, distributed shared memory and transactional memory.
Vincent received the 2022 Sydney University’s Dean’s Award for Outstanding Research Advisor. He was also awarded Education Leader of the Year by Blockchain Australia at their 2022 Blockies Awards.
Vincent has received the Best Paper Awards of ICDCS 2021, IPDPS 2022 and ICDCS 2022. He received a Future Fellowship from the Australian Research Council and leads the Concurrent Systems Research Group at the University of Sydney.
In the past, Vincent has been affiliated with INRIA, Cornell, CSIRO and EPFL. He received his PhD from Université de Rennes and his Habilitation from UPMC Sorbonne University. He served as Program Committee Chair of International Scientific Conferences (NETYS’13, FAB’21, Tokenomics’21, OPODIS’21). He co-wrote a book on Consistent Distributed Storage published by Morgan & Claypool and a book on Blockchain Scalability published by Springer. His Blockchain Scalability MOOC on Coursera is taken by thousands of students.
References
[1] Holistic Verification of Blockchain Consensus N. Bertrand, V. Gramoli, M. Lazić, I. Konnov, P. Tholoniat, J. Widder. 36th International Symposium on Distributed Computing (DISC), 2022. BA published in the proceedings of the ACM Symposium on Distributed Computing (PODC), 2022.
[2] Hacker Hijacks ISPs- Steals $83,000 from Bitcoin Mining Pools https://www.zdnet.com/article/hacker-hijacks-isps-steals-83000-from-bitcoin-mining-pools/
[3] Bitcoin Gold Hacked for $18 Million https://news.bitcoin.com/bitcoin-gold-hacked-for-18-million/
[4] $5.6M Double Spent: ETC Team Finally Acknowledges the 51% Attack On Network
https://news.bitcoin.com/5-6-million-stolen-as-etc-team-finally-acknowledge-the-51-attack-on-network/
[5] The attack of the clones against proof-of-authority. P Ekparinya, V Gramoli, G Jourjon. 27th Annual Network and Distributed System Security Symposium (NDSS), 2020. Community Ethereum Development Conference, 2019.
[6] Formal Verification of Blockchain Byzantine Fault Tolerance Pierre Tholoniathttps://arxiv.org/pdf/1909.07453.pdf
