2024/01/01 by Ye Liu, Liu, Ye, Chengxuan Zhang +2 · 5 citations
Computer Science · #Advanced Malware Detection Techniques #FOS: Computer and information sciences #Security and Verification in Computing #Software Engineering (cs.SE) #Software Engineering Research
paper · pdf · doi:10.48550/arxiv.2401.00650
openalex publication_date 2024/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.