PaperlayerView exact revision on arXiv

Source-linked AI summary

Combining GHOST and Casper

Vitalik Buterin, Diego Hernandez, Thor Kamphefner, Khiem Pham, Zhi Qiao, Danny Ryan, Juhyeok Sin, Ying Wang, Yan X Zhang

arXiv:2003.03052v3cs.CR

TL;DR

The paper addresses how to construct a proof-of-stake consensus protocol for Ethereum’s beacon chain. It presents Gasper by combining Casper FFG with LMD GHOST and proves safety, plausible liveness, and probabilistic liveness under stated assumptions. The analysis also identifies implementation and modeling boundaries relevant to interpreting those guarantees.

  • Problem

    The paper seeks a proof-of-stake consensus protocol for Ethereum’s beacon chain that combines finality and fork choice while supporting formal safety and liveness analysis.

  • Method

    Gasper combines Casper FFG for finality with LMD GHOST for fork choice, adapting the design to epoch-based proof-of-stake time and validator committees.

  • Results

    The paper proves safety, plausible liveness, and probabilistic liveness for Gasper under different assumptions.

  • Takeaways & Limitations

    Gasper provides a formal proof-of-concept for a full proof-of-stake blockchain design combining Casper FFG and LMD GHOST.

  • Takeaways & Limitations

    The probabilistic-liveness analysis assumes equal stake per validator and does not jointly analyze possible implementation patches.

Abstract

from arXiv · show

We present "Gasper," a proof-of-stake-based consensus protocol, which is an idealized version of the proposed Ethereum 2.0 beacon chain. The protocol combines Casper FFG, a finality tool, with LMD GHOST, a fork-choice rule. We prove safety, plausible liveness, and probabilistic liveness under different sets of assumptions.

1 Introduction

The paper aims to build a proof-of-stake consensus protocol for Ethereum’s beacon chain and presents Gasper as an idealized combination of Casper FFG and LMD GHOST. It outlines formal proofs of the protocol’s desired properties and differences from Ethereum’s planned implementation.

  • The paper’s goal is a proof-of-stake consensus protocol for Ethereum’s beacon chain, also usable for a solo blockchain without sharding.
  • Gasper combines Casper FFG’s finality gadget with LMD GHOST’s fork-choice rule as a full proof-of-stake protocol.Casper FFG finalizes blocks, while LMD GHOST uses validator attestations to signal block support.
  • The paper defines the protocol, presents its main construction, and formally proves its desired qualities.
  • It also compares Gasper with the planned Ethereum implementation, including attestation delays, delayed finalization, and dynamic validator sets.

2 Setup and Goals

The paper models blockchain consensus as agreement on one chain despite conflicting blocks, unreliable networks, and potentially malicious validators. It formalizes validators, signed messages, dependencies, views, and proof-of-stake incentives for the subsequent protocol analysis.

  • 2.1 Consensus Protocols, Validators, Blockchain: Consensus protocols seek an agreed history despite unreliable networks and potentially malicious validators.
  • 2.1 Consensus Protocols, Validators, Blockchain: Conflicting blocks can arise from network latency or Byzantine behavior, so consensus requires choosing one accepted chain.
  • 2.2 Messages and Views: Validators broadcast digitally signed messages that may propose blocks, attest to blocks, activate validators, or prove misconduct.
  • 2.2 Messages and Views: A validator’s view contains accepted messages it has seen, while dependencies determine whether messages are accepted.
  • 2.2 Messages and Views: Accepted blocks form a rooted tree from genesis, with parent-child edges, leaf blocks, and chains defined by parent relationships.
  • 2.3 Proof-of-stake: Proof-of-stake assigns voting power according to bonded stake rather than computational power, requiring additional theory to address incentives.

3 Main Ingredients

