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.

翻译：智能合约是运行在区块链上的计算机程序，用于自动化用户之间的交易执行。合约规范的缺失对智能合约的正确性验证构成了实际挑战。程序不变量是在整个执行过程中始终得到保持的性质，它刻画了程序行为的重要方面。本文提出了一种新颖的不变量生成框架INVCON+，专为Solidity智能合约设计。INVCON+扩展了现有不变量检测器InvCon，能够基于动态推断与静态验证自动生成经检验的合约不变量。与INVCON+不同，InvCon仅生成似然不变量（即具有高概率成立但仍未针对合约代码进行验证的断言）。特别地，INVCON+能够推断出更具表达力的不变量，从而捕获合约代码中更丰富的语义关系。我们在361个ERC20合约、10个ERC721真实世界合约以及常见ERC20漏洞基准上对INVCON+进行了评估。实验结果表明，INVCON+能够高效生成高质量的不变量规范，这些规范可用于保护智能合约免受常见漏洞的侵害。