以太坊智能合约安全形式化验证方法研究进展  

Review:Secure Formal Verification Methods for Ethereum Smart Contracts

作　　者：王赫彬 郑长友 黄松 孙金磊 丁一先[3] WANG He-bin;ZHENG Chang-you;HUANG Song;SUN Jin-lei;DING Yi-xian(School of Command and Control Engineering,Army Engineering University of PLA,Nanjing 210007,China;Military Software Training and Evaluation Center,Army Engineering University of PLA,Nanjing 210007,China;Liaoning Technical University,Fuxin 123000,China)

机构地区：[1]中国人民解放军陆军工程大学指挥控制工程学院,江苏南京210007 [2]中国人民解放军陆军工程大学全军军事训练软件测评中心,江苏南京210007 [3]辽宁工程技术大学,辽宁阜新123000

出　　处：《计算机技术与发展》2021年第9期104-111,共8页Computer Technology and Development

基　　金：国家重点研发计划重点专项项目(2018YFB1403400)。

摘　　要：以太坊智能合约是区块链技术的典型应用和实现。由于智能合约一旦部署就难以修改,智能合约在上链之前的正确性显得至关重要。虽然很多当前工作都对于智能合约漏洞的检测与预防进行了一系列研究,但是对于检查合约属性和范式的形式化验证方法还没有比较全面的总结。首先介绍了智能合约基本的表示和编译方式、常用的编程语言、出现的漏洞类型和常见的形式化验证方法,并分析了形式化验证方法在智能合约方面的研究现状;然后,通过实验结果分析验证了两种现有的有界模型检测工具的检测好坏,对于某些具体的合约攻击,漏报率达到30%以上,现有形式化验证方法漏报率高、应用范围受限以及验证语言安全性未知等一系列缺陷亟待解决;最后,针对现有形式化验证方法存在的不足之处展望了未来的研究方向。Ethereum smart contract is a typical application and implementation of blockchain technology.Since a smart contract is difficult to be modified once it is deployed,thus it is important for coders to check smart contracts’correctness before putting on the chains.Although there are many current researches of the vulnerability detection and prevention of smart contracts,no complete summary of the correctness and feasibility of concepts and properties of smart contracts,such as user interactions and specific technical concepts,are carried out.Firstly,basic representation and compilation,frequently-used programming languages,vulnerabilities of smart contracts and common formal verification methods were introduced.Secondly,the effectiveness of the two existing bounded model checking tools is checked and reproduced through the analysis of experiment results,false negative rate reaches 30%,and it is urgent to correct weaknesses of the existing formal verification methods,such as high rate of false positives,limited application scopes,unknown security of the verification language and so on.Finally,the future research directions are prospected according to the limitations of these existing researches of formal verification methods.

关 键 词：以太坊 智能合约 形式化验证 定理证明 模型检测 

分 类 号：TP309[自动化与计算机技术—计算机系统结构] TP311[自动化与计算机技术—计算机科学与技术]