On Verification of Smart Contracts via Model Checking

Combined with smart contracts, the application of blockchain techniques has grown faster and broader. However, it is very difficult to write secure and functionally correct smart contracts because of the openness of blockchain platforms. Formal verification, such as model checking, has been proven to be an effective way of guaranteeing security and correctness of systems. In this paper, we propose a novel model checking based framework, called mcVer, to support the verification of smart contracts written in Solidity. Built on model checking tool VERDS, the mcVer framework is able to verify not only safety properties but also liveness properties of smart contracts. For the properties that are not satisfied, mcVer produces a counter example by showing a sequence of statements in the original Solidity program as a hint for fault localization. We implemented the automatic transformation from a subset of the Solidity language to the modeling language of VERDS, that therefore provides automatic verification for smart contracts. Experiments are carried out on various cases, including checking contracts for finding typical security vulnerabilities and verifying properties of an access control smart contract. The experimental results demonstrate the flexibility and efficiency of mcVer.