An Automated Analyzer for Financial Security of Ethereum Smart Contracts

TL;DR

FASVERIF introduces a fully automated framework to assess the financial security of Ethereum smart contracts by automatically generating finance-focused security properties and corresponding models, then verifying them with a modified MSR-based pipeline that combines the $Tamarin$ prover and $Z3$. The approach leverages a statistical analysis of tens of thousands of real contracts to define invariant and equivalence properties that capture token and ether-related vulnerabilities, including transferMint and TD/TOD scenarios. The authors prove the soundness of translating Solidity into their KSolidity/MSR model and demonstrate superior accuracy and vulnerability coverage on large vulnerability and real-world datasets, identifying exploitable bugs missed by prior tools. While effective, the method has limitations in speed, Solidity feature support, and scope, which the authors acknowledge and propose for future extension. Overall, FASVERIF offers a principled, automated path toward scalable financial-security verification for DeFi contracts with practical impact for developers and security analysts.

Abstract

At present, millions of Ethereum smart contracts are created per year and attract financially motivated attackers. However, existing analyzers do not meet the need to precisely analyze the financial security of large numbers of contracts. In this paper, we propose and implement FASVERIF, an automated analyzer for fine-grained analysis of smart contracts' financial security. On the one hand, FASVERIF automatically generates models to be verified against security properties of smart contracts. On the other hand, our analyzer automatically generates the security properties, which is different from existing formal verifiers for smart contracts. As a result, FASVERIF can automatically process source code of smart contracts, and uses formal methods whenever possible to simultaneously maximize its accuracy. We evaluate FASVERIF on a vulnerabilities dataset by comparing it with other automatic tools. Our evaluation shows that FASVERIF greatly outperforms the representative tools using different technologies, with respect to accuracy and coverage of types of vulnerabilities.

Figures (19)

• Figure 1: Core subset of Solidity
• Figure 2: Example contract Ex1.
• Figure 3: Design of FASVERIF.
• Figure 4: Parts of the translation of functions and statements.
• Figure 5: Example contract Ex2.

Theorems & Definitions (49)

• Theorem 6.1
• Definition A.1
• Definition A.2
• Definition A.3
• Lemma A.4
• Definition A.5
• Definition A.6
• Definition A.7
• Definition A.8
• Lemma A.9