When is Spring coming? A Security Analysis of Avalanche Consensus

TL;DR

This paper provides a formal specification and analysis of the Avalanche blockchain consensus protocol, revealing a vulnerability affecting its liveness and proposing a potential fix.

Contribution

It offers the first detailed pseudocode formulation of Avalanche and analyzes its formal properties, identifying a liveness vulnerability and suggesting a solution.

Findings

Formal pseudocode of Avalanche protocol

Analysis of Avalanche's formal properties

Identification of a liveness vulnerability

Abstract

Avalanche is a blockchain consensus protocol with exceptionally low latency and high throughput. This has swiftly established the corresponding token as a top-tier cryptocurrency. Avalanche achieves such remarkable metrics by substituting proof of work with a random sampling mechanism. The protocol also differs from Bitcoin, Ethereum, and many others by forming a directed acyclic graph (DAG) instead of a chain. It does not totally order all transactions, establishes a partial order among them, and accepts transactions in the DAG that satisfy specific properties. Such parallelism is widely regarded as a technique that increases the efficiency of consensus. Despite its success, Avalanche consensus lacks a complete abstract specification and a matching formal analysis. To address this drawback, this work provides first a detailed formulation of Avalanche through pseudocode. This includes features that are omitted from the original whitepaper or are only vaguely explained in the documentation. Second, the paper gives an analysis of the formal properties fulfilled by Avalanche in the sense of a generic broadcast protocol that only orders related transactions. Last but not least, the analysis reveals a vulnerability that affects the liveness of the protocol. A possible solution that addresses the problem is also proposed.