  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.

Software Engineering