The DAO 事件的形式化分析

2021-05-19朱雪阳

网络安全与数据管理 2021年5期

朱雪阳

(1.中国科学院软件研究所计算机科学国家重点实验室，北京100190；2.中国科学院大学，北京100049)

0 引言

化名为“中本聪”(Satoshi Nakamoto)的学者于2008年提出了比特币概念并于2009 年初发行了最初的50 个比特币[1]。随后，人们发现比特币底层所用的区块链技术并不仅仅限于加密数字货币的应用[2]；特别是提供智能合约[3]编程的开放区块链平台以太坊(Ethereum)[4]的创立，使区块链技术的发展更加生机勃勃。

区块链是一种将数据区块按照时间顺序组织起来的加密链式结构，是一种不可篡改和不可伪造的去中心化共享账本。加入智能合约后，区块链技术可看作是一种新型的去中心化基础架构与分布式计算范式[5]。有了智能合约，开发人员能够在区块链上建立和发布各种分布式应用，为区块链技术的应用提供了无限的可能。

智能合约最初由SZABO N 提出[6](1997 年正式发表[7])，是以数字形式定义的一组承诺，以及合约参与方执行这些承诺所需的协议。智能合约的本质是运行于区块链这一去中心化基础架构上的分布式程序，是运行在共享区块链数据账本上的商业逻辑，在被触发时自动执行。

正如软件在网络安全的研究与实践中扮演着至关重要的角色，几乎所有的网络攻击都是利用系统软件或应用软件中存在的安全缺陷实施的[8]。在区块链系统安全中，智能合约也扮演着重要的角色。如著名的The DAO 事件[9]，由于智能合约中存在安全漏洞，黑客得以窃取在当时价值超过五千万美元的360 万个以太币。智能合约的安全(security)问题得到广泛关注[10]；许多用于合约漏洞检查的原型工具应运而生，如采用符号化执行[11]方法的工具Oyente[12]、Mythril[13]、Manticore[14]和Securify[15]等，以及在线检查合约漏洞的工具如文献[16]和文献[17]等。

在The DAO 事件中，造成重大损失的根源在于合约中存在一种被称为重入(Reentrancy)漏洞的错误。本文通过形式化分析来更清晰地展示该漏洞特点及攻击行为，并以此为例介绍基于模型检测技术的智能合约形式化验证方法。

1 DAO 合约及重入漏洞

本质上，一个智能合约文本描述了一个类，部署上链后，相当于生成一个该类的实例对象；链上的合约对象之间、外部地址与合约之间通过消息传递通信。因此，智能合约的设计及行为方式本质上遵从面向对象范式。为突出所要分析的问题，参照文献[16]的方法，将The DAO 合约中与重入漏洞相关的代码提取表示为如图1 所示的DAO 对象。

图1 表示合约DAO 的一个对象[16]

为便于阐述问题，将合约的余额balance 显式地定义在DAO 对象中。每个合约的参与对象o 有一个账号余额credit[o]。参与对象可通过调用方法deposit()存入一定数额的以太币，其余额相应增加；也可通过调用方法withdrawAll()将其存入的以太币全部取出，其余额清零。显然，在这个合约中，余额一致性要得到满足：对合约DAO 的任何操作都要保证DAO 的余额(balance) 是所有参与对象余额(credit[o])的总和。即合约应满足不变式(Invariant)：(sum o: credit[o])=balance。

仅从DAO 合约看，这一要求似乎一定能得到满足：方法deposit()在第6 行增加完credit[o]后接着在第7 行相应增加balance；方法withdrawAll()在第3行从balance 中扣减对象o 的余额并在第5 行将credit[o]清零。当withdrawAll()执行时，会调用对象o的方法pay()。如果参与对象是图2 左列所示Good-Client，上述不变式确实能够得到满足。但是，由于DAO 合约部署在区块链上，任何外部对象都有可能对它进行操作，结果可能出乎合约设计者的预料。例如，如果参与对象是图2 右列所示的Attacker，那么它的方法pay() 将回调Dao.withdrawAll()，引起DAO 的状态变化，并破坏上述不变式。

图2 合约DAO 的可能调用对象[16]

所以，DAO 合约存在的使重入攻击有可能实现的漏洞，一般称为重入漏洞。The DAO 事件中，攻击者正是利用这一漏洞窃取了大量以太币。

重入漏洞的产生主要是对使用模式的不确定性估计不足，只考虑到合规的使用而没预料到可能的攻击模式。工具如Oyente 等只要检测到有回调情况就汇报该漏洞，存在误报的情况。因为回调并不是产生重入漏洞的必然原因。例如，将DAO 合约中第5 句移到第2.5 句，则无论GoodClient 还是Attacker都不会破坏余额一致性，任何参与对象都不可能取出超过其余额的以太币。