The protocol combines Casper FFG’s checkpoint-based finality mechanism with LMD GHOST’s attestation-weighted fork choice. Casper provides accountability and plausible liveness, while LMD GHOST selects a canonical chain from observed validator support.

  • 3.1 Casper FFG: Casper FFG is a finality gadget that marks blocks finalized while remaining agnostic to whether the underlying blockchain uses proof-of-work or proof-of-stake.
  • 3.1 Casper FFG: Checkpoints occur at heights divisible by H, and attestations vote on directed edges between checkpoint blocks with stake-based weights.
  • 3.1 Casper FFG: A checkpoint becomes justified after a justified predecessor receives attestations totaling at least 2/3 of validator stake.
  • 3.1 Casper FFG: A justified checkpoint is finalized when it has a supermajority link to the next checkpoint height.
  • 3.1 Casper FFG: Casper’s accountable safety prevents conflicting finalized branches unless validators controlling sufficient stake violated slashing conditions, while plausible liveness permits new finalization when blocks can be created.
  • 3.2 LMD GHOST Fork-Choice rule: LMD GHOST repeatedly follows the heaviest observed subtree according to validators’ latest attestations until it reaches a leaf, defining the canonical chain.

4 Main Protocol: Gasper

Gasper combines Casper FFG’s finality mechanism with an LMD GHOST-based fork-choice rule in a proof-of-stake blockchain protocol. Its design uses epoch boundary pairs, rotating committees, proposer and attester duties, and local views to coordinate chain growth and finality.

  • Gasper combines GHOST and Casper FFG, using the former for fork choice and the latter for justification and finalization.Justification and finalization operate on epoch boundary pairs rather than checkpoint blocks alone.
  • Epoch Boundary Blocks and Pairs: Epoch boundary pairs identify a block together with an epoch because the same block can serve as a boundary block in multiple contexts.A block’s boundary-block status can depend on the chain containing it, while its slot-based epoch remains local to the block.
  • Slot Responsibilities: In each slot, a designated proposer extends the locally selected chain head, while every committee member attests to the head using HLMD GHOST.Blocks include their slot, parent pointer, and previously accepted attestations not already included by ancestors.
  • Committees: Each epoch pseudorandomly partitions validators into C committees, with one committee assigned to each slot.The permutation ρj assigns N/C validators to each committee and partitions all validators across the epoch’s committees.
  • Fork Choice: HLMD GHOST takes a validator’s view and returns a leaf block whose chain becomes canonical, using the fork-choice rule’s subtree-weight heuristic.Both block proposers and attesters run the rule on their own views, which may differ because messages arrive with latency.

4.5 Finalization

Gasper finalizes epoch boundary pairs through sequences of adjacent justified pairs linked by supermajority attestations. Its hybrid fork choice freezes the relevant justification state and excludes branches that have not caught up, while slashing conditions support uniqueness and honest participation.

  • Finalization: A pair is k-finalized when it begins a sequence of adjacent epoch boundary pairs whose earlier pairs are justified and whose final link is a supermajority link.The definition includes the genesis pair and allows k≥1 to accommodate delayed attestations and network latency.
  • Finalization: 1-finalization is expected most of the time, whereas k=2 handles attestation delays and k≥3 is mainly illustrative.The planned implementation cited in the paper does not include finalization for k≥3.
  • Hybrid LMD GHOST: The final fork choice starts from the highest-attestation-epoch justified pair among leaf views, restricts the graph to compatible branches, and then follows latest-attestation weights.Header-hash tie-breaking makes the returned choice deterministic when branches have equal weight.
  • Hybrid LMD GHOST: Algorithm 4.2 freezes the latest justified pair at epoch beginnings and filters out leaf branches whose justification has not caught up.These changes address prototype instability during epochs and pathological forks that could make an honest validator violate slashing condition S2.
  • Slashing Conditions: At most one pair can be justified per epoch unless the view contains evidence sufficient to slash at least one-third of total stake.Under that condition, the justified pair selected by Algorithm 4.2 is unique and well-defined, and honest validators do not accidentally violate the slashing rules.

5 Safety

