The Inspector: An efficient finality test for CBC Casper
Finality in CBC Casper is an emergent property of message-passing communication in the network. We explore how different degrees of finality can be tested by the Inspector.
This essay will explore the question of finality in CBC Casper . CBC Casper is a protocol that allows validators to reach consensus on some value, for instance, the state of a blockchain. It is critical that consensus reached at some point cannot be reverted later: this property is called finality .
Intuitively, finality says that a transaction all parties believe was executed cannot be reverted later in the future. We explore in this essay how finality is reached as a property of the messages passed by validators and how this property can be tuned to be more or less stringent. Although this excursion is self-contained, we also prepared a general introduction to consensus and finality for CBC Casper.
We do not assume you know anything about blockchains, finality or CBC Casper. In fact, the remainder of the discussion will not be concerned with blockchains at all, although it is applicable there too. But as a primer for some, and a refresher for others, we prepared a five-minute introduction to CBC Casper, which can be expanded right below. Give it a try!
If you followed our essay on consensus and finality, you know that unfortunately, finality is not achieved when all validators agree on one consensus value. We need in addition that validators acknowledge the agreement; otherwise, undelivered messages could tilt consensus another way.
Indeed, think of two friends, Alice and Bob, who know they must meet either at the cinema or at the park. Alice writes to Bob that she will be at the cinema, and Bob writes the same to Alice. They are in agreement and yet, Bob's phone has a very unstable network, with a long wait before sending or receiving messages. Not knowing where Bob is going, but knowing he definitely prefers to go to the park, Alice might instead decide to head there and write back to Bob that she is going to the park. This is a situation where although both agreed at some point, the agreement is not final.
Contrast this with the case where both Alice and Bob receive their friend's message. This situation is much more stable as both expect the other at the cinema. It is even more stable if both write back that they received the initial message, etc. This idea of layers is exploited by the Inspector, a finality test for CBC Casper. The more layers of acknowledgement, the more final a decision.
We first introduce the simplest meaningful test for finality. We look for a pattern where validators all agree on a value and all acknowledge the agreement. In other words, the pattern we look for is a complete bipartite graph , as pictured here.
But take a message transcript where 7 validators attempt to reach consensus on whether Blue or Red is the correct value. The color of a circle is the value estimated by the validator in its message.
Let's first discuss what we see here. Validators send messages, with older messages on the left and newer messages on the right. Each row contains the messages of one validator. This sample data is obtained by having validators speak once each in a predetermined sequence. When all validators have spoken, they start the sequence again, until we obtain all the messages presented here.
What do validators say when they speak? First, they observe past messages according to the following principles:
  • A validator always observes its own last message.
  • There is a 15% probability that a validator observes each message sent since the last time it spoke.
  • If a validator observes a message m, it observes all messages referenced in m.
  • No one ever equivocates, so all validators have exactly 0 or 1 latest message.