2 基于模型检测的漏洞分析方法

模型检测[18]是基于状态搜索的一种形式化验证方法，是模拟和测试方法的自然延伸。它是迄今为止最为成功的形式化方法，在计算机硬件、软件、网络与通信协议、控制系统、认证协议等领域都得到应用。在智能合约验证方面也有一些尝试[19-21]。

模型检测工具应用算法自动验证并发系统抽象模型是否满足给定性质，对不满足性质的模型能生成反例。比较著名的模型检测工具有SPIN[22]、NuSMV[23]和UPPAAL[24]等。基于模型检测的漏洞分析如图3 所示。

图3 基于模型检测的分析框架示意图

本文工作基于UPPAAL 介绍利用模型检测技术检测重入漏洞的方法。以下几节分别介绍如何构建DAO 合约的形式模型、余额一致性的逻辑公式表示以及如何从UPPAAL 所返回的结果中分析重入攻击行为。

3 重入漏洞的形式模型

本文用UPPAAL 的形式模型——时间自动机来描述合约语义。由于本例未涉及时间相关特性，因此以下简称自动机。用UPPAAL 的性质描述语言——分支时序逻辑(CTL)来表示余额一致性性质。

自动机由节点和边组成，每条边包含三类属性：条件(Guard)、状态更新操作(Update)和同步操作(Sync)。仅当边上条件被满足并且所需接收的信号到达时，边所表示的由一个节点到另一个节点的转换才可能发生。合约内或合约之间的函数调用行为可看作是多个自动机的并发。更详细的语义细节将结合DAO 合约的形式模型来介绍。

为考察DAO.withdrawAll()的行为，需构建三个自动机：

(1)自动机DAO_w。模拟DAO.withdrawAll()的执行过程，如图4(a)所示。DAO_w 初始处于idle 状态，当收到调用信号（callW[Cid]?）时启动，如果DAO.withdrawAll()中第二行的条件不满足，则经由边e2转到结束状态，再发出执行结束信号（endW[Cid]! ）完成函数的一次执行;否则经由e3 执行相应操作，并在e4 发出调用Client.pay()的信号(callP[Cid]！ )，然后等待其执行结束并返回(endP[Cid]?)，收到返回信号后，将变量credit[0]赋值为0。接着结束并发出执行结束信号(endW[Cid]?)，完成DAO.withdrawAll()的一次执行。

(2)自动机Client_p。模拟Client.pay()的行为，如图4(b)所示。由于自动机可以表示不确定转换，无论图2 所示的参与对象GoodClient 还是Attacker 中的pay()的行为，都可在同一自动机中描述。Client_p初始处于idle 状态，接收到调用信号(callP[Cid]？)时启动。接着，如果pay()中没有回调行为(如Good-Client.pay())，执行转换e2，然后发送执行结束信号(endP[Cid]! )；如果包含回调行为(如Attacker.pay())，执行转换e3，并发送对DAO.withdrawAll()的调用信号(callW[Cid+1]！ )(此时，上一次，即第Cid 次的调用还未结束，故为第Cid+1 次)。等待这次调用结束(接收到执行结束信号endW[Cid+1]?)后，发送自身进程结束信号(endP[Cid]! )。

(3)自动机initCaller。模拟对DAO.withdrawAll()进行初始调用动作，如图4(c)所示。initCaller 通过发送对DAO.withdrawAll()的调用信号(callW[0]! )启动一次交易；当它接收到对应的DAO.withdrawAll()执行结束信号(endW[0]?)时，结束整个执行，即结束一次交易。为方便随后的性质验证与分析，这里还用到一个布尔变量closed，初始值设为false，在交易结束时设为true(边e2)。

图4 合约DAO 及其调用模型

本例中设callNum=2，表明各函数至多被嵌套调用两次。标号Cid 从0 开始，表示对对应函数的第Cid+1 次嵌套调用。DAO.withdrawAll()最初只能由外部触发，故它的第一次调用为自动机initCaller发送调用信号callW[0]发起。

不失一般性地，假设有两个对象参与合约调用，他们已各自存入100 以太币，当前他们在合约DAO 中的账户余额都是100；合约的余额是200，即balance=200。假设由0 号参与对象启动DAO.withdrawAll()操作，对credit[0]和balance 的值进行修改。

在这个模型上，很直观地，上述关于“保证balance 的值为所有对象的余额总和”这一不变式可用CTL 公式描述为：

