A Sound Semantics Approximation of Solidity for Enhanced Vulnerability Detection

As Solidity smart contracts become central to decentralized finance and governance, the exploitation of critical vulnerabilities has repeatedly resulted in severe financial losses. Existing state-of-the-art methods that rely on symbolic execution or syntactic patterns are unable to model the language semantics accurately. This limits their ability to reason about all possible runtime behaviors and, hence, often produces numerous false alarms under adversarial blockchain environment. To address these challenges, in this paper, we propose a semantics-driven static analysis framework for detecting vulnerabilities in Solidity. Our proposed framework is grounded in Abstract Interpretation theory, enabling safe approximation of program semantics to formally capture dynamic behavioral properties of Solidity smart contracts at different levels of abstraction. While it performs fixpoint semantics computations on an augmented control flow graph guided by adversarial contexts, it applies semantic dependences refinement through numerical abstractions as well. This facilitates more precise reasoning regarding semantic properties indicating the presence of possible Solidity vulnerabilities. Our prototype, developed using the APRON library, supports various numerical abstract domains, such as Intervals, Octagons, and Polyhedra, thereby optimizing the trade-off between precision and computational cost. Empirical results on four benchmark datasets (SBC, Qian, RSD, and SolidiFI) show that the Interval domain works well for integer overflow and underflow and for reentrancy, while the Polyhedra domain captures the linear relations among variables needed for timestamp and transaction-ordering dependencies. Furthermore, the semantics-aware analysis enables our tool to achieve the highest F1-score in seven of the nine evaluated dataset-vulnerability combinations, with average F1-score improvements over the strongest existing baselines of about 5.3, 15.0, 13.6, and 5.5 percentage points for Reentrancy, Integer Overflow and Underflow, Timestamp Dependency, and Transaction Ordering Dependency, respectively, together with AUC improvements of up to 0.41.