电子学报 ›› 2021, Vol. 49 ›› Issue (4): 792-804.DOI: 10.12263/DZXB.20200723

• 综述评论 • 上一篇    下一篇

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

朱健, 胡凯, 张伯钧   

  1. 北京航空航天大学软件开发环境国家重点实验室, 北京 100191
  • 收稿日期:2020-07-16 修回日期:2020-10-07 出版日期:2021-04-25
    • 通讯作者:
    • 张伯钧
    • 作者简介:
    • 朱健 男,1997年生于安徽铜陵.现为北京航空航天大学硕士研究生.主要研究方向为区块链技术和形式化验证技术.E-mail:zhujian@buaa.edu.cn;胡凯 男,1963年生于湖南长沙,现为北京航空航天大学计算机学院教授、博士,主要研究方向和关注领域:分布式计算、区块链与数字社会技术.Email:hukai@buaa.edu.cn
    • 基金资助:
    • 国家重点研发项目 (No.2018YFB1402702); 国家自然科学基金 (No.61672074,No.61672075); 教育部中国移动基金 (No.MCM20180104); 软件开发重点实验室基金 (No.SKLSDE-2020ZX-21)

Review on Formal Verification of Smart Contract

ZHU Jian, HU Kai, ZHANG Bo-jun   

  1. State Key Laboratory of Software Development Environment, Beijing University of Aeronautics and Astronautics, Beijing 100191, China
  • Received:2020-07-16 Revised:2020-10-07 Online:2021-04-25 Published:2021-04-25

摘要: 形式化方法是在安全关键软件系统中被广泛采用而有效的基于数学的验证方法,而智能合约属于安全关键代码,采用形式化方法验证智能合约已经成为热点研究领域.本文对自2015年以来的47篇典型相关论文进行了研究分析,对技术进行了详细的分类研究和对比分析;对形式化验证智能合约的过程中使用的形式化方法、语言、工具和框架进行综述.研究表明,其中定理证明技术和符号执行技术适用范围最广,可验证性质最多,很多底层框架均有所涉及,而运行时验证技术属于轻量级的新验证技术,仍处于探索阶段.由此我们列出了一些关键问题如智能合约的自动化验证问题,转换一致性问题,形式化工具的信任问题和形式化验证的评判标准问题.本文还展望了未来形式化方法与智能合约结合的研究方向,对领域研究有一定的推动作用.

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

Abstract: 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.

Key words: formal verification, smart contract, blockchain, privacy protection, information security, trusted transaction

中图分类号: