Safety of CBC Casper consensus
In this essay, we reintroduce CBC Casper with a view to proving the safety of the protocol. Once safety is obtained, we show how the protocol can be designed for consensus over different sets, from binary decisions to blockchains.
A consensus protocol is a mechanism that provides guarantees for a set of communicating agents to agree on something . In the blockchain context, nodes that download new blocks want to make sure they agree on a set of transactions as canonical, a unique history of the system. With Proof of Work (PoW), as soon as a node solves the hashing puzzle with a set of transactions, it can publish this set with a proof of solution to its peers and hope to be included in the canonical chain .
The drawbacks of PoW have been widely covered: its extremely wasteful energy consumption aside, it is not clear that its throughput can be significantly increased while maintaining the same level of security. By making it very difficult to be granted the right to publish a new block, PoW effectively controls writing access to the main chain. Is there another way we could grant this right while maintaining integrity?
Any alternative would need to make it costly to produce faulty, out-of-consensus blocks. In PoW, should you decide to mine out of the main chain, agreed by consensus, your loss will be the work done (solving the cryptographic puzzle) to mine these non-consensus blocks. This loss can very well be measured in dollars and cents, via the energy wasted on the puzzle. Why not cut out the extrinsic penalties and make them intrinsic to the framework?
This is the strategy of Proof of Stake (PoS) . In this paradigm, nodes which participate in the protocol have the option to become validators. To do so, they must agree to lock up a certain amount of capital (in protocol currency, e.g.) and participate collectively in the selection of the canonical next block. If a validator starts acting funny by deviating from the protocol in a malicious way, its deposit is slashed, in true game theory fashion of rewards and punishments.
But for this idea to even be feasible, we need to understand what it means to equivocate. We call validators a set of consensus-forming peers. Validators must reach consensus on the chain and work to maintain a canonical version of the protocol history, in spite of faults. This is the object of the paper by Vlad Zamfir, Nate Rush, Aditya Asgaonkar and Georgios Piliouras . Aditya gave an excellent overview of the paper and its place in consensus research . This post serves instead as a visual walkthrough to see the concepts behind the maths!
When designing systems, more so for multibillion dollars systems, security is fundamental. Testing thoroughly the system is one way to ensure it works as intended. Is it acting in a predictable way? Does a given set of inputs lead to an internal inconsistency (perhaps, a crash)?
The Correct-By-Construction (CBC) methodology takes a different approach. We specify a set of first principles and derive correctness by logical induction from these first principles: the CBC way. To be practically useful, the first principles should not be inconsistent and should be specified by a set of formal rules. From these rules, properties of the system can be derived by formal logic and proven to be correct always.
The CBC way, exposed in the paper, also entails the following: Parts of the system may be left undefined, i.e., await for further specifications. One can prove that some property P holds for mechanisms living in some space S. On a subset of S, say a subcategory of mechanisms S', we may prove some property P', in addition to P, that may not hold for mechanisms in S that are not in S'. For instance, take S to be the space of blockchain consensus mechanisms. Restrict S' to be the space of mechanisms that use the longest chain fork choice rule. We know e.g., that the extra specification (the fork choice rule) gives us consistency, a property P' that may not hold for any other rule. The paper thus starts from a general, abstract specification, of which any part can be further refined to yield additional properties.
CBC Casper's strength lies in the definition of a general protocol space, that each successive refinement can build on and assume to be correct. The initial difficulty here is to understand what the protocol state is. The mechanism needs a few basic elements: weighted validators who send each other messages, to arrive at consensus.
The messages argue about the true value of some object out of a set of possible consensus values, and are sent to reach consensus on this value. A protocol state \sigma is a set of messages. You can think of this set as the messages one node has seen. We say this node is at state \sigma if it saw all the messages in \sigma. The general pattern of a message m is:
  • The estimate c: a consensus value among all possible values \mathcal{C},
  • The sender v: a reference to a validator from the set \mathcal{V},
  • The justification \sigma: a reference to some protocol state \sigma, i.e., a set of messages.
The estimate and the sender of the messages are clear. The justification requires more explanation. By including previous messages in its justification, a message acknowledges that it has seen them. The definition is recursive: a message in some justification must be included along with its own justification. In other words, if I see a message, I also acknowledge the previous messages that it saw. Let us present an example.
It is a tad messy. Representing all connections crowds the network a bit, so we prune edges to show only important, non-redundant ones. By redundant we mean here edges connecting a node already included in the justification of a previously connected node.
Why do we need a justification? The notion of time is not trivial in an asynchronous protocol. While two messages may have been sent in "meatspace" one after the other, there is no guarantee they will be received after some known delay by any other node, or indeed in the same order. State transitions formalize the temporal concept of "after": a state \sigma' follows some other state \sigma if \sigma' includes all messages in \sigma. For instance, there is no state transition from \{(1, B, \{m_1\})\} to \{(1, A, \{m_2\})\} if m_1 is different from m_2.
The set of all possible states following some state \sigma is called the futures cone \texttt{Futures}(\sigma). From \sigma, the protocol may transition to any of the states contained in \texttt{Futures}(\sigma).
Let us think adversarially and consider how an attacker might want to derail the protocol. Consensus happens when participants agree on a value, so an attacker could provide two different estimates in two different messages. Of course, neither message should include the other in its justification, since it does not want to acknowledge that it has estimated a different value elsewhere.
This is what we call equivocating, or in other words, send a pair of distinct messages, neither of which is justified by a state containing the other, as if existing in two different realities. At this point, the protocol can be thought of as branching, or living in two different threads.
In the example above, validator C equivocates. Suppose A notices. It can include both of C's messages in its next message's justification to acknowledge that it has seen seen the equivocation.
Since A includes the equivocating messages of C in its justification, any message that includes A's will also include the equivocation of C. As the execution of the protocol progresses, validators keep on acknowledging that C has equivocated at some point, and thus the weight of equivocating validators, given by F(\sigma) at state \sigma, is nondecreasing . States where the weight of all equivocating validators is lower than some constant t are said to belong to \Sigma_t.
A key theorem tells us that as long as less than t validators equivocate, there is a common future where still less than t validators equivocate. Two protocol states have a common future if each can transition to some shared state. This means that for every honest validator, their "current" state – the justification of their latest message – leads to some other state that can also be reached by all other honest validators. This is good news since it allows us to stay in \Sigma_t and thus know at least one path exists where the number of equivocating validators is still less than t.
When a common future \sigma exists (with equivocation weight smaller than some threshold t), agents must be able to decide what is true in the system. The end goal is to guarantee that agents cannot decide on a property and its opposite: they cannot decide that the consensus value is both 0 and 1. This is the safety guarantee.
A property is decided at some state \sigma if it is true in all futures of \sigma. If some validators equivocate, we want to be certain that unless their weight is larger than some t, the property holds at all states in \Sigma_t that belong to the futures cone of \sigma. Thus, modulo those equivocating, two groups of validators cannot decide on a property A and its opposite \text{not } A.
Of course, if a property is decided at some state \sigma, it is also decided at a state \sigma' that belongs to the futures of \sigma. Conversely, deciding a property at a state \sigma entails that it is not possible to have decided the negation of that property at a state \sigma'' that precedes \sigma.
This is almost enough machinery to prove that nodes at different protocol states cannot decide on a property and its opposite, the safety guarantee. It is easy enough for two agents: either they agree or they each choose one of the (mutually exclusive) alternatives. When we have more than two agents however, it can happen that each pair of agents has consistent decisions, but altogether decisions are inconsistent. Let's see how below.
Suppose that two switches need to be on for a light to switch on. Two agents observe the switches, while the third one observes the light itself. They report that both switches are on, yet the light is off. Every pairwise combinations of report is consistent: that one switch is on does not imply the light is on, and two switches can be observed on at the same time. But the combination of all three is inconsistent: one cannot observe both switches on while the light is turned off. Formally then, a set of properties is consistent if there is a state where all hold at the same time.
The safety guarantee can now be stated. Non-equivocating nodes make consistent decisions on states as long as the weight of equivocating validators is less than t. Safety is proven for decisions on protocol states! A little more machinery takes us from protocol states to actual estimations over consensus values, which is what we really care about. This section is slightly more technical and not presented here, with more details available in the paper for interested readers.
We saw above that Casper CBC defines an abstract protocol specification, made up of validators sending messages to reach consensus. Once we prove some nice properties on this general family of protocols, we can define a bit further some components of the mechanisms to obtain specific protocol instances. This is the magic of CBC: Do the hard work on the foundations and reap the profits downstream!
This part will build on all the definitions we gave above, with the explicit intent of presenting examples of specific protocol instances to illustrate the general framework. The good news however is that we have done a lot of hard work in the previous sections and this part will make some of the more difficult ideas very practical with examples. Before diving in, let’s take a minute to see where we stand.
A group of validators attempts to reach consensus over some object. They can talk to each other by sending messages. Each time a validator sends a message, it has to give an estimate, i.e., state the value it believes should be the consensus value, and provide a justification to its message by referring to some previous protocol state. This justification is none other than a set of previous messages, acknowledging "I have seen these messages, and my new message is a continuation of that". Meanwhile, nodes observe the messages and the protocol state transitions, in an asynchronous fashion: perhaps not everyone has seen the same state, but all states are made of messages referencing earlier states.
Now, if I am a validator, I can derail the protocol by doing the following. I send two different messages m and m', none of which references the other, estimating different values. Here I am basically saying "I am continuing history with m. But m' belongs to a different world, where history continues with m' instead". This is an equivocation fault. The protocol now runs two different versions (or threads), none of which is compatible with the other.
The problem with equivocation is that if validators start saying everything and its opposite (tout et son contraire), a consensus failure may occur. Nodes decide on something if they hold it to be true from a certain state onwards. How do we guarantee that these decisions will not be inconsistent?
The answer lies with the safety guarantee. We give ourselves some weight t, and assume that among all states observed by our nodes, the total weight of validators that have equivocated there is less than t. Then, by the safety guarantee, we know that there is a common future for the nodes and thus the nodes cannot make contradictory decisions. For more details on how the threshold t determines how final decisions are, check out our post on the Inspector!
We stand on solid ground with the protocol specs and its safety guarantee, it is time to make good use of it all. The protocol is developed to reach consensus and this is what we turn our attention to now.
When validators send messages, they estimate a certain value should be decided as consensus. On the other hand, dishonest validators can derail the protocol by estimating two different values. This entails that validators that do not equivocate will always have at most one latest message – they can have none if they have never spoken, or if their messages are not observed in a particular state. If they are observed in the state however, there is only one such latest message. The consensus is argued over this set of honest observed validators’ messages.
After we collect the latest messages of observed honest validators, we can move from the protocol state to the consensus values. We can map validators to their own estimate, or to the empty set if the validator is not observed or if it is equivocating. The estimate is the consensus value they have included in their latest message.
An estimator returns a set of consensus values from a protocol state . An estimator is latest honest estimate-driven if it only looks at the latest estimates of honest validators. In the following, all our estimator will be latest honest estimate-driven, thus providing the missing link between a protocol state and its estimated consensus value.
What do we have left to do? We proved that nodes cannot decide on contradictory consensus values unless the weight of equivocating validators is too high. We saw that validators who play nice and are included at some state of the protocol have sent only one latest message each. Finally, we mapped these latest messages to the consensus value they are estimating.
It is now time to specify what exactly is the set of values we arguing over, and how consensus is reached from the estimates of observed honest validators.
The simplest of the family of minimal CBC Casper protocols, the binary consensus, asks of validators to choose between two values, say, 0 and 1. The consensus value is obtained from a simple majority rule. Here, we give each validator v some weight \omega(v). Weights are tallied up for those who estimated value 0 vs. those who estimated value 1, with the heaviest set determining the consensus. Note that in case of a tie, both values are returned: remember that the estimator returns a subset of the set of consensus values, and this subset can have multiple elements.
The logical next step is to reach consensus over a set that contains more than 2 elements. In this version, validators estimate the value of an integer. We could again take the value returned by the heaviest set of validators, as we did for the binary consensus protocol. However, this might not best represent the idea of consensus, as the mode of a distribution (its highest peak) can be quite different from its mean or its median.
The paper chooses to estimate the median. Each integer is weighted by the total weight of the validators which returned that integer. The estimator then returns the median over these weighted integers. The weighted median is roughly obtained by returning an integer such that less than half of the total weight of all validators is below it, and less than half of the total weight of validators is above it. A drawing may help!
Seemingly, we have strayed rather far from the blockchain issues that motivated all this in the first place. Rest assured, however, that with all this power in our hands, we can very quickly adapt Casper to fit in a more blockchain-oriented framework. Its first application is to the fork choice rule nicknamed GHOST , for Greedy Heaviest Observed Sub-Tree (can you see the connection with Casper? 👻)
GHOST is particularly helpful for blockchains that tend to add blocks very rapidly. Unlike Bitcoin which adds a block on average every 10 minutes, Ethereum does so every 10 to 20 seconds (around 15 seconds, at the time of writing). This naturally increases the uncle rate, i.e., the rate at which valid blocks are produced which are not included in the main chain . Under the GHOST rule, parent blocks may have several children, all included in the canonical main chain. Since I am a decidedly visual person, I refer you to a great animation by Michael Birch .
What is the set of possible consensus values this time? The set of all possible blocks, starting from some genesis block g! This seems like a step-up from a few integers, and yet, armed with the GHOST rule and the few mechanisms we developed just previously, it is quite natural. When block b belongs to some state, one can compute b’s score by looking at the sum of weights of validators who return one of b’s descendants as estimate. This is OK, since we want the heaviest subtree.
Now, for the greedy part, we start from the genesis block g and get its best children, i.e., the children with the highest score, and recursively their own best children, etc., until we arrive at a leaf. At this point, GHOST returns a set of best leaves, which is exactly what we asked of our consensus protocol: tell us where to build next!
You should observe the similarity with the integer consensus of Section . There, we picked out of the set of all possible integers the weighted median of our validators' estimates. Here, the GHOST rule returns a block among all candidates, fitting the definition of an estimator like a glove.
The paper goes on to provide another flavor of Casper, known as FFG, the Friendly Finality Gadget. If you have already heard of it before, it is because it is actively discussed and researched on at the moment by the Ethereum community. It started as a consensus gadget on top of PoW, but was recently redesigned to allow for full PoS on top of sharding. It is a super interesting topic, and a very recent paper by Vitalik Buterin, Daniël Reijsbergen, Stefanos Leonardos and Georgios Piliouras makes the case for the cryptoeconomics of deposits and rewards in the Ethereum Casper finality gadget .
Since we mentioned sharding, it is in fact entirely possible to apply the CBC Casper framework directly to it. Vlad Zamfir has been doing some work towards this, including another cool visual for parent and child chains working together, with Alex Skidanov of NEAR Protocol .
Finally, a specification of CBC Casper for light clients would guarantee the safety of a blockchain where validators may not have access to the full history of protocol states. This is an extremely powerful technique to reduce the storage requirements of a node as well as associated computation overheads and an active research question today.