State-of-the-art survey of smart contract verification based on formal methods - Wenbo ZHANG; Simin CHEN; Lifei WEI; Wei SONG; Dongmei HUANG (网络与信息安全学报)
Smart contract represents an essential application scenario of blockchain technology.Smart contract technology improves programmability and scalability of blockchain, and has broad development prospects.However, a series of security incidents caused a great number of economic losses and weakened users’ confidence in the Ethereum platform.The security of smart contract has become a critical problem that restricts the further development of smart contract.Defects in smart contract code may cause serious consequences and cannot be modified once deployed, it is especially important to verify the correctness of smart contract in advance.In recent years, researchers have obtained many achievements in verification of smart contract, but there is a lack of systematic summary of these research results.Therefore, some basic principles of Ethereum were introduced, including the transaction, gas mechanism, storage and programming language.Eight common types of vulnerabilities in smart contract were summarized and their causes were explained.Some real security events were reviewed and some examples of vulnerability codes were presented.Then, the research work on automatic verification of smart contract based on symbolic execution, model checking and theorem proving was classified and summarized.Three open-source automated tools were selected, including Mythril, Slither and Oyente.And experiments were implemented to evaluate and compare the three tools from the aspects of efficiency, accuracy and the types of vulnerability can be detected.Furthermore, related review articles were surveyed, and the advantages of this paper compared with these works were summarized.The critical problems in the vulnerability detection technology of smart contract were also summarized and the direction of future research was proposed at last.