以太坊智能合约安全形式化验证方法研究进展

王赫彬，郑长友，黄 松，孙金磊，丁一先

(1.中国人民解放军陆军工程大学 指挥控制工程学院，江苏 南京 210007；2.中国人民解放军陆军工程大学 全军军事训练软件测评中心，江苏 南京 2100073.辽宁工程技术大学，辽宁 阜新 123000)

0 引 言

自2009年Satoshi Nakamoto的比特币发布以来，出现了各种各样的区块链实现。而自从2013年底Vitalik Buterin发布的以太坊白皮书将智能合约的概念引入到区块链之中，区块链技术的应用变得更加广泛，并使得比特币等加密货币的可编程能力更进一步。智能合约提供了一个框架，允许以可信任、去中心化的方式执行一个应用程序的业务逻辑。智能合约用户通常携带大量的价值数以亿计的货币，但是智能合约作为一种计算机代码可能具有未发现的和未知的漏洞，具有很大的安全隐患。2016年6月17日的The DAO攻击事件中，一名攻击者利用去中心化自治组织(decentralized autonomous organization，DAO)部署的智能合约代码中的多个漏洞，控制了当时价值约为5 000万美元的以太坊网络，并从合约中盗走了350多万以太币；2018年美链BEC上百亿项目归零、BAI(blockchain of artificial intelligence and internet of things)任意账户无限转账都是因为ERC20代币标准中出现的一系列漏洞，导致资金恶意发送转移，正常的矿工节点受到了危害。对于难以避免的智能合约安全性问题来说，在部署链上前发现并修复漏洞至关重要。

虽然现有的一些工作通过基于测试的检测方法来检测漏洞，但不能完备地发现智能合约源码和字节码中所有的漏洞，而且对于智能合约在一些概念和属性的正确表达缺乏全面的检查。而现有的一些代码及合约审计工作则依赖于审计专家的个人经验和主观判断，缺乏严谨性和说服力。形式化验证方法则通过证明序列、逻辑语句检查数学模型的逻辑，以证明某些规范的正确性并发现运行时错误，理论上可以发现更多的漏洞。智能合约对于安全性要求高，代码量相对较小，这些特点很适用于进行小型的形式化验证。文中对以太坊智能合约的相关概念进行了系统的介绍，分析了智能合约常见的漏洞类型，总结了常见的形式化验证方法，进行了实验结果分析并讨论了目前形式化验证工作存在的问题和挑战，提出了将来的改进方法及意见建议。

1 背景及相关概念介绍

1.1 以太坊智能合约

以太坊平台于2015年提出，是使用区块链平台执行智能合约的最流行的底层系统之一[1]。其市场容量达到了1 000亿美元，每天处理超过40万笔资金交易。以太坊包含以太坊虚拟机、执行环境(账户管理、默克树等)和共识算法三个部件，适用于公有链、私有链和联盟链三种区块链环境。不同的区块链环境可以通过扩展包的形式，将以太坊智能合约部署到链上。以太坊智能合约是部署在其平台上的一种计算机协议，具有可编程、可维护和安全可信等特点[2]。特别地，智能合约的执行过程是从一个状态到另一个状态[3]，可以用有限状态机将智能合约形式化地表示为一个五元组自动机Q*:

Q*=(Q0,Ω,ζ,t*,G*)

其中，Q0是合约执行自动机的所有状态的集合，Ω为所有输入事件的集合，ζ:Q0×Ω→Q0则是转移函数的集合，t*∈Q0为初始状态,G*⊂Q0为终止状态集合。

1.1.1 以太坊虚拟机

智能合约通常用有别于现有编程语言的高级语言编写，开发人员在编写完智能合约代码后，代码被编译成以太坊虚拟(Ethereum virtual machine，EVM)字节码在计算机上执行。EVM是一种完全基于堆栈的虚拟机架构，支持一个包含134个操作码的指令集，运行在256比特的基本数据类型之上。与Java虚拟机(Java virtual machine，JVM)相比，EVM相对更加简单，执行效果更加具有确定性。图1是一个合约代码被EVM编译成字节码的示例。

