Editor's Note: This article comes fromEthereum enthusiasts (ID: ethfans)Editor's Note: This article comes from

Ethereum enthusiasts (ID: ethfans)

Ethereum enthusiasts (ID: ethfans)

Gasper is an abstract proof-of-stake protocol layer implemented by the beacon chain protocol (the underlying protocol of the upcoming Ethereum 2.0 network). The key part of Gasper is a set of finality mechanism, which is used to ensure the durability of transactions and the uninterrupted operation of the system will not be damaged by attacks.

Gasper

We are happy to announce another milestone in the long-term collaboration between Runtime Verification and the Ethereum Foundation: we developed a formal framework to simulate and verify the beacon chain protocol, and successfully formally proved Gasper finality correctness; and, we also use these results to demonstrate that the Gasper abstraction implementation of the beacon chain also possesses these properties. Both the model and the proof script can be found here.

first level title

The beacon chain protocol is a new set of proof-of-stake protocol, which is the core of Ethereum's future major upgrade "Ethereum 2.0". In the beacon chain protocol, participating nodes (or "verifiers") all have deposits (stake, in the form of ETH) in the system. Validators confirm the validity of blocks and vote on various attributes by submitting "attestations" to the network. The beacon chain protocol itself includes several tools to help validators reach a consensus on the latest state of the blockchain.

Gasper proposes an abstract but precise description of the finality gadget in the beacon chain protocol, and also defines fork selection rules; the finality gadget is used to determine which blocks should be considered finalized by participants The fork selection rule is used to determine which fork is the main chain when the chain forks. Finality in Gasper generalizes a concept that originated in the "Casper Friendly Finality Gadget (Casper FFG)" paper, giving "finalization" a more general form.

secondary title

Justification and Finalization

The concept of finality is only relevant to "checkpoint blocks" (also called "epoch boundary blocks", which are blocks at the beginning of an epoch). Part of the attestation message is called "rationalization vote". In the rationalization vote, the verifier associates a source checkpoint block with a later target checkpoint block, visually indicating that The validator who initiated the attestation believes that "we can move from the state of the source checkpoint to the state of the destination checkpoint". In effect, a justification vote shows: (1) the validator who initiated the vote; (2) the source checkpoint and its justification height; (3) the target checkpoint and its justification height.

If and only if the conditions are met: (1) the source checkpoint B0 has been rationalized; (2) the majority (i.e. at least 2/3 of the validators) also voted for the B0-B1 source-target pair; then the target checkpoint B1 It is rationalized via source checkpoint B0.

• B0 achieves order-K finality (k > 0) and all checkpoints between B0 and Bk are finalized if and only if a majority of validators associate B0 with its K-generation descendant checkpoint Bk. Note that the genesis block itself is considered both rationalized and final. The diagram below demonstrates the rationalization and finalization concepts in Gasper.

• If a validator tries to deviate from the protocol and submit contradictory votes, the validator is penalized: a large portion of its deposit is deducted. Gasper defines two conditions (also known as slashing conditions) to define what constitutes a contradictory vote:

Surround-voting: The two checkpoints associated with a vote issued by the validator are exactly within the height range of two checkpoints of another vote issued by the verifier.

text

A validator who initiates a double vote is considered to have violated the first slash condition; a validator who initiates a wrap vote violates the second slash condition. In either case, validators who break the rules will have a large amount of their deposit deducted.

• secondary title

• Correctness (Correctness Properties)

Like other Byzantine Fault Tolerance (BFT) protocols, a key underlying assumption of the Gasper protocol is that the vast majority of verifiers (more than 2/3, defined by the amount of deposit) are honest and will follow the requirements of the protocol. Under this assumption, Gasper has two basic properties:

Accountable Safety: No two blocks belonging to different forks will be finalized unless at least 1/3 of validators (in terms of deposit amount) are slashed;

Plausible Liveness: No matter what happened to the blockchain in the past, the finalization process of the block will never be deadlocked.

Furthermore, in an environment where the set of validators changes dynamically (as validators leave the network and new validators join, the set of active validators may change), the third property quantifies when someone violates the rules of the protocol. The amount of security deposit that can be confiscated:

