Many blockchains in use today could be within weeks of catastrophic failure due to problems with the consensus protocols they use. Here Vincent Gramoli shows why this is so, and lays out the solution.
Blockchains have begun to revolutionise various industries, some of which are critical. The attacks that successfully exploit blockchain vulnerabilities are frequent, and today the billions of dollars they trade remain at risk because of human errors. We see the catastrophic impacts of human errors in situations like the MCAS software failures, that led to the crashes of Boeing 737s. As blockchain use becomes more widespread, it is essential that machine-checked proofs should be used to mitigate human errors in the blockchain's most sensitive protocols, like its consensus protocol.
To apply blockchain technology to the real world, testing is no longer sufficient, and formal verification is now required. This is why Redbelly features, to our knowledge, the first formally verified blockchain consensus protocol.
Redbelly Blockchain builds upon years of research led by the University of Sydney and the Commonwealth Science Industry Research Organisation (CSIRO). In collaboration with European researchers, the Concurrent Systems Research Group designed a novel deterministic consensus algorithm that prevents the formation of forks, which is the main cause of double spending of digital assets in blockchains.
Vulnerabilities in classic blockchains
During 2016-2020, the research group identified various vulnerabilities in classic blockchains. Some of these vulnerabilities affected the Ethereum blockchain and were acknowledged by the security teams of geth and OpenEthereum (formerly known as parity).
They were presented to the Ethereum developer community and published in one of the top scientific conferences on security [1]. The commonality between these vulnerabilities is a disagreement on the block to append to the blockchain, leading the blockchain to fork. This fork allows an attacker to double spend by including conflicting transactions in the resulting blockchain branches. These discoveries served as the basis for the design of a more secure blockchain.
It is important to note that these vulnerabilities are symptomatic of the probabilistic way most blockchains reach consensus on the next block to append. In other words, most blockchains offer a probabilistic consensus solution, guaranteeing that consensus is solved in almost all cases. The problem, inherent to any probabilistic consensus solutions that have now become commonplace, is that there exists a non-null probability that the consensus fails. Researchers have tried to minimise this probability by making assumptions on the environment, however, the risk of failure remains.
The crux of the problem is that the probability of failure grows exponentially fast with the usage of the blockchain. Consider, for example, a blockchain with a consensus protocol whose probability of consensus failure is 1 over 100 million. In other words, the probability of its consensus succeeding is 99.999999%. As one consensus instance is required to decide on each block, the probability that the blockchain does not fail while producing k blocks is:
For example, the probability that the blockchain would successfully append 15,000,000 blocks, which is about the number of blocks in Ethereum at the time of writing, would be 0.9999999915,000,000 = 86%.
The real problem is the trend
But the real problem is not so much about this number but rather about the trend: the probability of the blockchain failing grows exponentially fast with the number of blocks that are appended. Hence, the blockchain is expected to fail before appending its 70,000,000th block. With modern blockchains appending blocks at a pace of 30 blocks per second, this failure could arrive in less than a month. Once this failure occurs, multiple distinct histories of transactions appear in the blockchain, and there is no way to revert to a consistent state.
Redbelly solves the consensus problem
Redbelly has adopted a different solution by (really) solving consensus. This means that the consensus protocol solves all properties of the consensus problem (termination, agreement, validity) without any probability of failing to do so. To avoid any confusion and to contrast such a consensus solution with probabilistic consensus solutions, the distributed computing research community sometimes refers to it as a deterministic solution. Although this deterministic consensus protocol was published in a peer-reviewed paper in the proceedings of a scientific conference, there is still a risk that the reviewers missed an error that authors could have made. After all, this would not be the first mistake published in scientific publications [2].
To cope with this risk, we use formal verification: an automated way of mathematically checking that the properties of our problem are satisfied by our protocol specification in all its possible executions. With the help of researchers in the USA and Europe, we modelled the behaviour of hackers trying to influence the decision to double spend and showed that there is no way these hackers, however they behave, could succeed [3]. The difficulty as one can imagine is to model all sizes of supposedly tolerated coalitions of t < n/3 hackers that can delay messages in any way or act arbitrarily in a system of any possible size n. Until now, most efforts were dedicated to checking the proofs of individual blockchain consensus components with theorem provers, but this did not eradicate the efforts of writing the proofs. By contrast, our formal verification relies on parameterised model checking that checks the blockchain consensus protocol itself.
To conclude, Redbelly offers an unprecedented level of security in blockchains, not only through deterministic guarantees but also through formal verification that mitigates human errors. After years of scientific research, Redbelly finally allows blockchains to be used in the real world while mitigating risks for its users.
References
[1] Ekparinya, Gramoli, Jourjon. The attack of the clones against proof-of-authority. Presented at the Community Ethereum Development Conference, 2019. 27th Annual Network and Distributed System Security Symposium (NDSS), 2020.
[2] Tholoniat, Gramoli. Formal Verification of Blockchain Byzantine Fault Tolerance. Presented at the 6th Workshop on Formal Reasoning in Distributed Algorithms (FRIDA), 2019. Book chapter of Handbook on Blockchain, Springer Nature, DOI: 978-3-031-07534-6, 2022.
[3] Bertrand, Gramoli, Konnov, Lazic, Tholoniat, Widder. Brief Announcement: Holistic Verification of Blockchain Consensus. Proceedings of the 41st ACM Symposium on Principles of Distributed Computing (PODC), 2022.
