Automated Invariant Generation for Solidity Smart Contracts
Ye Liu, Chengxuan Zhang, Yi Li.
TL;DR
This work tackles the lack of formal specifications for Solidity smart contracts by introducing INVCON+, a framework that combines dynamic invariant detection with static verification to generate verified contract invariants. It advances on prior InvCon by enabling richer invariants, including implications, through an iterative Houdini-like process and a Solidity-specific invariant language. The approach is implemented in InvCon+ and evaluated on 361 ERC20 and 10 ERC721 contracts as well as vulnerability benchmarks, demonstrating high recall and fully verified invariants with practical runtime performance. The results show that mined invariants can effectively articulate contract semantics, improve security against common vulnerabilities, and can be crowdsourced across contracts to enhance coverage. The work provides a reproducible dataset, a public prototype, and concrete guidance for applying invariant-driven verification in real-world smart contract development and auditing.
Abstract
Smart contracts are computer programs running on blockchains to automate the transaction execution between users. The absence of contract specifications poses a real challenge to the correctness verification of smart contracts. Program invariants are properties that are always preserved throughout the execution, which characterize an important aspect of the program behaviors. In this paper, we propose a novel invariant generation framework, INVCON+, for Solidity smart contracts. INVCON+ extends the existing invariant detector, InvCon, to automatically produce verified contract invariants based on both dynamic inference and static verification. Unlike INVCON+, InvCon only produces likely invariants, which have a high probability to hold, yet are still not verified against the contract code. Particularly, INVCON+ is able to infer more expressive invariants that capture richer semantic relations of contract code. We evaluate INVCON+ on 361 ERC20 and 10 ERC721 real-world contracts, as well as common ERC20 vulnerability benchmarks. The experimental results indicate that INVCON+ efficiently produces high-quality invariant specifications, which can be used to secure smart contracts from common vulnerabilities.