Research Summary: Ethereum Proof-of-Stake under Scrutiny

Research Summary: Ethereum Proof-of-Stake under Scrutiny

TL;DR

  • Ethereum has undergone a recent change called the Merge, which made Ethereum a Proof-of-Stake blockchain shifting closer to BFT consensus.
  • The result is a blockchain being possibly produced in a tree-like form while participants try to finalize blocks.
  • Several attacks jeopardizing liveness have been found in this new setting. The Ethereum community has responded by creating a patch. We discovered a new attack on the patched protocol.
  • To support our analysis, we propose a new high-level formalization of the properties of liveness and availability of the Ethereum blockchain, and we provide a pseudo-code.
  • Our results yield that the Ethereum Proof-of-Stake has probabilistic liveness.

Core Research Question

We focused on the new Ethereum Proof-of-Stake consensus. We aim to produce a high-level formalization and study the protocol’s properties.

Citation

Ulysse Pavloff, Yackolley Amoussou-Guenou, and Sara Tucci-Piergiovanni. Ethereum Proof-of-Stake under Scrutiny, 2022 preprint arxiv. Accepted for publication in ACM SAC 2023.

Background

  • Finality: A block finalized cannot be revoked.
  • Safety: A chain is safe if there cannot exist forks. The finalized chain - the chain containing the finalized blocks - is safe if any two processes see different finalized chains means that one is a prefix of the other.
  • Liveness: A blockchain is live if new finalized blocks eventually get added to the chain.
  • Consensus protocol:
    • BFT: Byzantine Fault Tolerent protocols are protocols that guarantee safety as long as the proportion of malicious participants is less than 1/3.
    • Nakamoto-style: A consensus that might allow forks but provides a fork chain rule to chose a unique chain.
  • Fork choice rule: A rule inherent in the protocol for choosing the unique chain in the event of a fork, e.g. longest chain rule in Bitcoin.
  • Candidate chain: We call candidate chain the chain designated as the one to build upon by the fork choice rule.
  • Finality gadget: A rule designed to finalize blocks.
  • Proof of Stake: Proof-of-Stake (PoS) protocols are those in which participants leverage their money to obtain rights in the consensus process.
  • Bouncing attack: A bouncing attack is a type of liveness attack. It prevents finalization by constantly manipulating honest validators into changing their view on which chain is the candidate one.
  • Slot & Epoch: In the protocol, time is measured by periods of 12 seconds called slot, a period of 32 slots is called an epoch.

Summary

  • Ethereum has undergone a recent change called the Merge, which made Ethereum a Proof-of-Stake blockchain shifting closer to BFT consensus. Ethereum, which wished to keep the best of the two protocols designs (BFT and Nakomoto-style), now has a convoluted consensus protocol as its core. The result is a blockchain being possibly produced in a tree-like form while participants try to finalize blocks.
  • Several attacks jeopardizing liveness have been found in this new setting. The Ethereum community has responded by creating a patch. We discovered a new attack on the patched protocol.
  • To support our analysis, we propose a new formalization of the properties of liveness and availability of the Ethereum blockchain, and we provide a pseudo-code. We believe this formalization to be helpful for other analyses as well.
  • Our results yield that the Ethereum Proof-of-Stake has probabilistic liveness, influenced by the parameter describing the time frame allowed for validators to change their mind about the current candidate chain.

Method

  • We provide a system model which abstracts assumptions about the network, the participants’ behavior both honest and malicious, and clock synchronization assumptions.
  • We specify the expected properties of Ethereum in terms of safety and liveness.
  • We formalize the main functions of the protocol through pseudo-codes for a better understanding and analysis purposes. The functiuns are drawn from the specifications and various implementations (such as Prysm and Teku).

Results

Properties formalization & protocol overview

The protocol is constituted of two main elements: the fork choice rule and the finality gadget. The fork choice rule is called GHOST, and the finality gadget is called CASPER FFG. The combination gives its name to the protocol GASPER introduced as the new Ethereum protocol.

To study the combination of the mechanisms, we give several properties and definitions. We streamlined them in the background section.

The finality gadget, which aims at finalizing blocks, proceeds in two steps: first, justification, then finalization. Justification is done at the epoch level and consist of (a) aggregating the validators’ vote and (b) justfying the blocks of the current epoch if 2/3 of them agree on the view of the chain. By repeating the justification in succeding epochs, finalization can occur.

The fork choice rule uses justified blocks as a starting point to determine the candidate chain.
Using the intertwining of the two mechanisms, malicious validators can hinder the finalization process only repeating justification.

Probabilistic bouncing attack

The patch that is in place to stop the original bouncing attack prevents validators from changing their view of the chain after a certain amount of time has passed in the epoch: j slots.
Nonetheless, Byzantine validators can still use this to separate the views of validators and thus create a fork. They do so by sending a message that is received before the j^{\rm{th}} slot for a portion of validators and after for the rest of them. By cleverly choosing the proportion of validators on each chain of the fork, this attack can be repeated for an indefinite period.
Two conditions are necessary to perform this attack: a favorable setup[1], and a Byzantine proposer in one of the first j slots.

The probability of the attack being successful for k epochs is:

P(\textrm{bouncing }k \textrm{ times})=(1-\alpha^j)^k,

with \alpha \in [0,1] the proportion of honest validators and j the number of slots before locking a choice for the justification.

The probability of the bouncing attack stems from the probability of a proposer being Byzantine in the first j slot of the epoch, which is 1 minus the probability of having only honest proposers. We repeat this k times for the probability of this attack lasting k epochs.

This attack is inspired from the splitting attack presented alongside the patch. In the explanation of the patch that proposes to prevent the bouncing attack by stopping validators from changing their view of the chain, they mention how a Byzantine validator could take advantage of this rule if it can manipulate the network delay. We show that our attack exists even with weaker Byzantine validators that do not manipulate the network delay but only commit equivocation during the synchronous period.

Discussion and Key Takeaways

  • Our contribution provides a high-level formalization of Ethereum PoS.
  • We outlined an attack against the liveness of the protocol, showing the probabilistic liveness of the protocol under this attack.
  • Our analysis did not consider the protocol’s rewards and incentives. We leave this part, as well as analyzing rational behavior in the protocol, as future work.

Applicability

  • This work can be used for future analysis and comparison with future versions of the protocol.
  • This is the first step in providing a formalization for verification tools.

  1. A favorable setup leading to a probabilistic bouncing attack can occur after the asynchronous period if the network suffured a partition. It is similar to a scenario leading to a bouncing attack. ↩︎

5 Likes