典型文献
基于形式化方法的智能合约验证研究综述
文献摘要：
智能合约是区块链技术应用的一个重要场景,智能合约技术实现了区块链的可编程化,提高了其扩展性,有广阔的应用前景.然而,一系列关于智能合约的安全事件造成了大量经济损失,削弱了人们的信心,安全性问题已经成为制约智能合约进一步发展的关键问题.如果合约设计和代码实现的过程中存在缺陷,可能会造成严重后果.而智能合约发布后无法修改,因此,在智能合约发布前对其正确性做出验证尤为重要.近年来,国内外学者在智能合约的验证领域取得了大量成果,但对这些研究成果的系统分析和总结相对较少.对以太坊的交易过程、gas机制、存储结构、编写语言做了简要介绍,在此基础上调查归纳了智能合约中常见的8种漏洞类型,解释了漏洞产生的原因,回顾了一些真实发生的安全事件并给出了漏洞示例代码;根据不同的技术手段,如符号执行、模型检测、定理证明等,对智能合约的形式化验证工作做分类介绍,分析了各种方法的优劣,并选取了3个开源的自动化验证工具Mythril、Slither和Oyente,从运行效率、检测漏洞类型以及准确率等方面作出实验评估和对比;研究了目前已有的相关综述文章,总结了这些研究的区别与优势;概述了智能合约的漏洞检测技术中仍存在的关键问题,对智能合约验证工作的现状进行了分析和展望,提出了未来能够进一步研究的方向.
文献关键词：
智能合约;形式化方法;区块链;以太坊;程序验证
中图分类号：
作者姓名：
张文博;陈思敏;魏立斐;宋巍;黄冬梅
作者机构：
上海海洋大学信息学院,上海 201306;上海市高可信计算重点实验室,上海 200062;上海电力大学,上海 201306
文献出处：
引用格式：
[1]张文博;陈思敏;魏立斐;宋巍;黄冬梅-.基于形式化方法的智能合约验证研究综述)[J].网络与信息安全学报,2022(04):12-28
A类：
自动化验证工具,Mythril,Slither,Oyente
B类：
形式化方法,智能合约,区块链技术应用,可编程,扩展性,安全事件,安全性问题,代码,存在缺陷,严重后果,以太坊,交易过程,gas,存储结构,真实发生,示例,符号执行,模型检测,定理证明,形式化验证,开源,测漏,实验评估,漏洞检测,分析和展望,程序验证
AB值：
0.276635
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
