A Formal Verification Method for Smart Contract

Abstract

Smart contract is a computer protocol running on the blockchain, which is widely used in various fields. However, its security problems continue to emerge. Therefore, it is necessary to audit the security of smart contract before it is deployed on the blockchain. Traditional testing methods cannot guarantee a high reliability and correctness required by the smart contract. This paper shows a method for using modeling, simulation and verification language (MSVL) and propositional projection temporal logic (PPTL) to model and verify the smart contract. First, a converter tool SOL2M which can convert Solidity program to MSVL program is developed. Then, the security properties of the smart contract are described by PPTL and a standardized process to verify the contract is designed through UMC4M (Unified Model Checker for MSVL). Finally, an example is given to illustrate the feasibility and practicability of this method in smart contract verification.