基于形式化方法的智能合约验证研究综述

智能合约是区块链技术应用的一个重要场景，智能合约技术实现了区块链的可编程化，提高了其扩展性，有广阔的应用前景。然而，一系列关于智能合约的安全事件造成了大量经济损失，削弱了人们的信心，安全性问题已经成为制约智能合约进一步发展的关键问题。如果合约设计和代码实现的过程中存在缺陷，可能会造成严重后果。而智能合约发布后无法修改，因此，在智能合约发布前对其正确性做出验证尤为重要。近年来，国内外学者在智能合约的验证领域取得了大量成果，但对这些研究成果的系统分析和总结相对较少。对以太坊的交易过程、gas 机制、存储结构、编写语言做了简要介绍，在此基础上调查归纳了智能合约中常见的8种漏洞类型，解释了漏洞产生的原因，回顾了一些真实发生的安全事件并给出了漏洞示例代码；根据不同的技术手段，如符号执行、模型检测、定理证明等，对智能合约的形式化验证工作做分类介绍，分析了各种方法的优劣，并选取了3个开源的自动化验证工具Mythril、Slither和Oyente，从运行效率、检测漏洞类型以及准确率等方面作出实验评估和对比；研究了目前已有的相关综述文章，总结了这些研究的区别与优势；概述了智能合约的漏洞检测技术中仍存在的关键问题，对智能合约验证工作的现状进行了分析和展望，提出了未来能够进一步研究的方向。

State-of-the-art survey of smart contract verification based on formal methods

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.