Formal Methods: The Importance of Being ABFT in a World with Bad Actors
Oct 29, 2018
by Hedera Team
Hedera is the most used, sustainable, enterprise-grade public network for the decentralized economy.

In the past year, over $1 billion in cryptocurrency has been stolen by hackers. There have also been denial of service attacks that have shut down other types of servers for hours. For example, a 2016 DDoS attack (executed via a botnet consisting of a large number of  compromised internet connected devices) against DNS (Domain Name System) provider Dyn caused major internet services to be unavailable for many users across North America and Europe for a number of hours. If public distributed ledgers continue to grow, these networks could eventually have trillions of dollars of value flowing through them — and similar disruptive cyberattacks are bound to follow. That’s why, before using distributed ledgers, enterprises and careful consumers will demand that the platforms demonstrate the highest possible levels of network security.

The highest security standard for consensus algorithms is known as Asynchronous Byzantine Fault Tolerance (ABFT). The hashgraph algorithm, as used in the Hedera public ledger, achieves this gold standard, with a mathematical proof that it is ABFT. This proof-of-stake consensus system was first proved to be ABFT in a rigorous math proof published in 2016. That proof has now been verified by computer in a formal verification completed by a Carnegie Mellon University professor — and we think it is important to explain what that means.

If you’re reading the Hedera blog, you’re probably familiar with the Byzantine Generals Problem (if not, here’s a short explainer). The problem is for a distributed group to achieve consensus on a set of transactions when you can’t trust all the members of the group, nor the network over which they communicate. In a public ledger where anyone can run a node, you can’t trust all of the nodes to be honest, as a bad actor could stand up a node, or create a firewall, or launch a set of attacking computers. They could seek to disrupt consensus by delaying transactions or otherwise corrupting things.

Byzantine fault tolerance means that the honest members of a network can be guaranteed to agree on the timing and order of a set of transactions, even if almost ⅓ of the influence of the nodes is maliciously trying to prevent that consensus. Or to trick the honest nodes into reaching different conclusions, or even if to attack the internet itself. But more than that, a Byzantine Fault Tolerant (BFT) system must deliver finality of consensus. This means there will come a moment in time when a node knows it has achieved consensus, and that all participating nodes will reach the same consensus, and that there is zero chance that the consensus will change.

However, there is another aspect to consider — whether this can still be achieved when there are attacks on the internet itself. Intuitively, if an honest node does not receive a message it expects, it cannot easily distinguish between that message being sent by an another honest node but subsequently being lost by the network, or a dishonest node not sending the message in the first place. The more unreliable the network is with respect to delivery of messages, the more challenging is consensus — and so accordingly the more challenging to achieve BFT.

Some consensus algorithms have proofs that they are BFT, but the proofs rely on simplifying assumptions about the network’s reliability with respect to message delivery — assumptions that do not reflect the reality of today’s internet — a reality that includes firewalls, botnets, DDoS attacks, worms, and viruses that can impact message delivery. For example, so called partially synchronous BFT or partially asynchronous BFT systems make the assumption that messages are never lost and will always arrive within some known bound. With such an assumption, nodes can reliably deduce whether another node is faulty. But this assumption doesn’t match reality.

A much stronger version of BFT, one that better acknowledges today’s network reliability, is asynchronous BFT (ABFT). Rather than assuming 100% reliability, and assuming some maximum message latency, ABFT systems allow for messages to be lost or indefinitely delayed  — assuming only that an honest node’s messages will eventually get through. It is much more challenging for an honest node to assess whether another node is not following the rules, if that node’s messages can be indeterminately delayed.

It is challenging to make consensus asynchronous BFT. But it better reflects the reality of networks than pretending we can assume synchronous or partially synchronous. The importance of ABFT has been widely recognized among computer scientists, but for decades it could not be achieved at scale. This changed with Dr. Leemon Baird’s invention of the proof-of-stake hashgraph consensus algorithm used by Hedera, which he proved mathematically to be ABFT in his 2016 tech report, and published again in the Hedera whitepaper.

While other mathematicians have verified the proof of hashgraph being ABFT, additional confidence in its correctness is possible. Formal methods is the process of having a computer check whether a system (such as an algorithm or piece of software) satisfies some set of requirements or properties (such as ABFT). This starts with writing a math proof in the traditional form, and then working to put it in a form that a computer can check. This verifies an algorithm's properties in a more thorough fashion than just having humans read it. Coq is a formal proof assistant system that provides a formal language to write mathematical definitions and axioms and theorems, together with an environment for interactive development of machine-checked proofs.

We are now pleased to announce additional validation of hashgraph’s ABFT status. A Carnegie Mellon professor has completed a computer-checked math proof using Coq, that verifies that the hashgraph algorithm used by Hedera is ABFT. With this new proof, the Hedera platform becomes the first public, proof-of-stake, distributed ledger that has a computer-verified mathematical proof that it is ABFT.

Our announcement on the Coq proof can be found at https://hedera.com/blog/coq-proof-completed-by-carnegie-mellon-professor-confirms-hashgraph-consensus-algorithm-is-asynchronous-byzantine-fault-tolerant.

The ultimate vision, as part of our ongoing commitment to the long-term security of the Hedera platform, is for every layer of the stack to be verified with the same rigor — from algorithms to software to even hardware. The Coq proof validates the original proof that Hedera’s foundational algorithm is ABFT. The next step is to verify efficiency tweaks to the algorithm, and then to verify that the consensus software correctly implements it. So stay tuned!

To download and run the Coq scripts, visit https://hedera.com/platform#security.