图1 智能合约代码编译过程示例

1.1.2 智能合约语言

智能合约通常使用专门的智能合约语言进行编写[4]。智能合约语言包含高级语言、中间级语言(intermediate representation，IR)和低级语言三种类型。开发人员通常使用高级语言编写智能合约，因为高级语言能够提供期望的表达方式。IR语言介于高级语言和低级语言之间，可以用于编写程序以推导属性和检查规范，也可以用于优化代码的结构。而低级语言则提供了一种在分布式虚拟机上执行的实现方式。基于合约语言不同的安全特性，可以采用不同的方法对合约进行形式化验证。其中Solidity、Vyper是以太坊平台常用的智能合约高级语言，EVM是其常用的低级语言，而EthIR和Yul是其常用的中间语言。

1.2 常用的形式化验证方法

形式化验证方法[5]是指在形式化建模的基础上，对具有精确语法和语义的形式化语言的系统建立事务及性质等的关系，从而验证系统所应具有的功能正确性和其他关键性质。

1.2.1 定理证明

定理证明[6]适用于很多系统，方法流程是对其进行形式化规约，并将要证明的命题写为“待验证系统满足形式化规约”，从而将验证问题转化为证明一个可满足性问题，使用预先定义的公理和推理规则作为输入来完成证明过程。定理证明分为交互式定理证明、自动化定理证明和混合定理证明三种[7]，而不同类型系统的复杂度决定了不同定理证明方式的可行性。复杂度较小的可以使用自动化定理证明，复杂度较大的则可以使用交互式定理证明。

1.2.2 模型检测

模型检测[8]是指对于一个协议框架利用逻辑公式进行检查，观察该协议描述的需求或系统是否具有某些期望的性质。通常需要验证的性质包括安全性(safety)、活跃性(liveness)、无阻性(non-blocking)和非严格顺序性(no strict sequencing)等。该方法适用于可以用有限状态模型表示的系统。模型检测器可以自动化完成精准模型和规范的检测，给出可用的判断结果。

1.3 常见的漏洞类型

随着智能合约语言的迭代更新，不断有新的漏洞被修复，但同时新的版本语言的语法也会带来新的安全漏洞隐患。截至2020年8月，Solidity语言从0.3.x版本更新到了0.7.0版本。按照漏洞来源依赖，以太坊智能合约漏洞可以分为区块链依赖漏洞、软件安全依赖漏洞和以太坊及合约语言依赖漏洞[9]。图2是一些以太坊智能合约的常见漏洞。

2 相关研究进展

本节将介绍智能合约形式化验证的一些最新技术研究进展。暂时没有一个固定的标准对于这些形式化验证方法进行分类，但是已经有很多研究对于智能合约的正确设计和漏洞挖掘产生了效果。借鉴了1.2节传统的形式化验证方法，可以采用以下几种技术手段对智能合约进行形式化验证。

2.1 类型推断

基于类型推断的形式化验证使用数十行或数百行的核心类型理论来替换智能合约语言的类型或类型子集，能够用来快速证明数学定理。这种方法使用函数式程序语言，更多地关注类型检查，而不是运行程序，具有相对简单的语法。这种方法的一般流程为：首先将智能合约高级语言翻译成函数式程序语言，指定源语言中的数据在验证语言中的数据格式和数据类型，并转换包含这些数据的源语言中的函数；然后提出并证明关于这些函数的定理，可以完成运行时程序正确性的验证。

