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

Review on Formal Verification of Smart Contract

作　　者：朱健 胡凯 张伯钧 ZHU Jian;HU Kai;ZHANG Bo-jun(State Key Laboratory of Software Development Environment,Beijing University of Aeronautics and Astronautics,Beijing 100191,China)

机构地区：[1]北京航空航天大学软件开发环境国家重点实验室,北京100191

出　　处：《电子学报》2021年第4期792-804,共13页Acta Electronica Sinica

基　　金：国家重点研发项目(No.2018YFB1402702);国家自然科学基金(No.61672074,No.61672075);教育部中国移动基金(No.MCM20180104);软件开发重点实验室基金(No.SKLSDE-2020ZX-21)。

摘　　要：形式化方法是在安全关键软件系统中被广泛采用而有效的基于数学的验证方法,而智能合约属于安全关键代码,采用形式化方法验证智能合约已经成为热点研究领域.本文对自2015年以来的47篇典型相关论文进行了研究分析,对技术进行了详细的分类研究和对比分析;对形式化验证智能合约的过程中使用的形式化方法、语言、工具和框架进行综述.研究表明,其中定理证明技术和符号执行技术适用范围最广,可验证性质最多,很多底层框架均有所涉及,而运行时验证技术属于轻量级的新验证技术,仍处于探索阶段.由此我们列出了一些关键问题如智能合约的自动化验证问题,转换一致性问题,形式化工具的信任问题和形式化验证的评判标准问题.本文还展望了未来形式化方法与智能合约结合的研究方向,对领域研究有一定的推动作用.Formal methods are widely used in safety-critical software systems and have effective mathematical-based verification methods,while smart contracts belong to safety-critical codes.Using formal methods to verify smart contracts has become a popular research topic.This paper has conducted researches and analysis on 47 typical related papers since 2015 and carried out detailed classification research and comparative analysis on technology,as well as the formal methods,languages,tools and frameworks used in the formal verification of smart contracts overview.Research shows that theorem proving technique and symbolic execution technique have the widest scope of application,can verify the most properties and are involved in many basic frameworks.And the runtime verification is a new lightweight verification technology,still in the exploratory stage.From this,we have listed some key issues such as automatic verification of smart contracts,conversion consistency,trust in formal tools,and evaluation criteria for formal verification.This paper also looks forward for the future research direction on the combination of formal methods and smart contracts.For attracting more valuable ideas and promote the research in the field.

关 键 词：形式化验证 智能合约 区块链 隐私保护 信息安全 可信交易 

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