Smart contract vulnerabilities pose significant security risks to the Ethereum ecosystem, driving the development of automated tools for detection and mitigation. Smart contracts are written in Solidity, a rapidly evolving programming language that continues to add features and improvements to enhance smart contract security. New versions of Solidity change the compilation process, potentially affecting how tools interpret and analyze smart contract code. We use Solidity as a case study to investigate a broader problem in software analysis: whether tool effectiveness remains stable as the underlying programming language and execution environment evolve. In this continuously evolving landscape, we investigated the compatibility of detection tools with different Solidity versions. More specifically, we analyzed detection tools by empirically assessing (i) their crash resilience, (ii) their detection effectiveness, and (iii) their execution time across different versions of Solidity. We collected 2,500 real-world smart contracts to construct a balanced wild dataset and created a separate injected-vulnerability dataset comprising 270 contracts. We extended SmartBugs, a framework that enables the execution of vulnerability detection tools for Solidity, adding 11 new tools. Results indicate that most tools are crash-resilient to version 0.4. However, 20% of the evaluated tools have been updated to remain compatible. Tool performance varies across Solidity versions and is affected by Solidity changes; execution time is higher in version 0.4.x, which was used for evaluation. We present a list of Solidity changes that affect tool performance and offer actionable takeaways for both researchers and practitioners.
Marco Campion, Isabella Mastroeni, Michele Pasqua, Caterina Urban
We introduce Abstract Lipschitz Continuity (ALC), an extensional property of functions, in particular of program semantics, requiring that bounded differences between properties of two inputs yield proportionally bounded differences between properties of the corresponding outputs. ALC explicitly discerns between two complementary forms of approximation: property-based (or qualitative) approximations, which retain a property of the data and are formalized by upper closure operators as in abstract interpretation, and quantitative approximations, which measure the closeness of data and are formalized by pre-metrics, a weakening of metrics that covers the distances arising in program analysis. Keeping the two forms of approximation explicit has two main benefits. First, it allows us to precisely relate ALC to established extensional properties: ALC is a sufficient condition for partial completeness in abstract interpretation, for partial abstract non-interference in language-based security and, with a null Lipschitz constant, for abstract robustness in machine learning. Second, it supports reasoning about ALC of program semantics by induction on the syntax of programs: we present a sound deductive system, parametric in the property-based approximations and in the pre-metric of interest, that reduces a proof of ALC for a program to proofs for its basic commands and to some explicit side conditions, which isolate what makes ALC compositional across sequential composition, non-deterministic choice and iteration.