微软研究院和哈佛大学研究团队的Bhargavan等人[10]提出了一个用于形式化分析的F*框架，试图通过将合约代码翻译成F*语言后，通过类型推断来验证智能合约。该框架包括Solidity*和EVM*两个工具原型，Solidity*支持Solidity的部分语法类型转换，将智能合约从Solidity语言翻译成F*语言，EVM*再从EVM字节码形式反编译成F*语言。转换过程中支持递归，不支持循环。Solidity*运用类型推导发现运行时函数和变元的错误和违反的规范，EVM*则可以分析低层次的属性，估算gas消耗的上界。验证了396份合约，其中46份成功地进行了翻译和类型检查，发现了一些可重入漏洞和未经检查的send语句返回调用问题。

Coblenz等人[11]研发的Obsidian是一种面向类型的安全区块链编程语言，该语言以用户为中心，用户实验反馈与语言开发同时进行，类型状态依赖系统保证了程序员编写正确的合约。针对可用操作依赖的高级状态、代码错误导致的资金损失或挪用和不一致状态导致的重入攻击等三种严重的bug源，类型状态会将动态信息记录到类型之中，之后进行静态的类型推断，同时，线性类型系统计算货币的数量，完成对于交易过程中的财务信息追踪溯源。

Schrans等人[12]开发了一种专门用于编写鲁棒性智能合约的静态类型编程语言Flint，引入保护块(protection blocks)根据类型状态限制运行代码的时间和用户，对于状态的写入进行了限制，简化了合约的推理。具有调用保护、默认不变量、资产类型推理和安全语义等安全特性，实现了安全的内部及外部资金转移(asset transfer)、事件监控和安全的算术运算等代码保护功能，通过限制交易过程中的类型状态，将Solidity语言的安全性进行了提升，避免了智能合约重入漏洞和整数溢出等问题的出现。目前，智能合约交互语言Rholang[13]和Plutus[14]分别使用ρ演算和λ演算等抽象演算方法，完成了一些验证工作。

2.2 交互式定理证明

智能合约的交互式定理证明是传统的定理证明方法在智能合约验证中的应用。智能合约高级语言如Solidity和低级语言如EVM上的字节码需要被定义成可以为定理证明器编译的语言，然后再利用交互式定理证明验证以太坊智能合约的安全性质。定理证明器也可以选择用一些自动化SMT定理证明器，SMT求解器使用一阶逻辑语言来表示命题，然后通过枚举赋值的方式进行证明。可满足命题的赋值为程序提供正确的输入，可以证明在执行路径中给定的状态是可达的。

Amani等[15]研发的eth-isabelle是一种作用于EVM字节码的Isabelle/HOL定理证明器。首先将EVM字节码序列语义用Lem语言形式化构造成线性代码块，将EVM指令划分为以JUMPDEST为开始的基本块、JUMP、JUMPI等跳转指令以及其他指令基本块三种，然后再翻译到Isabelle/HOL或Coq中进行定理证明。基于以太坊的gas机制给出了一种out-of-gas异常处理方法，使用分离逻辑(separation logic)验证以太坊虚拟内存中的字节码程序，支持使用程序规则、基本块规则和指令规则自动生成验证条件和验证规范，降低了EVM操作码形式智能合约形式化验证的时间复杂度。

Lei等[16]提出的Lolisa是Solidity语言的一个大型子集的形式化语法和语义，采用了更鲁棒的静态类型系统，不仅包含了Solidity中映射符、修改器、合约类型和地址类型等语法组件，而且还包含了诸如多个返回值、指针算法以及结构和字段访问等通用编程语言特性。基于Solidity语言的可扩展性，提出将Lolisa扩展到其他合约编程语言的方案。接着开发了一种支持不同验证范式的可扩展、可重用的形式化内存框架GREM，模拟了物理内存的硬件结构，并且使用Coq提供了一套防干扰的应用程序编程接口(application programming interfaces，API)，实现了一个独立可定制的框架。之后开发的执行时验证同构体(execution verification isomorphism，EVI)将符号执行与定理证明结合，提高了高阶逻辑定理证明辅助工具的自动化程度，并且证明了Lolisa可满足于EVI。

