Hedera Hashgraph, a next-generation distributed public ledger with highly diversified governance, today announced that the hashgraph consensus algorithm has been validated as asynchronous Byzantine Fault Tolerant (aBFT) by a math proof checked by computer using the Coq system.
This proves the claims stated in the hashgraph tech report that hashgraph is aBFT – mathematically the highest possible level of security for distributed systems. Dr. Leemon Baird will present a session today on formal methods at Hedera18, the inaugural hashgraph developer conference. Interested participants can join the live stream at learn.hederahashgraph.com/livestream.
Coq is a formal proof verification system. Coq provides a formal language to write mathematical definitions and executable algorithms and theorems together with an environment for the semi-interactive development of machine-checked proofs. It is often used for certifying the properties of programs, programming languages, and mathematics. Unlike most math proofs that are merely checked by humans, a Coq proof is actually checked by a computer. This avoids some of the mistakes that humans can make when reading a proof.
The verification was conducted through the Coq Proof Assistant, which checks that the proof is correct, and was completed by Karl Crary, Associate Professor of Computer Science at Carnegie Mellon University.
“This is just the beginning. Formalized methods like these, where a computer verifies a math proof of correctness, are the future of software, wherever security and trust are critical.”
Hedera plans to continue to create additional Coq system proofs, to prove the correctness of additional efficiency improvements, and eventually to ensure that the software implementing the algorithm is also correct.
Asynchronous Byzantine Fault Tolerance
For over three decades, Byzantine fault tolerance (BFT) has been the standard for security in distributed systems. Byzantine fault tolerance means that honest members of a network can be guaranteed to agree on a common consensus, even if malicious members (Byzantine nodes) are trying to prevent that consensus, or trick them into reaching different conclusions. A system is BFT if it can guarantee that there will come a moment in time when all nodes agree on consensus, and they know they’ve reached consensus, and it is always the same consensus.
BFT means achieving this even while allowing for a wide range of faults or attacks. Byzantine faults include behaviors like lying, collusion, and selective non-participation. Clearly, it will be harder for a set of nodes to come to valid consensus under these sorts of errors, compared to simpler scenarios where nodes may just crash.
The strongest form of BFT is asynchronous. An aBFT system allows for the possibility of some messages between honest members being delayed arbitrarily long, or not making it to their intended recipients at all. The adversary might even control the network itself, at least partially. This is the gold standard for distributed consensus. A truly secure distributed ledger technology (DLT) must be able to achieve consensus under this assumption.
Algorithms may claim to support ‘partially’ asynchronous BFT, where messages are never delayed by more than a certain period of time, and always get through by that deadline. But today’s reality is that many kinds of attackers can prey on exactly this assumption, to either bring a network to its knees, or disrupt the order of transactions. Botnets, Distributed Denial of Service (DDoS) attacks, and malicious firewalls can all interfere with messages. As such, ‘partially’ asynchronous BFT will not provide for reliable, real-world systems in the long run. As Hedera builds an internet-wide trust layer that could eventually process trillions of dollars worth of transactions, we must ensure that we apply the strongest security principles possible to deal with such attacks.
With the new Coq proof, Hedera becomes the first public ledger that has a computer-verified mathematical proof that it is truly asynchronous BFT. It guarantees consensus will be achieved, we will know it when it happens, and we will all reach the same consensus, and do so even under realistic assumptions about malicious nodes and network errors.