Review on Formal Verification of Smart Contract

ZHU Jian; HU Kai; ZHANG Bo-jun

doi:10.12263/DZXB.20200723

您当前的位置：

首页 >

文章列表页 >

Review on Formal Verification of Smart Contract

更新时间：2025-12-08

- Review on Formal Verification of Smart Contract
- Acta Electronica Sinica Vol. 49, Issue 4, Pages: 792-804(2021)
- 作者机构：
  
  北京航空航天大学软件开发环境国家重点实验室,北京,100191
- 作者简介：
- 基金信息：
  
  National Key Research and Development Program (No.2018YFB1402702);National Natural Science Foundation of China (No.61672074, No.61672075);Joint Fund of Ministry of Education of China and China Mobile (No.MCM20180104);Foundation of Key Laboratory of Software Development (No.SKLSDE-2020ZX-21)
- DOI：10.12263/DZXB.20200723
  CLC： TP301
- Published：2021
- 稿件说明：
移动端阅览
ZHU Jian, HU Kai, ZHANG Bo-jun. Review on Formal Verification of Smart Contract[J]. Acta Electronica Sinica, 2021, 49(4): 792-804.
DOI：

ZHU Jian, HU Kai, ZHANG Bo-jun. Review on Formal Verification of Smart Contract[J]. Acta Electronica Sinica, 2021, 49(4): 792-804. DOI： 10.12263/DZXB.20200723.

摘要

形式化方法是在安全关键软件系统中被广泛采用而有效的基于数学的验证方法，而智能合约属于安全关键代码，采用形式化方法验证智能合约已经成为热点研究领域.本文对自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.

关键词

Keywords

references

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Blockchain-Based Hierarchical Federated Learning System

TokenVis: Visual Analytics for Evolutionary Patterns of Ethereum ERC-20 Smart Contract

The Inherent Mechanism, Model and Key Technique Prospects of JointCloud Computing Distributed Ledger

Blockchain Data Controlled Sharing Scheme Based on Proxy Re-Encryption

Blockchain Trusted Privacy Service Computing Model for CNN

Related Author

HU Rong-lei

LIU Si-hui

DUAN Xiao-yi

ZUO Pei-liang

ZHANG Yan-shuo

LI Guo-zheng

ZHAO Cong

LIU Chi

Related Institution

Department of Electronics and Information Engineering, Beijing Electronic Science and Technology Institute

School of Computer Science and Technology， Beijing Institute of Technology

School of Data Science， Fudan University

National Key Laboratory of Parallel and Distributed Processing， College of Computer Science， National University of Defense Technology

Key Laboratory of Software Engineering for Complex Systems， College of Computer Science， National University of Defense Technology

⁰