Yang等人[17]开发的FEther编译器是一种基于Coq的混合定理证明工具，基于Solidity语言的形式化语法和语义子集Lolisa，结合符号执行和高阶逻辑定理证明，提高了执行和验证合约的自动化程度，同时FEther具有很好的可重用性，可以将验证过的代码片段复用检查其他代码段的属性，其运行效率远远超过Coq标准教程中的解释器。是第一个在Coq中对于Solidity语言进行语法和语义定义的证明引擎。Annenkov等人[18]提出了一个基于Coq的框架ConCert，可以对于智能合约进行形式化证明鉴定。

Sergey等[19]研发的中间语言Scilla提供了一个编程组件，为智能合约间的通信提供了一个计算与交互的分离、效率和纯计算的分离及调用动作和连续过程的分离等，允许丰富的交互模式，具有规则形式写成的语义，将Scilla嵌入Coq之中，易于进行形式化验证。描述了基于自动机[20]的Scilla模型，展示了自动机关于安全和时间等属性的简化验证过程。除了Coq和Isabelle/HOL等工具外，Why3[21]也实现了EVM的语义表示，可以基于EVM字节码进行一些智能合约的定理证明。

2.3 有界模型检测

智能合约的模型检测中常用的方法为有界模型检测(bounded model check，BMC)，有界模型检查器系统地、象征性地研究系统的行为，直到某个边界k，寻找对给定属性的违反，其中边界k表示允许从某个初始状态进行的转换的数量。使用单个逻辑语句检查智能合约的性质及规范，若合约状态转移符合规范，则证明智能合约满足所验证的安全特性；否则构造模型检测器会构造一个状态转移的反例，证明合约违反了该条规范，存在安全性问题。

牛津大学的Antonino等[22]开发了一种基于Solid语言的有界模型检测工具Solidifier，Solid语言对于Solidity语言和以太坊区块链进行形式化描述，之后将Solid转换成中间语言Boogie[23]，使用Corral[24]对于Boogie语言形式的合约进行有界模型检测。提出合约验证和函数验证两种工具，定义main过程和捕获Solid调用结构的callP过程，探索区块链的行为，寻找合约错误。通过特定代码模式匹配或未预料到的行为方式，查找不符合开发人员意图的程序错误及状态。

Joel等[26]开发了一种基于符号执行的有界模型检测工具ETHBMC，设定了Keccak256函数、Memcopy-like指令和Inter-Contract交互等测试断言，建立了以太坊的攻击模型、内存模型和数据调用模型等，然后符号执行检测模块中的漏洞，对于每个具有易受攻击的路径生成交易过程实例。通过对于当前go-ethereum区块链工具套件中活跃的大约220万个用户大规模分析，自动生成5 905个触发漏洞的有效输入，与之前的分析方法相比较，具有22.8%的更多输入。

Zhang等[27]开发了一个用4 800多行Python和C++写成的有界模型检测工具NPCHECKER，处理Solidity及Vyper语言的不确定性对于合约付款等交易过程的影响。发现由于不可预测的事务调度和外部未知的被调用者行为而读写更改的合约全局变量，公开了各种不确定性因素和问题。NPCHECKER的工作流程为：首先将EVM字节码反编译，然后利用内联汇编将汇编指令转换成LLVM，恢复控制流图，最后使用SMACK[28]和Boogie等模型检测工具检查恢复的IR代码中是否含有NPⅠ和NPⅡ两种付款bug。在以太坊主网上收集到3万多份在线合约并对其进行了评估。NPCHECKER在1 111份合约中检测到不确定性支付，识别了六种未知的新漏洞类型。目前，NuSMV[29]、SPIN[30]等传统的模型检测工具被用于能源交易市场、网上购物等智能合约，完成需求规范开发阶段和最终系统验证集成阶段的交互验证。

2.4 其他验证方法

