The Good, the Bad and the Ugly: Pitfalls and Best Practices in Automated Sound Static Analysis of Ethereum Smart Contracts
This work addresses the need for reliable security analysis in Ethereum smart contracts to prevent monetary losses, but it is incremental as it builds on and critiques existing methods.
The paper reviews existing automated sound static analysis tools for Ethereum smart contracts, identifying common pitfalls, and presents eThor, a new tool designed with rigorous semantic foundations to address these issues, though no specific performance numbers are provided.
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.