State-based Invariant Property Generation of Solidity Smart Contracts using Abstract Interpretation

Solidity sets its place as one of the most popular and widely-used smart contract language for Ethereum in recent years. To automate the verification of Solidity codes, especially in case of critical systems, this is intrinsic to synthesize their invariant properties which hold in every valid executions. This paper defines a formal semantics of Solidity subset and introduces an Abstract Interpretation-based sound semantics approximation to infer state-based invariant properties of Solidity contracts. The intuition behind our proposal is to apply abstraction to all possible states reachable on the executions of the contract's functions in any order under all possible instantiation context, which reflects the decentralized mining strategies in the blockchain networks. The invariant computation is expressed as a fixpoint solution of state-based functions in an abstract domain of interest, based on the generic static analysis framework.