除了以上研究深入广泛的以太坊智能合约形式化验证方法外，根据以太坊智能合约框架的性质用途和工作流程，还有很多结合紧密的验证方法产生更加具有领域自适应性的应用。本节介绍几种在主流的智能合约形式化验证之上有所改进的方法。

2.4.1 用户和区块链行为建模

传统的模型检测方法可以对智能合约及其用户进行建模，但是不能对底层的区块链进行建模。Abdellatif等[31]提出了一种对于区块链及其用户进行建模的方法，按照行为交互优先级(behavior interaction priorities，BIP)使用统计型模型检测器(statistical model checking，SMC)进行验证。对于给定的系统B和性质δ，SMC模型检测器使用概率有界线性时序逻辑(probabilistic bounded linear time logic，PB-LTL)来判断B是否满足δ。令B满足δ记为B|=δ，首先判断公式：

P({B|=δ})>θ

是否成立，其中P(.)为某个事件发生的概率，θ为某个选定的阈值；然后估算P({B|=δ})的值p，使得估计值p0满足：

P(|p-p0|≤α)≥1-β

其中，α为估计精度，β为攻击风险水平。运用该方法能够发现传统模型检测方法难以发现的易受攻击用户行为和交易路径。

2.4.2 博弈论

Giancarlo等[32]提出了一种利用博弈论(game theory)来对涉及物理行为的智能合约进行验证的方法。首先通过博弈论分析交易过程中顾客和商家的行为，观察两方行为的相互影响，然后使用概率模型检测器PRISM通过分析顾客和商家不确定的选择行为对于选择事件对应的概率的影响，将行为建模成离散时间马尔可夫决策过程(discrete time Markov decision process，DTMDP)，来解决不确定性问题。根据顾客的诚实度和商家的信誉使用了六种存款与出售价格比率，对于一组诚实的顾客与不诚实的商家，商家损失30%的可能性不大于2%，顾客损失30%的可能性却可以达到50%。

2.4.3 着色Petri网

Wang等[33]改进了字节码的程序逻辑规则，应用霍尔条件(Hoare condition)建立了着色Petri网(colored Petri Nets，CPN)模型。首先，对于Solidity源代码形式的智能合约，利用ANTLR语法分析器建立抽象语法树(abstract syntax tree，AST)模型并解析抽象语法树中的元素，生成等价的CPN模型；然后，对于EVM字节码形式的智能合约，对于字节码序列对应的操作语义进行静态分析，划分出具有不同特征的基本块，构建控制流图(control flow graph，CFG)，生成等价的CPN模型。最后，将之前建立的CPN模型放入CPN工具中完成动态仿真和模型检测。该方法设计了一种自动化的建模方法，引入了一个自定义调用库和一种基于回溯的路径推导算法，提高了传统模型检测方法的针对性和有效性。

2.4.4 K框架

K框架[34]是一种可执行的程序框架语义集，可以用于形式化智能合约，对事务进行状态和网络演化进行建模，并使用转换规则来详细阐述状态的修改和网络的演化。K框架在逻辑上可以分成三个模块:data.k,language.k和ethereum.k，目的是与以太坊的依赖结构保持一致。Hildenbrandt等[35]在K框架中定义了一个EVM的语义—KEVM，将EVM表示成K框架范式中的ENBF样式提供的语言语法、状态配置描述和驱动程序执行的转换规则三个主要组件，深入解释了KEVM的结构定义描述，然后给出了几种语义扩展，根据ERC20标准验证了标准代币的两种不同语言实现，使用K框架的可达性逻辑证明器，表现了KEVM语义框架的可用性。此外，该框架还可用于gas消耗分析和解析以太坊白皮书中EVM的语言规范等。KVyper[36]由Vyper到LLL、LLL到EVM两个翻译器组成，可用于发现Vyper编译器中存在的错误。KSolidity[37]是K框架中Solidity语义的定义，可用于Solidity语言合约测试。

除此之外，ZEUS[38]和Oyente[39]也使用形式化验证的方法分别在源码级和操作码级进行了自动化的漏洞检测，并发现了一些以太坊智能合约存在的安全漏洞。