These assumptions model for instance a situation where all validators are honest but latency in the network prevents them from receiving some messages.
After observing a set of messages, the sending validator must provide an estimate for the consensus value, based on the latest message of each validator. If, for instance, it has never received a message from validator v, then it ignores v. The sending validator tallies up the estimates contained in the latest messages it has received. If a strict majority of the latest messages estimate Blue, then the sending validator estimates Blue, and same for Red. If however, no strict majority exists for either color, the validator chooses between Blue and Red randomly. Hover above a message in the graphs to see the messages that justify its estimate!
This tiny graph does not even begin to represent just how many validators and messages will be part of a blockchain consensus, but already finding such a pattern as in Image 1 is hard: the algorithmic time to find one is exponential in the number of messages . We need a better algorithm to do so.
Fortunately, we have more structure: the graph can be partitioned by validator, assigning each message to its original sender. From there, we can find for each validator the messages after which they always estimate the consensus value. Let us call these messages level 0 and reveal them in the graph below.
When do validators acknowledge a final decision? We could check for validators who acknowledge level 0 messages from other validators. In particular, we could call level 1 a message for which a large number q of latest messages in its justification are level 0, where q is a quorum. This is beginning to look like a clique.
This looks like a multidimensional Minesweeper, but we keep going and call level 2 a message which acknowledges at least q level 1 messages in its justification.
We are looking for a committee—a set of validators—with the following property. Each member of the committee must have a level 1 message from the committee, meaning that its level 1 message must be justified by at least q level 0 messages from other members of the committee. Notice that validator 4 does not have a level 1 message, and thus cannot be part of the committee in any case. We ignore it and recompute the level of all messages.
Ignoring validator 4 changes the levels of the messages! The level 2 message is now level 1 only. Still, all remaining validators have a level 1 message, and thus form a committee satisfying the property we spelled out above: "Each member of the committee must have a level 1 message from the committee".
This procedure is the key to the algorithm. We successively ignore validators who do not have a message at level k, for some k fixed. If we ignore enough validators that the number of remaining ones falls below our quorum q, then we will never have level k for q. But the procedure can also stop as it did in the previous example, leaving a "closed" committee of validators, where messages are justified by other messages from the committee.
What does that tell us? We have a committee S of 6 validators such that all members of that committee have a level 1 message, one that cites at least q = 5 level 0 messages from validators in the committee. We set q to be larger than the majority of validators. We will not provide the proof, but this buys us the guarantee that if validators from that committee later send a message disagreeing with the current consensus value, then it must be the case that at least a certain number t of validators has equivocated. Another way of saying it: unless more than t validators equivocate, whatever the committee says must have a majority of the non-equivocators agree with the consensus value. This property is called t-finality.
The construction above works for levels above k = 1. The more layers of acknowledgement exist, the harder it is for validators to break the consensus. This relationship is expressed in t: the higher level k a committee is good on, the more equivocating validators t are needed to break the consensus. Same goes with q: a higher quorum means again that more equivocating validators t are needed to break the consensus. If we have n validators, the precise formula is
t = 2 (q - n/2) (1 - 2^{-k}) \, .
Assuming our quorum contains 3/4 of validators, we need equivocation from t = \frac{1}{2} n (1 - 2^{-k}) validators to make consensus unstable. The next image plots the relationship.
The relationship between t and q is more often inverted in CBC Casper. Instead of taking q as input to determine a level of finality based on the quorum size, clients running the protocol set some threshold t and determine q from it. For instance, a client can set a finality threshold corresponding to t = 3n/4 validators acting maliciously, which requires for, say, k = 2
\begin{aligned} t \leq 2 (q - n/2) & (1 - 2^{-2}) = 3/2 (q-n/2) \\ & \Leftrightarrow q \geq 2t/3 + n/2 \\ & \Leftrightarrow q \geq n \, . \end{aligned}
Here, the quorum must be exactly equal to the number of validators participating in the consensus to guarantee such finality at level 2. You should take away from this that aiming for a higher t-finality requires either more depth of acknowledgments (a higher k) or a wider quorum (a higher q). We end this essay with some examples to show how finality is violated when over t validators equivocate.
We look back at Section , where we had 4 validators agree on the value Blue and all acknowledging the agreement. Thus, this committee of size 4 has level 1 messages for a quorum q = 4. By the formula above, this guarantees t-finality for
t = 2 (q - n/2)(1-2^{-k}) = 2 \cdot (4 - 2) \cdot (1-1/2) = 2 \, .
After the committee of 4 validators has reached finality at level 1 on Blue, validator 1 suddenly sends a message estimating Red. If we assume validator 1 is honest, i.e., has not equivocated and always has exactly one latest message, it must cite in its new Red message validators who have equivocated.
CBC Casper defines simple primitives for consensus. Validators send and receive messages which are justified by previous messages. Messages contain estimates, the value believed by the sender to be the consensus. Users interacting with the protocol must be certain that once validators do agree on a value, they will not change their mind later, a property called finality.
The work done here presents a way for clients, who listen to the messages sent by the validators, to detect when finality is reached. Surprisingly, finality is not a binary property, but can be tuned by the clients to be more or less stringent. A client with a very high threshold may not accept as final a value which a client with a lower threshold does. Still, all clients must have an efficient way of computing whether a value is final or not, and can do so from the messages alone. For this reason, we characterize finality as an emergent property arising from a set of messages that is connected enough.
Exciting avenues open from here:
  • What are the dynamics and (economic) properties of a protocol when different clients set different thresholds?
  • In this essay, we always compute from a complete transcript of messages the levels of agreement. In reality, an optimized procedure can take advantage of the fact that messages are a stream, and store for instance the current level of a message while making fewer updates with new messages.
  • Can any of this be ported to light clients who may not have access to the full transcript?