Combating Reentrancy Bugs on Sharded Blockchains

TL;DR

This paper investigates reentrancy bugs in sharded blockchains like ICP, NEAR, and MultiversX, highlighting their prevalence, analyzing existing prevention techniques, and proposing new patterns and formal verification methods to mitigate these vulnerabilities.

Contribution

It provides the first detailed analysis of reentrancy in sharded blockchains, evaluates Ethereum techniques in this context, and introduces novel programming patterns and formal verification approaches.

Findings

66% of reviewed ICP contracts had reentrancy bugs

Ethereum prevention techniques face issues in sharded models

Proposed Rust and Motoko patterns effectively mitigate bugs

Abstract

Reentrancy is a well-known source of smart contract bugs on Ethereum, leading e.g. to double-spending vulnerabilities in DeFi applications. But less is known about this problem in other blockchains, which can have significantly different execution models. Sharded blockchains in particular generally use an asynchronous messaging model that differs substantially from the synchronous and transactional model of Ethereum. We study the features of this model and its effect on reentrancy bugs on three examples: the Internet Computer (ICP) blockchain, NEAR Protocol, and MultiversX. We argue that this model, while useful for improving performance, also makes it easier to introduce reentrancy bugs. For example, reviews of the pre-production versions of some of the most critical ICP smart contracts found that 66% (10/15) of the reviewed contracts -- written by expert authors -- contained reentrancy bugs of medium or high severity, with potential damages in tens of millions of dollars. We evaluate existing Ethereum programming techniques (in particular the effects-checks-interactions pattern, and locking) to prevent reentrancy bugs in the context of this new messaging model and identify some issues with them. We then present novel Rust and Motoko patterns that can be leveraged on ICP to solve these issues. Finally, we demonstrate that the formal verification tool TLA+ can be used to find and eliminate such bugs in real world smart contracts on sharded blockchains.