Formal methods for blockchain

In these systems, participants distributed across the network arrive at a consensus without going through a central authority. Byzantine fault tolerant (BFT) consensus algorithms, among the most sophisticated available, guarantee that a consensus will be reached even if a certain number of network nodes fail or act maliciously. But the algorithms only work if the number of bad actors (or “Byzantines”) remains below a certain threshold (generally a third of the total number of participants). To determine the number of bad actors in a given distributed system and, therefore, whether the consensus reached is reliable, you have to be able to count the bad actors during system execution.

We have developed a three-step runtime verification method, based on our MAAT IAT formal analysis tool, that identifies Byzantine behavior and provides public proof.

1. A behavioral model of the consensus algorithm is produced in the MAAT IAT specification language, an operator-based language describing parallel interaction processes proven using the Coq proof assistant.
2. The messages exchanged between network participants are monitored and logged by a centralized multi-trace module that observes all system communications.
3. The conformity of each participant’s behavior is assessed using a formal multi-trace conformity technique in MAAT IAT. If a Byzantine is identified, the model is updated, and the tool continues to search for other bad actors.

Our method goes beyond the state of the art in that it can identify several bad actors operating at the same time, it provides public proof, and it requires no specific hardware. It can also be used for any distributed algorithm that can be modeled in the MAAT IAT language.