Gasper’s safety theorem shows that conflicting finalized blocks imply slashable behavior, under persistence of finalization and inclusion of finalized blocks in the canonical chain. The proof relies on the structure of justified and finalized epoch boundary pairs.

  • Supporting Lemma: A finalized pair and a later justified pair must be ordered ancestrally unless the view is (1/3)-slashable.This is Lemma 5.1, which supplies the ordering relation needed by the safety proof.
  • Safety Theorem: Theorem 5.2 states that if finalization persistence or canonical-chain inclusion fails, the view is (1/3)-slashable.The two required properties are that finalized pairs remain finalized as the view updates and that every finalized pair’s block lies on the canonical chain.
  • Safety Proof: Because finalization is persistent and the canonical chain passes through the highest justified pair, finalized blocks remain on one canonical chain across future views.The proof then reduces safety to showing that no two finalized blocks conflict.
  • Safety Proof: Conflicting finalized blocks imply two incompatible justification structures and therefore evidence that validators violated the slashing conditions with at least one-third stake.The proof applies Lemma 5.1 to the later finalized pair and derives a contradiction unless the chain is slashable.

6 Plausible Liveness

Gasper has plausible liveness when at least two-thirds of stake is honest: under good synchrony, honest validators can repeatedly create stable epoch-boundary chains and finalize new pairs. The argument extends Casper FFG’s finality reasoning to Gasper’s underlying protocol.

  • Plausible Liveness: With at least 2N/3 honest stake, a new block can always plausibly be finalized while honest validators continue following the protocol, regardless of prior blockchain events.This is the paper’s plausible-liveness theorem.
  • Stable Chains: Good synchrony can make validators share a view at an epoch boundary, allowing an honest proposer to extend the block selected by HLMD.The new block becomes the epoch boundary block for the current epoch.
  • Justification: If at least two-thirds of stake is honest, it is plausible that validators attest to the new block or a descendant, creating a supermajority link that justifies it.The attestations can be included in the next epoch boundary block under good synchrony.
  • Finalization: A stable chain with consecutive supermajority links can finalize the preceding epoch-boundary pair through 1-finalization.The next epoch boundary block carries the link from the justified pair to its adjacent successor.
  • Scope: The plausible-liveness analysis extends Casper FFG’s finality focus because Gasper also supplies the underlying proof-of-stake blockchain and seeks probabilistic liveness for it.Casper FFG assumed a probabilistically live underlying blockchain rather than proving that property itself.

7 Probabilistic Liveness

Gasper’s probabilistic-liveness proof separates success into three stages: obtaining a high-weight block, justifying it, and eventually finalizing a block. The analysis uses explicit assumptions and concentration bounds, while finalization abstracts justification probability into an independent parameter.

  • Proof strategy: The proof proceeds from high weight after the first slot to probable justification, then from probable justification to probable finalization.Under favorable conditions, a high-weight block is likely to gain an increasing advantage over competitors and become justified; repeated likely justification makes finalization increasingly probable.
  • Limitations: The probabilistic analysis depends on parameters and assumptions that differ from the planned Ethereum 2.0 implementation, including equal stake per validator and an attestation consideration delay.The authors present the pure-protocol analysis as a proof of concept whose proof strategies may generalize, rather than as a mathematical guarantee of the actual implementation.
  • 7.1 High Weight After the First Slot - The Equivocation Game: The equivocation game models the first slot with two voting options and encodes liveness assumptions separately from later liveness results.Simulations examine pessimistic, optimistic, and intermediate regimes; under reasonable conditions, one option is likely to obtain 2N/3 stake after the first slot.
  • 7.2 High Weight after First Slot Leads to Justification: Under A(ϵ), any newly justified block must descend from the last justified block, preserving progress along the existing justified chain.Lemma 7.3 and the subsequent argument establish this descendant relation for the view at the end of the epoch.
  • 7.2 High Weight after First Slot Leads to Justification: With probability r, a winning block receives at least 2S/3 attestations after the first slot and then accumulates honest validators’ attestations in subsequent slots.The proof tracks honest and dishonest attestors per slot and uses concentration inequalities to control deviations from expected committee composition.
  • 7.3 Probabilistic Justification Leads to Probabilistic Finalization: Theorem 7.5 shows that if each epoch independently justifies a block with probability p ≥ 1/2, failure to finalize over n epochs decreases exponentially with n.The result is agnostic to how p was obtained; for p = 0.5, the probability of finalizing a block is around 99% after n = 20 epochs.

