Ethereum Proof-of-Stake under Scrutiny

TL;DR

This paper critically examines Ethereum's Proof-of-Stake consensus post-Merge, revealing potential vulnerabilities, formalizing its properties, and demonstrating that it offers safety but only probabilistic liveness, influenced by validator parameters.

Contribution

The paper introduces a new formalization of Ethereum's liveness and availability, analyzes attacks, and identifies that the protocol has safety with probabilistic liveness.

Findings

Ethereum PoS has safety but only probabilistic liveness.

A new attack was discovered on the patched protocol.

Formalization aids in analyzing blockchain liveness and safety.

Abstract

Ethereum has undergone a recent change called \textit{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 protocol 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. We categorize different attacks jeopardizing the liveness of the protocol. The Ethereum community has responded by creating patches against some of them. 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. We believe this formalization to be helpful for other analyses as well. Our results yield that the Ethereum Proof-of-Stake has safety but only probabilistic liveness. The probability of the liveness is influenced by the parameter describing the time frame allowed for validators to change their mind about the current main chain.