Slashable bound: As long as extra-protocol conditions can be used to control validator activation and exit parameter conditions, it can be proved that (when breaking security) there is a lower bound on the amount of deposit that can be slashed.

A dynamic set of validators (which is what the Beacon Chain protocol implements) introduces another challenging problem: the system is no longer able to reliably punish malicious validators, since they may be able to do so after they have done something bad but before their deposit is actually slashed. leave the network. The slashable lower limit property makes it possible to adjust the variable range of the active validator set and maintain a minimum level of accountability.

Verify the finality of Gasper

Gasper aims to provide a mathematical, precise description of finality that can be used to formally prove its correctness; this correctness is also the key to proving the security of the beacon chain protocol. The Ethereum platform is increasingly being used as a stock price for large financial trading systems, highlighting the unprecedented importance of security guarantees.

1. In collaboration with the Ethereum Foundation, we have formalized Gasper's finality mechanism under the general condition of dynamic validator sets using the Coq proof helper. We point out and prove all three key properties of Gasper under this condition: accountable safety, likelihood liveness, and slashable lower bound; all proofs use the same Coq model.

2. Here we only give a brief account of this achievement. Full details are available at:

Technical report on the project

The project's Github repository

secondary title

Modeling and Verification Methods

The first step is to develop a model of the protocol that allows us to express all the key properties that we wish to formally state and prove. This model builds on our previous work validating the safety and liveness of Casper FFG (the previous model had defined an early version of the Gasper finality mechanism).

This model has three main structural modules:

\sum is the sum operator; stake.[st_fun v] gives the amount of stake corresponding to validator v (st_fun assumes that every validator must have a stake in the system).

In addition, because we want to simulate a dynamic set of validators, that is, the set of active validators may change from block to block, we declare an abstract (limited) mapping vset: {fmap Hash -> {set Validator}}, Given the set of active validators at a block. Now, using vset and wt , we can define what a supermajority set is:

At a certain block, if the weight of a subset of the set of active validators exceeds 2/3 of the weight of the entire set, then the subset is an absolute majority set.

block tree. We use the finite type of block hash to simulate a block Hash:finType, and use genesis to represent the genesis block. We use the notation h1 <~ h2 to represent block parent-child relationships (h1 is the parent of h2) to simulate a checkpoint block tree.

Next, we use h1 <~* h2 to define the ancestor relationship, h1 is the ancestor of h2, and h2 is the descendant of h1 (h1 and h2 can be the same block). As for the attributes of the ancestor relationship, for example, the ancestors of the ancestors are also ancestors, which are similar to the attributes of the father-son relationship.

text

secondary title

Based on these definitions and their corresponding properties, we define all other structures and properties in the model, including penalty conditions, quorum intersection properties, and rationalization and finalization. For example, the property of confiscating a community in the event of a protocol violation can be defined using the following abstract membership constraints:

The proposition states that slashing a group means that there are two supermajority groups vL and vR at some blocks bL and bR, and the intersection of these two groups is the slashed validator (initiated double voting or surround voting) The complete collection of . Note that under the special condition that the set of active validators is always fixed, the weight of the intersection of these supermajority sets is at least 1/3 of all deposits.

Another example is the definition of a finalizing fork (i.e. a security violation):

This proposition states that two contradictory blocks b1 and b2 are both finalized (because neither b1 nor b2 is an ancestor block of the other). These two blocks can be finalized by an arbitrarily long chain at any rationalization height.

These definitions and sets of results are used to point out and prove three theorems of accountability security, likelihood activity and slashable lower bound. For clarity, we also redefine the formulation of the accountability security theorem as follows:

The definition is simple and just says: if security is broken (with any finalized fork), it must mean that some validator set is slashed. This proof mechanizes the informal argument given by Gasper, and shows why forks being finalized means that there must be two supermajority groups that violate one of the slashing conditions, so their intersection can be slashed.

text

Our technical report describes the formalization process and proofs of these properties, while our project code repository provides a full specification.

first level title

keep going