Red Belly Blockchain was discovered three years ago and results from more than fifteen years of expertise in the field of distributed systems developed in research institutes among the best in the USA, France, Switzerland and Australia.
As an alternative to the energy greedy proof-of-work, new blockchains constrain the set of participants whose selection is debatable. These blockchains typically allow a fixed consortium of machines to decide upon new transaction blocks. In this paper, we introduce the community blockchain that bridges the gap between these public blockchains and constrained blockchains. The idea is to allow potentially all participants to decide upon “some” block while restricting the set of participants deciding upon “one” block. We also propose an implementation called ComChain that builds upon the Red Belly Blockchain, the fastest blockchain we are aware of. It runs a consensus among the existing community to elect a new community. This reconfiguration speeds up as the number of removed nodes increases.
In the 6th Workshop on Formal Reasoning in Distributed Algorithms (FRIDA'19) collocated with DISC 2019.
To implement a blockchain, the trend is now to integrate a non-trivial Byzantine fault tolerant consensus algorithm instead of the seminal idea of waiting to receive blocks to decide upon the longest branch. After a decade of existence, blockchains trade now large amounts of valuable assets and a simple disagreement could lead to disastrous losses. Unfortunately, Byzantine consensus solutions used in blockchains are at best proved correct “by hand” as we are not aware of any of them having been formally verified.
In this paper, we propose two contributions: (i) we illustrate the severity of the problem by listing six vulnerabilities of blockchain consensus including two new counter-examples; (ii) we then formally verify two Byzantine fault tolerant components of Red Belly Blockchain using the ByMC model checker. First, we specify a simple broadcast primitive in 116 lines of code that is verified in 40 seconds on a 2-core Intel machine. Then, we specify a blockchain consensus algorithm in 276 lines of code that is verified in 17 minutes on a 64-core AMD machine using MPI. To conclude, we argue that it has now become both relatively simple and crucial to formally verify the correctness of blockchain consensus protocols.
Workshop on Verification of Distributed Systems (VDS'19) collocated with NETYS 2019.
In this paper, we introduce Polygraph, the first accountable Byzantine consensus algorithm. If among n users t<n/3 are malicious then it ensures consensus, otherwise (f>=n/3) it eventually detects malicious users that cause disagreement. Polygraph is appealing for blockchain applications as it allows them to totally order blocks in a chain whenever possible, hence avoiding forks and double spending and, otherwise, to punish (e.g., via slashing) at least n/3 malicious users when a fork occurs. This problem is more difficult than perhaps it first appears. We show that a commonly used state-of-the-art Byzantine fault tolerance consensus algorithm cannot be made accountable without storing and exchanging extra logs of at least Omega(n) rounds. By contrast, each round of Polygraph exchanges only O(n^3) bits and O(n^2) messages. Finally, we use a blockchain application to evaluate Polygraph on a geodistributed system of 80 machines to commit ten thousand of transactions per second.
In this paper, we present the largest experiment of a blockchain system to date. To achieve scalability across 1000 servers in more than 10 countries located on four different continents, we drastically revisited Byzantine fault tolerant blockchains and verification of signatures. The resulting blockchain, called the Red Belly Blockchain (RBBC), commits more than a hundred thousand transactions issued by permissionless nodes, that are grouped into blocks within few seconds through a partially synchronous consensus run by permissioned nodes. It prevents double spending by guaranteeing that a unique block is decided at any given index of the chain in a deterministic way.