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

2021 年 5 月 8 日 专知

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

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

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

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