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

作     者：张文博 陈思敏 魏立斐 宋巍 黄冬梅 ZHANG Wenbo;CHEN Simin;WEI Lifei;SONG Wei;HUANG Dongmei

作者机构：上海海洋大学信息学院上海201306 上海市高可信计算重点实验室上海200062 上海电力大学上海201306 

基　　金：国家自然科学基金(61872142,62102243,61972241) 上海市青年科技英才扬帆计划(21YF1417000) 上海市高可信计算重点实验室开放课题 上海市自然科学基金面上项目(18ZR1417300) 上海市科委部分地方高校能力建设项目(20050501900) 上海海洋大学青年教师科研启动项目 

出 版 物：《网络与信息安全学报》 (Chinese Journal of Network and Information Security)

年 卷 期：2022年第8卷第4期

页      码：12-28页

摘      要：智能合约是区块链技术应用的一个重要场景,智能合约技术实现了区块链的可编程化,提高了其扩展性,有广阔的应用前景。然而,一系列关于智能合约的安全事件造成了大量经济损失,削弱了人们的信心,安全性问题已经成为制约智能合约进一步发展的关键问题。如果合约设计和代码实现的过程中存在缺陷,可能会造成严重后果。而智能合约发布后无法修改,因此,在智能合约发布前对其正确性做出验证尤为重要。近年来,国内外学者在智能合约的验证领域取得了大量成果,但对这些研究成果的系统分析和总结相对较少。对以太坊的交易过程、gas机制、存储结构、编写语言做了简要介绍,在此基础上调查归纳了智能合约中常见的8种漏洞类型,解释了漏洞产生的原因,回顾了一些真实发生的安全事件并给出了漏洞示例代码;根据不同的技术手段,如符号执行、模型检测、定理证明等,对智能合约的形式化验证工作做分类介绍,分析了各种方法的优劣,并选取了3个开源的自动化验证工具Mythril、Slither和Oyente,从运行效率、检测漏洞类型以及准确率等方面作出实验评估和对比;研究了目前已有的相关综述文章,总结了这些研究的区别与优势;概述了智能合约的漏洞检测技术中仍存在的关键问题,对智能合约验证工作的现状进行了分析和展望,提出了未来能够进一步研究的方向。

主 题 词：智能合约 形式化方法 区块链 以太坊 程序验证 

学科分类：12[管理学] 1201[管理学-管理科学与工程类] 08[工学] 081201[081201] 0812[工学-测绘类] 

D　O　I：10.11959/j.issn.2096−109x.2022041

馆 藏 号：203114076...