8 Practice versus Theory

Gasper is a mathematically tractable idealization of Ethereum 2.0, while the planned implementation adds practical delays, reduced finalization rules, and dynamic validator sets. These changes affect liveness, implementation risks, and the strength of safety guarantees.

  • Practice versus Theory: Ethereum 2.0’s implementation differs from Gasper because Gasper isolates the beacon chain’s theoretical core for mathematical analysis.The implementation includes design choices whose combined rigorous analysis would be substantially messier.
  • Implementation Risks: Software errors in interpreting views, stores, and state are outside Gasper’s mathematical guarantees and can independently threaten safety and liveness.The actual beacon chain updates its store from blocks and attestations and maintains a stake-related state structure.
  • Attestation Delays: The implementation delays attestation inclusion and fork-choice consideration to improve dissemination, decentralization, and resistance to timing attacks.Inclusion delays can be tuned between 1 and 4 slots; consideration delay ignores attestations from the current slot.
  • Attestation Delays: The attestation consideration delay improves probabilistic-liveness guarantees by neutralizing the first-slot equivocation game.If an honest validator is selected to propose a block, with probability at least 2/3 in the worst case, all honest validators vote for it in the first slot.
  • Four-Case Finalization Rule: The practical finalization rule reduces Gasper’s general rule to four cases involving only recent epoch-boundary blocks.The implementation honors attestations for up to two epochs, yielding the four cases illustrated in Figure 8.
  • Dynamic Validator Sets: Dynamic validator sets preserve the core slashing argument, but conflicting finalized blocks imply slashability through overlapping two-thirds stake subsets.The corresponding theorem states that conflicting finalized blocks provide evidence sufficient to slash validators with substantial total weight, while broader bounds expose a tradeoff between validator flexibility and accountability.

9 Conclusion

The paper presents Gasper as a complete proof-of-stake blockchain protocol combining LMD GHOST and Casper FFG, separating mathematically clean analysis from implementation details. It proves core safety and liveness properties while noting that implementation patches and validator-set design require reassessment.

  • 9 Conclusion: Gasper combines LMD GHOST and Casper FFG into a full proof-of-stake blockchain design.Casper FFG provides finality, while LMD GHOST is the fork-choice component.
  • 9 Conclusion: The analysis separates Ethereum 2.0’s mathematically clean protocol foundations from implementation details.The authors analyze implementation changes largely as isolated modifications.
  • 9 Conclusion: The paper’s analytical techniques may also support studies of other protocols, including probabilistic liveness proofs and equivocation-game constructions.
  • 9 Conclusion: Implementation patches can change safety or liveness assumptions, and interactions among otherwise innocuous patches can be undesirable.The authors therefore recommend reassessing the implications of patches that become core to the protocol.
  • 9 Conclusion: The design balances simplicity, understandability, practicality, safety, and liveness rather than claiming strict superiority over other proof-of-stake protocols.The comparison section emphasizes tradeoffs based on different design goals and network assumptions.

A Technicalities of Views

The paper uses validator views rather than full views to represent coherent, dependency-satisfied information states. This simplifies visualization and protocol reasoning when messages may arrive before their dependencies.

  • A Technicalities of Views: A validator’s full view contains all messages and timestamps it has seen, while the network full view collects everything broadcast across validators.
  • A Technicalities of Views: Views can be visualized as connected trees of blocks and attestations, whereas full views may require disconnected graphs.
  • A Technicalities of Views: Full-view protocols must distinguish messages a validator has seen from messages it has accepted and fully understands.This distinction can require recursively checking whether message dependencies exist.
  • A Technicalities of Views: If a message arrives before a dependency, a view-based protocol can ignore that message until its prerequisites arrive.This makes working with views equivalent to postponing choices involving incomplete dependencies.
  • A Technicalities of Views: Views form coherent states in which validators can reason about messages without the dependency caveats associated with full views.

B The Equivocation Game

