Semantics-Based Static Vulnerability Detection in Solidity Using Abstract Interpretation
摘要
This paper introduces a novel semantics-based static analysis approach for Solidity, leveraging the Abstract Interpretation theory to enhance Ethereum smart contract vulnerability detection. Our approach formalizes a sound approximation of Solidity semantics, balancing precision and computational efficiency through tunable abstraction levels. By integrating local and blockchain state considerations into an augmented flow graph capturing both data and control flow, we achieve effective vulnerability detection. Implemented using the APRON library’s Interval and Octagon abstract domains, our approach demonstrates significant improvements over state-of-the-art tools in the case of Reentrancy and Arithmetic vulnerabilities.