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

2021 年 5 月 8 日 专知


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


区块链技术已在金融、云计算、物联网等众多工业 领域中取得了广泛的应用.智能合约作为第二代区块 链技术的创新发展以及其丰富的可发展内涵,已经越 来越引起业界的重视和宽广的应用预期,成为区块链技术链上最具有发展的核心技术,在数字化的发展进 程中起着越来越重要的作用.智能合约是一段脚本代 码,它允许在没有第三方的情况下进行可信交易,这些 交易可追踪且不可逆转.智能合约和区块链技术结合 以来已经有广泛的应用,承载了巨大的价值和交易量, 但同时,由智能合约引发的区块链安全问题也十分突出.据研究人员统计[1] ,超过 34000个智能合约都有可 被利用的安全隐患,有的造成非常重大的损失,随着应 用深入,总体呈上升趋势.


频频爆出的智能合约安全事件,使得越来越多来 自学术界和工业界的研究人员开始将注意力集中在 使用形式化方法来验证智能合约,以保证其功能的正 确性和运行时的安全性.形式化方法(formalmethods) 是基于数学的技术,用于系统或计算机软件的规范, 开发和验证,在逻辑科学中是指分析、研究思维形式 结构的方法,形式化方法设计包括描述语言,建模,模 型验证,模型转换和自动代码生成等系列阶段形成的 自顶向下的设计方法,已经获得业界的认可,目前在 诸如航空航天等安全关键实时的系统中应用较多.智 能合约可以看作一种特殊的安全关键软件,不同之处 在于它要求价值转移的安全与准确.并且它作为合 同,要求多方达成一致,更加需要形式化验证的过程 来保证多方认可. 


当前对形式化方法验证智能合约领域的综述类文 章较少,经过调研,国内外有 2篇相关著作.2019年, Singh等人[2] 对形式化方法解决智能合约存在的七个问 题进行综述,包括区块链协议和扩展性问题等.同年, Liu等人[3] 对智能合约的安全性研究进行了综述,主要 包括智能合约的安全性保证和安全性验证,后者涉及 了对形式化验证技术的讨论. 本文广泛收集了基于形式化方法验证智能合约领 域的相关研究,选取标准为该文献对智能合约的形式 化验证提出了新技术,新理论或该文献对智能合约形 式化验证的相关理论和技术提供实证研究支持.本文 收录的对象为 2015年以来符合定义的文献选取标准的 相关研究,经过大量的筛选,从中挑出 47篇相关的论 文.我们将每篇论文聚焦的问题可分为智能合约的功 能性问题,隐私性问题,安全性问题和语义一致性问题:合约功能性问题是指智能合约的行为是否符合预 期,合约状态是否满足规约条件;合约隐私性问题主要涉及智能合约的数据加密算 法,协议各方的隐私保护措施;合约的安全性通常包括有界性,可达性和无状态 二义性.当这些性质不被满足时,通常会引发安全漏洞, 例如重入,整数溢出,变量未初始化等;语义一致性问题主要讨论源代码与转换后的目标 代码之间是否一致.



专知便捷查看

便捷下载,请关注专知公众号(点击上方蓝色专知关注)

  • 后台回复“智能合约” 就可以获取智能合约的形式化验证方法研究综述》专知下载链接



专知,专业可信的人工智能知识分发 ,让认知协作更快更好!欢迎注册登录专知www.zhuanzhi.ai,获取5000+AI主题干货知识资料!


欢迎微信扫一扫加入专知人工智能知识星球群,获取最新AI专业干货知识教程资料和与专家交流咨询
点击“ 阅读原文 ”,了解使用 专知 ,查看获取5000+AI主题知识资源
登录查看更多
15

相关内容