其中q=(balance==sum(i:int[0,oNum-1]) credit[i])，是一命题逻辑公式。

直观地说，模型所表示的程序的所有可能执行路径形成一棵树。CTL 公式A＜＞q 表示这棵树的每一条路径上，都存在至少一个节点满足命题逻辑公式q。公式(1)即是余额一致性的时序逻辑公式描述。其含义是：无论参与对象的行为如何，q在每个状态下满足。至此，完成了图1 所示的DAO 合约以及性质“余额一致性”的建模。

4 重入漏洞的形式分析

如果DAO 合约在两次嵌套调用(一次回调)时不满足余额一致性性质，那么就可以判断其存在重入漏洞[16]。因此，将模型中Cid 的取值范围设为{0，1}，即DAO.withdrawAll()只被回调一次。

在UPPAAL 中，在模型上验证某一性质，将得到“满足该性质”或“不满足该性质”的结果。对于不满足的性质，工具还可生成反例。

可从验证结果得到这样一些信息：

如果性质满足，只要参与对象模型涵盖了所有可能的使用行为，可以得出该合约不存在可重入漏洞的结论。

反之，如果模型不满足该性质，说明至少存在一条路径，其上有状态不满足余额一致性。这样就存在攻击路径，攻击者可利用它来实现重入攻击。UPPAAL 可以返回一条攻击路径来帮助开发者查错。为了得到一条完整的路径，本文用公式(2)来验证。

图5 参与对象回调DAO 时的消息序列图及状态变化

公式(2)表示，在所有执行路径上，当整个执行结束时，q 满足。当整个执行回到initCaller 的e2 边时，closed 被置为真。显然，若公式(2)不成立，公式(1)也不成立。

在UPPAAL 中，在上述DAO 模型及其调用模型上验证公式(2)，将被告知“不满足该性质”，并生成反例。反例的消息序列图及状态变化如图5 所示(没有变化的状态省略)。这个序列图很好地展示了当参与对象包含回调时模型的行为。通过状态变化，可以看到余额一致性性质是如何被破坏的。图中的5 条线程分别对应交易发起者(initCaller)，对DAO.withdrawAll()的两次嵌套调用(DAO_w(0)和DAO_w(1))，对pay()的两次嵌套调用(Client_p(0)和Client_p(1))；最右列是几个变量值的变化情况，无变化的情况省略。可以看到，在初始状态S0，余额是一致的；在状态S1，合约的余额已被扣减，但用户余额不变(credit[0]=100)；由于该用户尚有余额(credit[0]＞0)，在pay()回调的DAO.withdrawAll()(第二次调用，对应于DAO_w(1))执行时，合约余额再次被扣减(S3)；直到对pay() 的第二调用(Client_p(1))执行返回后，credit[0]才被清零(状态S3)。这个状态一直保持到结束(S4)。可以直观地看出，在这执行过程中除了初始状态，其他状态都不满足q，因而验证模型不满足公式(2)从而不满足公式(1)。因此，可以断言，当参与对象的pay()有回调行为时，DAO 合约是可重入的，它的状态会被意外修改。

在这一模型中只允许设置两层嵌套(即回调一次DAO.withdrawAll())，在实际的DAO 攻击事件中，回调次数(即balance 被扣减，而credit[0]不变)取决于什么时候balance 被取完或攻击者的gas 耗尽。

合约DAO 的重入漏洞的隐密性在于，如果函数pay()中不回调DAO.withdrawAll()，在执行结束时，余额一致性是能够保持的。图6 所示的消息序列图对应的即是图2 中的goodClient 的行为。当closed 为真时q 为真(S7)，故而整个行为满足公式(2)。但公式(2)成立并不能推出公式(1)成立。

图6 参与对象无回调时的消息序列图及状态变化

重入漏洞看似由回调引起，但实际上回调并不是根本原因。例如，修改一下DAO 合约，将图1 中DAO.withdrawAll()的第5 行代码放至第2.5 行处，这时相应的模型也要修改：将图4(a) 所示自动机DAO_w 的边e5 上的更新操作credit[0]移至e3,紧接着对balance 的更新，形成新的模型DAOfixed。这时，无论Client_p 走哪条路径，公式(1)都成立。图7展示的是修改后的模型在pay()中包含回调的情况下的执行序列。可以看到，DAO.withdrawAll()的第二次执行(DAOfixed(1)) 过程中并不再次调用pay()(Client_p(1))。实际上，在这个模型中，无论将嵌套调用次数(callNum)设为多大，pay()只为被执行一次，DAO.withdrawAll()只会被执行两次。例如，图8所示的是当callNum=4 的情况。