Formally Verifying Finality in Gasper: The Core of the Beacon Chain
Gasper is an abstract proof-of-stake protocol layer that is implemented by the Beacon Chain protocol, the underlying protocol of the upcoming Ethereum 2.0 network. A key component of Gasper is a finality mechanism that ensures durability of transactions and the continuous operation of the system even under attacks.
We are happy to report the successful completion of another major milestone in an ongoing collaboration between Runtime Verification and Ethereum Foundation, to build a formal framework for modeling and verifying the Beacon Chain. We have formally proved key correctness properties of finality in Gasper and used these results to show that these properties also hold in an abstraction of Gasper’s implementation in the Beacon Chain. The models and proof scripts are all available online.
In this post, we focus on the first part of this achievement, which is verifying Gasper’s properties. So what’s Gasper? How are its properties formally verified? And why is this important?
Gasper
The Beacon Chain protocol is a new proof-of-stake protocol that is at the heart of Ethereum’s upcoming major upgrade, Ethereum 2.0. In the Beacon Chain protocol, participating nodes, or validators, have a stake (in Ether) in the system. A validator testifies for the validity of a block and votes for several of its properties by submitting attestations to the network. The Beacon Chain protocol implements various gadgets through which validators may achieve consensus on the state of the block chain.
Gasper gives a high-level, but precise, description of the finality gadget in the Beacon chain protocol, which is deciding which blocks are to be considered final and irreversible, in addition to defining the canonical chain if the chain forks (the fork-choice rule). Finality in Gasper generalizes the original Casper Friendly Finality Gadget (Casper FFG) protocol, primarily by allowing a more general form of finalization.
Justification and Finalization
Finality operates only on checkpoint blocks (or epoch-boundary blocks: blocks corresponding to the beginning of epochs). As part of their attestations, validators make justification votes linking a source checkpoint block with a later target checkpoint block, intuitively suggesting that we can move from the source to the target. A justification vote essentially specifies: (1) the voting validator, (2) the source checkpoint block and its justification height, and (3) the target checkpoint block and its justification height.
A target block B1 is justified by a source block B0 if both conditions hold: (1) the source block B0 is already justified, and (2) a supermajority (i.e. at least 2/3 of validators) by stake vote for the same source-target pair B0-B1.
A block B0 is k-finalized (k > 0) if there is a supermajority link from B0 to the k'th descendent checkpoint block Bk and all checkpoint blocks along this chain from B0 to Bk are all justified blocks. Note that the genesis block is assumed justified and finalized. The figure below illustrates the justification and finalization concepts in Gasper.
Slashing Conditions
If a validator attempts to deviate from the protocol and submits conflicting votes to blocks, the validator is penalized by having some significant portion of its deposited stake slashed. Gasper defines two conditions, called the slashing conditions, that characterize conflicting votes:
- Double-voting: A validator publishing two distinct votes with the same target height.
- Surround-voting: A validator publishing a vote within the span of another of its votes.
These are illustrated in the diagram below.
A validator who double-votes is said to have violated the first slashing condition, while a validator that has surround-voted has violated the second slashing condition. In either case, the offending validator will have his stake slashed for this violation.
Correctness Properties
As in other Byzantine Fault Tolerance (BFT) protocols, a key underlying assumption in Gasper is that a super-majority (i.e. at least 2/3) of validators (by deposited stake) are honest and are following the protocol. With this assumption, there are two fundamental correctness properties of Gasper:
- Accountable Safety: No two blocks belonging to two different forks in the blockchain are both finalized unless at least 1/3 of validators (by stake) is slashable.
- Plausible Liveness: Regardless of what happened in the past, the block finalization process can never be deadlocked.
Furthermore, in the context of dynamic validator sets, where the active validator set may change over time allowing validators to join and leave the network, a third property quantifies the slashable stake in case of a violation:
- Slashable bound: A lower bound on how much stake is provably slashable (when safety is violated) in terms of activation and exit parameters that are controllable using external policies.
Dynamic validator sets (which are implemented by the Beacon Chain protocol) introduce another challenging problem: the system is now less likely to be able to provably slash the misbehaving validators since they may misbehave and then leave the network before their deposits are actually slashed. The lower bound given by this property enables adjusting the allowable variability in the active validator set so as to maintain a minimum acceptable level of accountability in the system.
Verifying Finality in Gasper
Gasper aims to provide a mathematically precise description of finality that can be used to formally prove its correctness, which is essential for proving the security of the Beacon Chain protocol. The Ethereum platform is increasingly being used as the backbone of large financial transaction systems, highlighting the ever-increasing importance of ensuring its security.
In collaboration with the Ethereum Foundation, we have formalized the finality mechanism of Gasper in the general setting of dynamic validator sets using the Coq proof assistant. We state and prove all three key properties of Gasper in this setting: Accountable Safety, Plausible Liveness and the Slashable Bound theorem, all in the same Coq model.
Deductive verification of the protocol gives the greatest confidence in the correctness and completeness of arguments, ensuring that there are no unstated assumptions or invalid deduction steps. It makes explicit all the assumptions needed for the arguments to hold. The formalization also feeds back into the description of the protocol making it more precise and complete.
Here we only give a high-level overview of this accomplishment. Complete details can be found in:
- The technical report accompanying the project; and
- The project’s Github repository.
Modeling and Verification Approach
The first step was to build a model of the protocol that would enable us to express all the key properties that we wanted to formally state and prove. The model builds on our previous work on verifying safety and liveness in Casper FFG, which defines an earlier version of the finality mechanism of Gasper.
There are three main structural building blocks of the model:
Validators and quorums. Validators are abstractly represented as members of a finite type (having a finite number of members that can be enumerated), written as Validator : finType. The fact that each validator has a stake in the system is modeled by an uninterpreted function stake : {fmap Validator -> nat} mapping a validator to its stake as a natural number. Furthermore, given a set of validators, its weight wt is defined as the sum of the stake amounts of all validators in the set:
\sum is the summation operator, and stake.[st_fun v] gives the stake amount corresponding to validator v (st_fun is the hypothesis that stake function is total - i.e. every validator must have a stake in the system).
Several properties of the wt function follow from its definition, e.g. the weight of the empty set of validators is necessarily zero, and that weight of the union of two disjoint sets is the sum of their weights. These properties are needed when reasoning about weights in the argument of the slashable bound theorem.
Furthermore, since we intend to model dynamic validator sets where the active set of validators may change across different blocks, we declare an abstract (finite) map vset : {fmap Hash -> {set Validator}} that gives the set of active validators at a block. Now, using vset and wt, we can define what it means for a set to be a supermajority set:
A set is a supermajority set with respect to a block if it’s a subset of the set of active validators of the block with weight at least 2/3 of the total weight.
Block tree. We model a block by a finite type of block hashes Hash : finType, with genesis representing the Genesis block. We model the checkpoint block tree using a parent binary relation using the notation h1 <~ h2, which is axiomatized to mean that h1 is the parent of h2.
This definition is then used to define the ancestor binary relation h1 < as the reflexive, transitive closure of * h2< . Therefore, if h1 <~* h2 then h1 is an ancestor of h2 and h2 is a descendant of h1 (and h1 and h2 can possibly be the same block). Properties about the ancestry relation, such as the property that the ancestor of an ancestor of a block is also an ancestor of that block, follow from it being the reflexive-transitive closure of the parent relation.
Global State. The state is represented by a finite set of justification votes, which are votes of the form (v, s,t, s_h, t_h), where v is the voting validator, s and t are the source and target blocks this vote is for, and s_h and t_h are their attestation heights. Whether a vote has been cast or not can be determined by a boolean membership predicate:
Example Specification
Based on these definitions and their properties, we defined all other structures and properties in the model, including the slashing conditions, the quorum intersection property, and justification and finalization. For example, the property of slashing a quorum due to a violation is defined using abstract membership constraints as follows:
This is a proposition that states that slashing a quorum means the existence of two supermajority quorums vL and vR with respect to some blocks bL and bR respectively whose intersection consists entirely of slashed validators (validators that have double-voted or surround-voted). Note that in the special case that the active validator set is fixed across all blocks, the intersection of these supermajority quorums will have weight at least 1/3 of the total stake.
Another example is the definition of a finalization fork (a violation of safety):
This proposition states that two conflicting blocks b1 and b2 (i.e. neither block is the ancestor of the other) are both finalized. These two blocks may be finalized using finalization chains of any length and at any justification heights.
These definitions and results are ultimately used to state and prove the three key theorems of Accountable Safety, Plausible Liveness and the Slashable Bound. To illustrate, we reproduce below the statement of the Accountable Safety theorem:
The statement simply says that having a violation of safety (a finalization fork of any kind) implies that the a quorum of validators is slashable. The proof mechanizes the informal argument given by Gasper, and shows how a finalization fork means a violation of one of the slashing conditions by two offending supermajority quorums, and hence the slashing of their interaction set. We refer the reader to the technical report describing the formalization and proofs of these properties and to the project repository for the full specification.
Moving Forward
In this post, we described the first part of what we accomplished at Runtime Verification in collaboration with the Ethereum Foundation in the current phase of our engagement. This first part was about formalizing Gasper and proving its three key properties: Accountable Safety, Plausible Liveness and the Slashable Bound theorem, assuming dynamic validator sets. The second part of our accomplishment, which we haven’t talked about here, is showing how these results carry over to a finer-grained model (written in the K framework) that gives an abstraction of the Beacon Chain transition function. We will have another post about this development later.
The completion of this milestone marks another major step towards achieving the ultimate goal of this collaboration, which is to formally prove that the Beacon Chain protocol satisfies all three key properties and have a clear statement of all the assumptions needed at a level of abstraction that is very close to that of the protocol’s specification.
We look forward to continuing our collaboration with the Ethereum Foundation on this work. For this engagement, we have had the great pleasure of working with the following experts at the Ethereum Foundation: Danny Ryan, Carl Beekhuizen, Martin Lundfall, Yan Zhang and Aditya Asgaonkar.