专知会员服务
62+阅读 · 2021年5月3日
专知会员服务
35+阅读 · 2021年3月21日
跨媒体分析与推理技术研究综述
专知会员服务
69+阅读 · 2021年3月11日
专知会员服务
30+阅读 · 2021年3月7日
专知会员服务
182+阅读 · 2021年2月4日
专知会员服务
15+阅读 · 2021年1月23日
专知会员服务
49+阅读 · 2020年12月28日
机器学习模型安全与隐私研究综述
专知会员服务
110+阅读 · 2020年11月12日
深度学习目标检测方法综述
专知会员服务
268+阅读 · 2020年8月1日
基于深度学习的表面缺陷检测方法综述
专知会员服务
92+阅读 · 2020年5月31日
多模态视觉语言表征学习研究综述
专知
25+阅读 · 2020年12月3日
【数字孪生】数字孪生技术发展趋势与安全风险浅析
产业智能官
53+阅读 · 2019年8月28日
网络安全威胁情报相关汇总
计算机与网络安全
6+阅读 · 2019年8月9日
综述 | 机器视觉表面缺陷检测
计算机视觉life
8+阅读 · 2019年8月2日
区块链隐私保护研究综述——祝烈煌详解
计算机研究与发展
22+阅读 · 2018年11月28日
形式化方法的研究进展与趋势
中国计算机学会
35+阅读 · 2018年11月8日
机器视觉技术的农业应用研究进展
科技导报
7+阅读 · 2018年7月24日
【区块链】区块链是什么?20问:读懂区块链
产业智能官
8+阅读 · 2018年1月10日
Arxiv
103+阅读 · 2021年6月8日
Arxiv
19+阅读 · 2020年12月23日
A Survey on Edge Intelligence
Arxiv
50+阅读 · 2020年3月26日
A Comprehensive Survey on Transfer Learning
Arxiv
119+阅读 · 2019年11月7日
Arxiv
5+阅读 · 2019年4月25日
Learning From Positive and Unlabeled Data: A Survey
Arxiv
5+阅读 · 2018年11月12日
VIP会员
相关VIP内容
专知会员服务
62+阅读 · 2021年5月3日
专知会员服务
35+阅读 · 2021年3月21日
跨媒体分析与推理技术研究综述
专知会员服务
69+阅读 · 2021年3月11日
专知会员服务
30+阅读 · 2021年3月7日
专知会员服务
182+阅读 · 2021年2月4日
专知会员服务
15+阅读 · 2021年1月23日
专知会员服务
49+阅读 · 2020年12月28日
机器学习模型安全与隐私研究综述
专知会员服务
110+阅读 · 2020年11月12日
深度学习目标检测方法综述
专知会员服务
268+阅读 · 2020年8月1日
基于深度学习的表面缺陷检测方法综述
专知会员服务
92+阅读 · 2020年5月31日
相关资讯
多模态视觉语言表征学习研究综述
专知
25+阅读 · 2020年12月3日
【数字孪生】数字孪生技术发展趋势与安全风险浅析
产业智能官
53+阅读 · 2019年8月28日
网络安全威胁情报相关汇总
计算机与网络安全
6+阅读 · 2019年8月9日
综述 | 机器视觉表面缺陷检测
计算机视觉life
8+阅读 · 2019年8月2日
区块链隐私保护研究综述——祝烈煌详解
计算机研究与发展
22+阅读 · 2018年11月28日
形式化方法的研究进展与趋势
中国计算机学会
35+阅读 · 2018年11月8日
机器视觉技术的农业应用研究进展
科技导报
7+阅读 · 2018年7月24日
【区块链】区块链是什么?20问:读懂区块链
产业智能官
8+阅读 · 2018年1月10日
相关论文
Arxiv
103+阅读 · 2021年6月8日
Arxiv
19+阅读 · 2020年12月23日
A Survey on Edge Intelligence
Arxiv
50+阅读 · 2020年3月26日
A Comprehensive Survey on Transfer Learning
Arxiv
119+阅读 · 2019年11月7日
Arxiv
5+阅读 · 2019年4月25日
Learning From Positive and Unlabeled Data: A Survey
Arxiv
5+阅读 · 2018年11月12日
Top
微信扫码咨询专知VIP会员