智能合约的形式化验证方法研究综述
Review on Formal Verification of Smart Contract
查看参考文献69篇
|
文摘
|
形式化方法是在安全关键软件系统中被广泛采用而有效的基于数学的验证方法,而智能合约属于安全关键代码,采用形式化方法验证智能合约已经成为热点研究领域.本文对自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. |
|
来源
|
电子学报
,2021,49(4):792-804 【核心库】
|
|
DOI
|
10.12263/dzxb.20200723
|
|
关键词
|
形式化验证
;
智能合约
;
区块链
;
隐私保护
;
信息安全
;
可信交易
|
|
地址
|
北京航空航天大学, 软件开发环境国家重点实验室, 北京, 100191
|
|
语种
|
中文 |
|
文献类型
|
综述型 |
|
ISSN
|
0372-2112 |
|
学科
|
自动化技术、计算机技术 |
|
基金
|
国家重点研发项目
;
国家自然科学基金
;
教育部中国移动基金
;
软件开发重点实验室基金
|
|
文献收藏号
|
CSCD:6956646
|
参考文献 共
69
共4页
|
|
1.
Nikolic I.
Finding the Greedy,Prodigal,and Suicidal Contracts at Scale,2018/2020
|
CSCD被引
1
次
|
|
|
|
|
2.
Amritarj Singh. Blockchain smart contracts formalization: approaches and challenges to address vulnerabilities.
Computers & Security,2020(88):1-10
|
CSCD被引
1
次
|
|
|
|
|
3.
Liu J. A survey on security verification of blockchain smart contracts.
IEEE Access,2019(7):77894-77904
|
CSCD被引
12
次
|
|
|
|
|
4.
王璞巍. 面向合同的智能合约的形式化定义及参考实现.
软件学报,2019,30(9):2608-2619
|
CSCD被引
11
次
|
|
|
|
|
5.
Leroy X. A formally verified compiler back-end.
Journal of Automated Reasoning,2009,43(4):363-446
|
CSCD被引
6
次
|
|
|
|
|
6.
Bhargavan K. Formal verification of smart contracts: short paper.
The 2016 ACM Workshop on Programming Languages and Analysis for Security,2016:91-96
|
CSCD被引
3
次
|
|
|
|
|
7.
Fan Zhang. Town Crier: an authenticated data feed for smart contracts.
The 2016 ACM SIGSAC Conference on Computer and Communications Security,2016:270-282
|
CSCD被引
1
次
|
|
|
|
|
8.
Nielsen B J.
Smart Contract Interactions in Coq,2019/2020
|
CSCD被引
1
次
|
|
|
|
|
9.
Zhu J.
Formal Verification of Solidity Vontracts in Event-B,2020
|
CSCD被引
1
次
|
|
|
|
|
10.
胡凯. 智能合约的形式化验证方法.
信息安全研究,2016,2(12):1080-1089
|
CSCD被引
22
次
|
|
|
|
|
11.
Grishchenko I. A semantic framework for the security analysis of ethereum smart contracts.
International Conference on Principles of Security and Trust,2018:243-269
|
CSCD被引
7
次
|
|
|
|
|
12.
Sun T. A formal verification framework for security issues of blockchain smart contracts.
Electronics,2020,9(2):254-255
|
CSCD被引
3
次
|
|
|
|
|
13.
Hirai Y. Defining the ethereum virtual machine for interactive theorem provers.
International Conference on Financial Cryptography and Data Security,2017:520-535
|
CSCD被引
1
次
|
|
|
|
|
14.
Mulligan D P. Lem: Reusable engineering of real-world semantics.
ACM SIGPLAN Notices,2014,49(9):175-188
|
CSCD被引
2
次
|
|
|
|
|
15.
Hildenbrandt E. KEVM: A complete formal semantics of the ethereum virtual machine.
2018 IEEE 31st Computer Security Foundations Symposium,2018:204-217
|
CSCD被引
2
次
|
|
|
|
|
16.
Sidney A. Towards verifying ethereum smart contract bytecode in Isabelle/HOL.
The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs,2018:66-77
|
CSCD被引
1
次
|
|
|
|
|
17.
Daejun P. A formal verification tool for ethereum VM bytecode.
The 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering,2018:912-915
|
CSCD被引
1
次
|
|
|
|
|
18.
Idelberger F. Evaluation of logic-based smart contracts for blockchain systems.
International Symposium on Rules and Rule Markup Languages for the Semantic Web,2016:167-183
|
CSCD被引
4
次
|
|
|
|
|
19.
Sergey I. A concurrent perspective on smart contracts.
International Conference on Financial Cryptography and Data Security,2017:478-493
|
CSCD被引
1
次
|
|
|
|
|
20.
Sanchez D C.
Raziel: Private and Verifiable Smart Contracts on Blockchains,2018/2020
|
CSCD被引
1
次
|
|
|
|
|
了解气象卫星更多信息，请访问