3 总结与展望

3.1 现有研究存在的不足

如第二节所述，智能合约形式化验证工具发展迅速，但是仍有一些缺陷，主要问题如下：

(1)合约语言不完整。不同的形式化验证方法通常能够验证合约语言的一个子集，而不能完整地验证所有智能合约可能出现的问题。总结一些常用形式化验证方法对于智能合约的处理，如表1所示。

表1 智能合约形式化验证框架/工具对比分析

可以看出，很多语言只能处理合约语言的一个语义语法子集，如FEther基于Solidity语言的Lolisa子集进行证明，不能对整个Solidity语言进行验证，查找漏洞的手段较少，发现漏洞的类型不足。有些待验证的规范可能包含类型特性子集之外的语义语法元素，导致难以验证智能合约满足的性质及规范。扩展可验证的合约语言子集，建立更多的验证范式，发现更多的漏洞类型是一个需要解决的技术问题。

(2)应用范围受限。由于智能合约仍是一个较新的领域，因此形式化验证缺乏一个统计评价标准和最佳实践，方法应用没有突破高昂成本、合约规模等技术局限。文中选取了106个Solidity源码合约样本结合偷以太币(Steal Ether)、黑杰克(Hijack)和自毁(Suicidal)三种攻击行为，对Solidifier和ETHBMC两种有界模型检测工具检查效果进行对比，其编译通过率和漏报率结果如表2所示。三种工具都存在较多的问题漏报的情况。此外，形式化验证还只适用于简化的合约模型，采用的启发式方法难以扩展到复杂的合约中去。自动化程度不高，且缺乏对于高阶业务逻辑范式的证明。

(3)验证语言安全性未知。在验证的过程中，通常需要将源代码形式或字节码形式的合约翻译成另一种语言，例如F*方法，但是验证语言的安全性没有得到保证，具有很大的安全隐患。翻译过程的正确性也是未知的，很有可能出现转换前后的类型有很大差别。因此证明或提高验证语言的安全性及翻译过程的正确性是形式化验证面临的一些重难点工作。

3.2 未来研究方向和改进思路

针对现有工具存在的问题，提出如下未来改进思路：

(1)扩展形式化验证方法的应用范围。由于缺乏测试判定准则(test oracles)，验证好坏通常难以衡量。所以需要建立标准的测试判定用例集，对于验证方法的有效性进行定性定量评估。通过建立综合评价指标体系，找出实践性好的验证方法及工具，有助于在此基础上对智能合约的形式化验证进行改进和提高。通过与符号执行、污点分析等方法的结合，提高形式化验证方法的自动化程度，创建可重用的验证模式库，减少验证所需时间，增强合约验证方法的可用性。

(2)提高形式化验证方法的验证效果。针对智能合约形式化验证过程不直观的问题，可以通过类型标记、着色Petri网等增强合约验证的可视化效果，利用逆向工程重新构造合约执行的控制流图。根据以太坊智能合约具有的一些性质和用途，建立具有严谨可靠数学基础的区块链模型和智能合约机制模型，提高以太坊平台合约验证的效果。

4 结束语

以太坊为代表的智能合约平台的出现扩展了区块链的资金转移能力，促进了区块链2.0时代的到来。文中梳理了以太坊智能合约常用的语言和常见的漏洞类型，讨论了基于类型推断的形式化验证、智能合约的交互式定理证明和智能合约的有界模型检测等主流的智能合约形式化验证方法，通过对几种现有形式化验证工具的实验结果分析研究发现，并针对现有方法的不足之处，提出了未来研究的改进思路。下一步工作的重点和难点在于根据以太坊智能合约的实现机制、环境状态和网络演化等内部性质用途，提出具有自适应性的理论着力提高验证的准确性，减少时间和空间成本，扩展验证的适用范围，进一步提高以太坊智能合约的安全开发部署能力。