CBC Casper and formal verification
This is Ryuya (Twitter: nrryuya) from the LayerX R&D team. We published our first paper on our work on CBC Casper: “Refinement and Verification of CBC Casper”.
This paper is accepted at Crypto Valley Conference 2019 and the poster of this work is accepted at IEEE S&P 2019.
CBC Casper is a proposal of beautiful PoS consensus protocol which has various potential advantages and will possibly be adopted by ETH2.0 in the future. In this article, I describe the basics of CBC Casper and introduce our work.
Consensus protocols in blockchain
Before I start to explain CBC Casper, I’ll briefly introduce what kinds of consensus protocols are used for blockchain. First, there are two kinds of blockchain consensus: (1) block-based consensus and (2) chain-based consensus.
In (1) block-based consensus, we execute a consensus protocol for each block. If participants agree on a block, the block is included in the chain. Otherwise, they skip the block and the next block is proposed. In these kinds of protocols, a fork of the chain is impossible or rare. The famous protocols of this type include Tendermint and Algorand. The consensus protocol executed for each block is often inspired by classical protocols like pBFT. (I just named this as “block-based” right now. I sometimes see it is called “BFT-based”.)
In (2) chain-based consensus, participants extend chains before the blocks are finalized. We set an appropriate rule about which chain they should extend (fork-choice rule) so that the chain eventually converges. Needless to say, Bitcoin and the current Ethereum are using chain-based consensus. They choose block proposers by mining game and use the longest-chain rule as the fork-choice rule. There are PoS chain-based consensus protocols like Ouroboros. In these protocols, finality is probabilistic.
Casper the Friendly Finality Gadget (FFG), which is planned to be used in ETH2.0, is a mechanism to add deterministic finality to chain-based consensus in a way similar to pBFT. GRANDPA of Polkadot is also a finality gadget.
CBC Casper? It is classified as a chain-based consensus but it has deterministic finality, as explained below.
CBC Casper
CBC Casper is a family of PoS consensus protocols, originally proposed by Vlad Zamfir. The latest white paper can be found here.
What makes CBC Casper different from other protocols is its (1) “correct-by-construction” methodology and (2) message justification.
(1) “Correct-by-construction” methodology
CBC Casper is like a framework to define consensus protocols. Each member of CBC Casper is defined by 5 parameters.
You can instantiate a specific protocol from the CBC framework. For example, in a blockchain consensus protocol, consensus values are all the possible blocks and estimator is the fork-choice rule. (Additionally, you also need to specify the validator strategy.) You can also adopt data structures other than blockchain.
“Correct-by-construction” means that protocols instantiated by CBC Casper always satisfy safety (i.e. validators do not make conflicting decisions). Other properties including liveness (i.e. validators eventually make decisions) are discussed in each instantiation.
The CBC framework is flexible enough to represent protocols from “block-and-vote” consensus to “vote-by-block” consensus. Hence, we can analyze various trade-offs (e.g. between time to finality and message overhead) in a single framework.
(2) Message justification
In CBC Casper, every message includes a justification i.e. messages which the sender has seen so far. A justification is evidence of the fork-choice. Every block a validator proposes or votes for is enforced to be the result of the fork-choice rule.
By having justifications, we can detect (and punish!) a kind of Byzantine fault, equivocation i.e. a validator who sends two messages which do not justify each other is punished.
When a validator switches the chain without equivocating, she must show the evidence as justification to prove the switch is correct under the fork-choice rule.
Since non-equivocating validators must include their previous messages, the evidence of her fork-choice at some point in time is always a part of the evidence of her future fork-choice. From this, validators are eventually “locked on” a block after seeing a sufficient number of other validators agreeing on the block.
By setting a threshold of equivocation faults, when a sufficient number of validators locked on a block, the block gets finalized. Hence, CBC Casper has deterministic finality. The actual mechanism to detect finality is called safety oracle.
In a protocol instantiation, we specify the validator strategy so that a sufficient number of validators eventually locked on blocks for liveness.
In the “vote-by-block” consensus, I conjecture that it is almost sufficient for liveness to show that the underlying chain converges.
Advantages of CBC Casper
As explained, the advantages of CBC Casper include flexibility and theoretical simplicity.
Further, in the detection of finalized blocks, you can set your own threshold i.e. it is subjective finality (similar to “6 confirmation” in Bitcoin, but arbitrary close to 100% equivocation fault tolerance!).
Also, unlike Casper FFG, the finality cycle of CBC Casper is block-basis, allowing low latency to finality.
For readers who want to know more about CBC Casper, I recommend the posts by Barnabé Monnot and Vitalik’s tutorial.
Formal verification of CBC Casper
The main contribution of our paper is to refine the existing formalization and verify it with Isabelle/HOL (proof assistant). A proof assistant is like an IDE for mathematical logic and helps humans to detect bugs in pen-and-paper proofs and accelerate formal verification.
The proofs can be found here.
https://github.com/LayerXcom/cbc-casper-proof
Specifically, we proved properties about fundamental concepts of CBC Casper such as message justification and state transition and then proved safety and refined safety oracle.
Also, one of the motivations of this paper is to systemize the knowledge of CBC Casper across multiple (draft) papers and blog posts in an academic style, to make CBC Casper “get out of the wilds”!
Future work
I’ve just started to work on an actual protocol instantiation to prove liveness of a CBC Casper consensus protocol.
Another interesting direction is code generation. Isabelle/HOL allows us to generate code from the defined proofs. For example, this picture shows a part of the Haskell code generated by Isabelle/HOL.
Also, applications for sharding which Vlad working on is ambitious and interesting work. (See this slide by Vlad!)
Although CBC Casper is theoretically simple, there are a few issues to actually implement it. Vitalik proposed a lot of modifications to make it more practical, especially in the context of the ETH2.0 beacon chain.
Acknowledgment
That’s all! Maximum respect to the father of CBC Casper: Vlad Zamfir, other authors of the original paper: Nate Rush, Aditya Asgaonkar and Georgios Piliouras, and of course, Vitalik Buterin.
Also, we would like to thank Yoichi Hirai for the prior work and Yusuke Ishibashi for supporting us with our questions concerning proofs in Isabelle.
If you are interested in working with us on CBC Casper, please DM me on Twitter!
