The Good, the Bad and the Ugly: Pitfalls and Best Practices in Automated Sound Static Analysis of Ethereum Smart Contracts

TL;DR

This paper reviews current automated static analysis tools for Ethereum smart contracts, highlights common pitfalls, and introduces eThor, a new tool designed with rigorous semantic foundations to improve analysis accuracy and reliability.

Contribution

It provides a comprehensive review of existing tools, identifies key issues, and presents eThor, a novel static analysis tool with a principled, semantics-based design.

Findings

Many existing tools suffer from prevalent errors and limitations.

eThor demonstrates improved soundness and reliability in analyzing smart contracts.

The paper offers best practices for designing sound static analyzers.

Abstract

Ethereum smart contracts are distributed programs running on top of the Ethereum blockchain. Since program flaws can cause significant monetary losses and can hardly be fixed due to the immutable nature of the blockchain, there is a strong need of automated analysis tools which provide formal security guarantees. Designing such analyzers, however, proved to be challenging and error-prone. We review the existing approaches to automated, sound, static analysis of Ethereum smart contracts and highlight prevalent issues in the state of the art. Finally, we overview eThor, a recent static analysis tool that we developed following a principled design and implementation approach based on rigorous semantic foundations to overcome the problems of past works.