The equivocation game abstracts one Gasper slot into a timed voting model with honest and Byzantine validators, message delays, and timing noise. Its simulations use a conservative one-third Byzantine fraction.

  • B The Equivocation Game: The equivocation game models one Gasper slot as a one-shot game in which validators vote on two options.It is parametrized by V, a, ϵ1, and ϵ2.
  • B The Equivocation Game: The game uses a single real-time interval [0, 1], corresponding to one Gasper slot.
  • B The Equivocation Game: Honest validators vote at t = 0.5 for the option with more stake in their view, breaking ties in favor of O1.This abstracts Gasper’s attestation timing and fixed tiebreaking rule.
  • B The Equivocation Game: Timing error and message delay are modeled with independent uniform noise variables bounded by ϵ1 and ϵ2, alongside average delay a.A vote attempted at t is received at approximately t + a + X + Y.
  • B The Equivocation Game: The model assumes unit stake per validator and at least 2N/3 honest validators, while simulations use V = 111, Nh = 74, and Nb = 37.The simulation chooses the maximally pessimistic p = 1/3 Byzantine fraction.

B.1 The Pessimistic Regime - High Latency

The pessimistic high-latency regime tests whether coordinated dishonest voting can split honest validators’ views and prevent a decisive honest majority. The attack becomes stronger when dishonest voting approaches honest voting time, but simultaneous voting favors honest validators because delayed dishonest votes do not confuse them.

  • B.1 The Pessimistic Regime - High Latency: The pessimistic regime is a mental experiment showing that collusion can favor dishonest validators under conditions fair to both sides.
  • B.1 The Pessimistic Regime - High Latency: When message delay a is large relative to timing error ϵ1, dishonest validators can split their votes between two options near the honest voting time.The attack uses fake timestamps near 0.5 while distributing pN/2 votes to each option.
  • B.1 The Pessimistic Regime - High Latency: At t = 0.5, honest validators usually see few honest votes, so their votes split probabilistically while dishonest votes are already divided.
  • B.1 The Pessimistic Regime - High Latency: For large N, one option is very unlikely to approach 2N/3 stake under the split-vote attack.The honest votes are modeled as Bernoulli trials concentrated around a tie.
  • B.1 The Pessimistic Regime - High Latency: a = 0.15, ϵ1 = 0.05, and ϵ2 = 0.15: the simulations make message receipt uniform over [t, t + 0.3].Smaller ϵ2 would make the regime more pessimistic by further limiting visibility among honest validators.
  • B.1 The Pessimistic Regime - High Latency: 42%: dishonest validators win in Case 3 as their voting time approaches the honest validators’ voting time.Case 1 gives honest validators earlier visibility of dishonest attestations, while Case 4 nearly always favors honest validators because delay prevents confusion.

B.2 The Optimistic Regime - Low Latency

Under perfect synchrony, all decisions propagate immediately, allowing honest validators to maintain a decisive voting advantage despite dishonest strategies. With p = 1/3, the resulting vote differential is N/3, and the simulation shows honest validators always win.

  • Perfect synchrony means all decisions are immediately propagated to every validator.
  • When one choice leads, all honest validators learn the lead and vote for that choice.
  • With p = 1/3, honest validators retain a vote differential of N/3 despite dishonest voting strategies.
  • Figure 12 shows that honest validators always win when dishonest and honest validators vote in the same time frame.

B.3 An Example Inbetween

The in-between regime uses specific, deliberately arbitrary parameters to illustrate outcomes between pessimistic and optimistic extremes. Across three cases, dishonest voting can affect results, but honest validators almost always win in the simultaneous-voting case.

  • The parameter choices are acknowledged as fairly arbitrary rather than principled ground-truth values.
  • The in-between example uses a = 0.1, ϵ1 = 0.05, and ϵ2 = 0.1 to avoid both extreme regimes.
  • Case 1: In Case 1, early dishonest voting has some impact but does not distract from honest validators’ protocol-following votes.
  • Case 2: In Case 2, dishonest validators voting closer to honest validators increases the effectiveness of the attack.
  • Case 3: In Case 3, dishonest and honest validators vote simultaneously, yet honest validators still almost always win.
Loading 2003.03052v3…