一个CM通信

研究突出了

MadMax:分析智能合约的废气世界

文/ Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent, Bernhard Scholz, Yannis Smaragdakis
ACM通讯，2020年10月，第63卷第10期，87-95页
10.1145 / 3416262
评论

以太坊是一个分布式区块链平台，作为智能合约的生态系统:成熟的相互通信程序，捕获帐户的交易逻辑。气体限制限制以太坊智能合约的执行:指令执行时消耗气体，只要气体可用，执行就继续进行。

针对天然气的漏洞允许攻击者迫使关键合同功能耗尽天然气，有效地对合同实施永久性的拒绝服务攻击。对于程序员来说，这类漏洞是最难防范的，因为在非攻击场景中，out- gas行为可能并不常见，而且对这些漏洞的推理也不容忽视。

在本文中，我们识别了气体聚焦的漏洞，并提出了MadMax:一种静态程序分析技术，可以以非常高的置信度自动检测气体聚焦的漏洞。MadMax在Datalog中结合了智能合约反编译器和语义查询。我们的方法捕获了高级的程序建模概念(例如“动态数据结构存储”和“安全的可恢复循环”)，并提供了高精度和可伸缩性。MadMax在短短10小时内分析了以太坊区块链智能合约的整体，并标记了价值数十亿美元的合约中的漏洞。手工检查标记过的合同样本表明，81%的样本警告确实会导致漏洞。

回到顶部

1.简介

以太坊是一个去中心化的区块链平台，可以执行任意表达的计算聪明的合同。智能合约几乎可以捕获任何复杂的交互，比如响应来自其他账户的通信，分配或接受资金。这种可编程逻辑的可能性是无限的。它可以编码收益计划、投资假设、利率政策、有条件的交易指令、交易或支付协议以及复杂的定价。实际上，任何事务性多方交互都是可表达的，不需要中介或第三方信任。

智能合约通常处理中的事务醚，它是以太坊的原生加密货币区块链，目前市值达数百亿美元。智能合约(与非计算性的“钱包”相反)在流通的以太币总量中占有相当大的比例，这使它们成为攻击者的成熟目标。因此，开发人员和审计人员有强烈的动机广泛地使用各种工具和编程技术，以最大限度地减少他们的合同被攻击的风险。

因此，智能合约的分析和验证是高价值的任务，可能比任何其他应用领域都要高。货币价值和公共可用性的结合使得及早发现漏洞成为一项至关重要的任务。

一个广泛的合同漏洞家族的关注次陷入无油可用的的行为。气体是以太坊中计算的燃料。由于大量复制的执行平台，通过向用户收取运行合同的费用，避免了浪费他人的资源。每条执行指令都需要消耗汽油，这些汽油可以通过以太币进行交易。由于用户预先支付了gas，交易的计算可能会超过其分配的gas量。在这种情况下，以太坊虚拟机(EVM)，它是编译智能合约的运行时环境，会引发一个耗尽气体的异常并中止事务。如果合同没有预料到(或没有正确处理)由于耗气条件可能导致交易流产，那么合同就会面临以天然气为核心的漏洞的风险。一个易受攻击的智能合约可能会因为不正确的耗气状态处理而永远被阻塞:重新执行合约的功能将无法取得进展，并无限期地产生耗气异常。因此，尽管攻击者不能直接挪用资金，但他们可以对合同造成损害，将其余额锁定，这实际上是一种拒绝服务攻击。这种攻击可能会以间接的方式使攻击者受益——例如，伤害竞争对手或生态系统，在黑帽社区中积累名声，或进行敲诈。

在这部作品中，我们展示了MadMax:¹用于检测智能合约中气体集中漏洞的静态程序分析框架。MadMax是一个静态分析管道，由一个反编译器(从低级EVM字节码到结构化中间语言)和一个基于逻辑的分析规范组成。MadMax是高效和有效的:它在短短10小时内分析了整个以太坊区块链，报告了大量的易受攻击的合同，总价值超过28亿美元，具有高精度，从随机样本中确定。

MadMax在智能合约分析和验证领域是独一无二的。这是一种采用尖端技术的方法声明静态分析技术(例如，上下文敏感的流分析和数据结构的内存布局建模)，而过去的分析器主要集中在轻量级静态分析，符号执行，或功能正确性的全面验证。正如MadMax所演示的，静态程序分析提供了独特的优势组合:非常高的可伸缩性(适用于整个区块链)和潜在漏洞的高覆盖率。此外，MadMax还通过编码复杂的属性(如“安全可恢复的循环”或“由公共调用引起的增加的存储”)来提高自动化安全分析的抽象级别，从而允许检测跨多个事务的漏洞。

回到顶部

2.背景

区块链是使用密码学保护的共享、透明的分布式事务分类帐。可以将区块链看作是一个长且不断增长的块列表，每个块编码一个单独的事务序列，总是可用于检查并且不会被篡改。每个块包含前一个块的密码签名。因此，在不拒绝它的所有后继块的情况下，前一个块不能被更改或拒绝。对等点/矿工运行一个挖掘客户端来单独维护区块链的当前版本。每个对等体都考虑从a开始的最长有效链《创世纪》块为区块链的可接受版本。为了鼓励所有对等点进行交易验证并阻止浪费或误导的工作，区块链协议通常结合了两个因素:作为对成功执行验证的对等点的奖励的激励，以及需要昂贵的计算来生成块的工作证明。要了解分布式共识和永久记录保存是如何产生的，请考虑一个恶意客户，他试图重复花费一定的金额。客户可能传播相互冲突的交易(例如，支付卖方)一个而且B)传送到网络的不同部分。当不同的对等体意识到两个版本的真相时，大多数会产生，因为对等体会在他们认为是当前版本的基础上构建更多的块。因此，大多数人很快就会接受两种开支交易中的一种作为权威，而拒绝另一种。少数派必须效仿，否则其进一步参与增长区块链的行为也将被宣告无效:其他对等体将忽略任何没有形成最长链的区块。

使用这种方法，区块链可以用于协调所有具有信任的多方交互，而不是在默认情况下授予某个权威。

最初的区块链，至少以其流行的形式，是由于比特币平台。¹¹比特币显然是一个特殊用途的加密货币平台。因此，在比特币账本上注册的数据可以被视为交易方和金额(有少量的逻辑允许加密身份验证)。相比之下，我们感兴趣的区块链公式是由以太坊平台推广的^4，21:注册账户可以包含智能合约，即可以执行任意计算的成熟程序，可以对复杂逻辑进行编码。

以太坊智能合约编程通常使用Solidity语言完成。¹⁸solid是一种类似javascript的语言，通过静态类型、契约作为类封装结构、契约继承和许多其他特性进行了增强。

从直接运行在以太坊区块链上的代码中删除了Solidity(或其他高级语言)抽象级别。相反，以太坊本机支持底层字节码语言——以太坊平台本质上是一个分布式的复制虚拟机，称为Ethereum VM(维生素)。EVM是一种底层堆栈机，其指令集包括标准算术指令、基本密码学原语(主要是密码学散列)、用于标识契约和调用不同契约(基于密码学签名)的原语、与异常相关的指令以及用于气体计算的原语。数据存储在区块链(称为存储)，以持久数据结构的形式，或以契约局部瞬态的形式内存。

在我们的工作中，我们专注于在字节码级别分析智能合约。这是一个高成本的设计决策(由于字节码的低级特性)。同时，EVM字节码级别的抽象产生了一个高回报用于针对它的分析。字节码级别的分析不需要契约的源代码，允许分析新的和部署的契约，这些契约最初是用任何语言编写的。在字节码级别，输入代码是规范化的，所有控制流都是显式的、统一的和简化的。此外，高级语言和EVM字节码之间的阻抗不匹配常常是混乱和错误的来源。例如，考虑下面的代码模式:

这段代码遍历数组的所有位置，将它们设为零。这种迭代很可能会耗尽能量。(这样的代码背后是一个漏洞¹在政府¹⁶比如智能合约。)这种迭代在稳固级别上是隐式的，但在字节码级别上立即显现出来。

回到顶部

3.气体聚焦漏洞

接下来，我们将确定一些最常见的以气体为焦点的漏洞模式。尽管我们的整个分析工作都在EVM字节码级别，但我们还是出于演示目的而使用了Solidity。

以太坊执行模型通过让用户预先支付执行交易所需的gas来激励用户最小化执行指令的数量。耗尽天然气是常见的，但在大多数情况下，这不是灾难性的:事务被恢复，最终用户以更高的天然气预算重新运行它。

然而，以太坊智能合约可以相对容易地达到这样一种状态，即永远不会有足够的气体来运行它们的代码。最常见的原因是以太坊网络的块气体限制——目前是9M单位的气体，这足以对存储(即区块链)进行几百次写入。

3.1.无限质量操作

以气体为中心的脆弱性的最标准形式是无界质量操作。如果循环的行为是由用户输入决定的，那么循环的迭代次数可能会太多，超过块气体的限制，或者变得过于经济昂贵而无法执行。法典可能没有预料到这种可能性，因此无法确保合同能够在这些条件下继续按预期运作。这通常会导致拒绝所有必须尝试迭代循环的事务的服务。考虑合同:

随着帐户数量的增加，需要执行gasapplyInterest将会上升。非常快(仅仅添加了几百个条目之后)账户)，该函数将不可能在不引发out- gas异常的情况下执行:循环指令的成本超过以太坊区块气体限制。

以太坊编程安全建议¹⁷建议程序应该避免为无限数量的客户端执行操作(而只是使客户端能够从契约中“拉”)。然而，契约很容易违反这一实践，没有意识到循环的迭代只受用户控制的数量的限制。

另一种建议是，当循环确实需要为无限数量的客户端执行操作时，应该在每次迭代中检查气体的数量，合约应该“跟踪(它)走了多远，并能够从那个点恢复”。¹⁷这种模式复杂、容易出错，而且(正如我们所确定的)在实践中非常罕见。

3.2.非孤立的呼叫(损害钱包)

另一种使合同陷入耗尽天然气问题的方法是调用本身可能会抛出耗尽天然气异常的外部功能。问题的第一个元素是程序员可能没有广泛考虑的调用。这种调用通常是隐式的，作为以太传输的一部分。发送Ether需要调用接收方的回退函数。

基于solididity原语和推荐的实践可以很好地说明问题。在solid中，发送以太坊是通过发送或者是转移原始的。它们有不同的方法来处理传输错误。例如，如果发送以太失败，send返回false:

另一方面，转移如果发送Ether失败，将引发错误(即抛出异常)。

重要的是,发送和转移可靠性原语在设计时考虑到了故障。两者都在EVM字节码级别转换为常规调用，但被调用方的天然气预算有限，只有2300。这还不足以允许在接收者端执行一些日志代码。因此，重点放在错误处理上。

本地的一个好实践(也用于推荐的以太坊安全代码模式中¹⁷)正在使用发送原语，总是检查结果，如果发送失败，通过抛出异常终止事务。这有效地将发送成一个转移加上用户想要的任何其他代码。

当该异常在循环中抛出时，问题就出现了，循环也在处理其他外部帐户。合同程序员或审计人员很容易忽略潜在的威胁。例如，循环可能只迭代有限的次数(例如，竞赛可能会奖励分数板上的三个领先者)，从而使程序员误以为它的汽油消耗量是固定的。此外，认为外部一方会故意中止给它钱的交易是违反直觉的。最后，急切中止事务的通常保守的naïve错误处理共同导致了这个问题。

我们可以在一个漏洞的示例代码中看到这个问题^20.吸引人地称为钱包逆反心理。²考虑一个简单的循环，试图奖励竞赛的三个获胜者:

问题是发送命令还将导致执行获胜者的回调函数。对于攻击者来说，让合约变得脆弱所需要做的就是让自己成为赢家，然后提供一个耗尽能量的回调函数。发送方合同可能永远无法从这种情况中恢复—例如，代码清除胜利者可能只出现在上述循环结束后。

3.3.整数溢出

编程错误通常表示为以气体为中心的漏洞，这是由于可能的整数溢出造成的，通常(但不完全)是由于solidity类型推断方法引起的。这是一个与3.1节的一般攻击不同的模式，因为迭代不仅是无界的，而且是不终止的。

考虑以下合同:

的使用var引出一个类型推理问题。(更新版本的solididity静态检测此问题。)变量的推断类型我是uint8(例如，一个字节)，因为变量初始化为0和uint8上的所有操作兼容的最精确类型是否为0我．不幸的是，这意味着仅仅增加了256个成员收款人足以造成回路不终止，迅速导致气体衰竭。攻击者可以通过添加fake来利用这个漏洞收款人使用适当的公共函数(未显示)，直到溢出被触发。

回到顶部

4.反编译维生素与字节码

我们以气体为重点的漏洞分析的第一步是反编译步骤，将EVM字节码的抽象级别提高到一种结构化中间语言(IR):控制流图(CFGs)，而不是三地址代码。反编译步骤是本身静态分析，如EVM字节码是低级的:更接近于特定于机器的程序集，而不是结构化的IRs(如Java字节码或。净IL)。

4.1.EVM字节码分析的挑战

EVM是一个基于堆栈的底层IR，具有最小的结构化语言特征。在字节码形式的智能合约中，符号信息被数字常量所取代，函数被融合在一起，控制流难以重构。为了说明这一点，将EVM字节码语言与最著名的字节码语言:Java (JVM)字节码——一种高级得多的IR进行比较。设计上的差异包括:

• 与JVM字节码不同，EVM没有结构、类或对象，也没有方法的概念。
• Java字节码是类型化的字节码，而EVM字节码不是。
• 在JVM字节码中，堆栈深度在不同的控制流路径下是固定的:执行不能到达具有不同堆栈大小的相同程序点。在EVM字节码中，不存在这样的保证。
• EVM字节码中的所有控制流边(即跳转)都是变量，而不是常量。跳转的目标是从堆栈中读取的值。因此，即使要确定基本块的连通性，也需要进行价值流分析。相比之下，JVM字节码有一组明确定义的每次跳转的目标，与值流无关(即与堆栈内容无关)。
• JVM字节码定义了方法调用和返回指令。在EVM字节码中，尽管对智能合约外部的调用是可识别的，但合约内部的函数调用只会被转换为跳转(到可变目的地，如上所述)。契约的所有功能融合在一起，以低级跳跃作为转移控制的手段。

要调用一个契约内函数，代码将返回地址压入堆栈，压入参数，压入目标块的标识符(一个散列)，并执行跳转(弹出堆栈顶部元素，将其用作跳转目标)。要返回，代码将调用方基本块的标识符从堆栈中弹出并跳转到它。

4.2.反编译方法

MadMax最初基于Vandal反编译器。^3.，19随后，相同的分析逻辑被移植到我们的Gigahorse反编译器框架中。⁶

我们的反编译步骤接受EVM字节码作为输入，并以标准的结构化中间表示产生输出:一个控制流图(由基本块和连接它们的边组成);三地址代码用于所有操作(而不是操作堆栈);和公认的(可能的)函数边界。这种表示被编码为关系(例如，表)，并递归地查询，以形成更高层次的程序分析。

我们观察到EVM字节码输入很像延续传递风格(CPS)形式的函数语言:所有调用和返回都是前向调用(跳转)，其中调用添加延续(返回指令)作为参数之一。CPS和低水平跳跃的等价性之前已经被观察到——最明显的是Thielecke。¹⁵

有CPS输入，需要检测值和控制流的技术设置正是控制流分析(CFA)。^12，13控制流分析也是一个原始的建议上下文相关的（调用敏感)价值流静态分析:为k-CFA分析，每个呼叫目标分别针对每个呼叫方(即呼叫指令)、呼叫方的呼叫方等进行分析，达到最大深度，k。

因此，反编译采用控制流分析的标准形式，¹³抽象解释的:抽象解释的上下文敏感性适应输入契约的复杂性，经常导致深入上下文的分析(例如，k= 12)。最终结果是一个使用中列出的模式的三地址代码图1．语法糖和次要细节省略用于表示目的。语言语法用[和]括起来，元变量隐式地不加引号。例如,年代:【来: = BINOP (x，y)表示该语句年代是否存在二进制运算x而且y其结果是来,在那里x，y,来是引用字节码变量的元变量。分析程序中的变量和分析中的元变量之间的区别从上下文来看是明确的;因此，从今以后，我们简单地称之为“变量”。我们省略语句标识符，年代，当它不影响规则时。我们还使用*作为通配符，也就是说，它表示任何变量，它会被忽略。

图1。域和反编译器输出(即，用于主要分析的输入关系)。

该模式使用标准的结构化中间语言，以一种稍微抽象的方式捕获EVM字节码的所有元素。例如，JUMPI指令有语句，而不是任意值作为目标。所有二进制操作都被同等对待，因为我们目前不试图分析算术表达式。中不包括一元运算或变量之间的直接赋值图1，尽管我们在实现中这样做，因为这些可以被视为二进制操作的特殊情况。RTVALUE对返回gas成本、事务id、代码大小、调用者和其他运行时数量的指令进行统一处理。

回到顶部

5.核心MadMax分析

主要的MadMax分析使用基于逻辑的规范对反编译的输出进行操作。分析是用数据日志语言实现的:一种基于逻辑的语言，相当于递归的一阶逻辑。⁸分析由几个层组成，这些层逐步推断出有关所分析的智能合约的更高层次的概念。从的三地址码表示开始图1，循环、归纳变量和数据流等概念首先被识别。然后，对内存和动态数据结构进行分析，推断出动态数据结构、重入时存储增加的契约、嵌套数组等概念。最后，推断出气体集中漏洞的分析级别的概念(例如，带有无界大容量存储的循环)。

5.1.流程和回路分析

以太坊气体集中的漏洞往往需要对基础契约的高级语义理解。在表达更深层的语义之前，需要进行各种初始的低级分析。因此，MadMax分析的第一步是循环和数据流信息的推导。这就产生了几个关系，进一步的分析步骤就建立在这些关系上。文中给出了关系以及一些额外的域和输入上下文定义图2．我们没有为任何这些关系提供Datalog规则—它们的实现虽然并不总是直接的，但是标准的。例如，它类似于标准数据记录分析公式中的流计算¹⁴或Java字节码框架，如JChord^9，10和Doop。²

图2。用于基线循环和数据流分析的额外域、输入和输出模式。

中的前三个计算关系图2(INLOOP, INDUCTIONVAR和LOOPEXITCOND)在结构化循环中编码有用的概念。注意，低级程序中的循环不必是结构化的;例如，可能不存在支配所有循环语句的循环头。然而，Solidity和其他EVM语言经常在编译过程中生成结构化循环。循环分析查找归纳变量，即在每次迭代中按可预测的(但不一定是静态已知的)量递增的变量。

接下来的四个关系捕获数据流分析。关系流表示变量之间的数据流依赖关系。在其最简单的形式中，FLOWS只是BINOP输入关系的自反传递闭包;也就是说，它忽略存储和内存加载和存储指令。然而，可以在不影响其他分析的情况下给出更复杂的flow定义。VARALIAS是类似的关系，但限制更严格，变量之间直接赋值，不需要进一步的运算。相应地，HASCONSTANTVALUE做了一个简单的常量传播:它只是VARALIAS与输入CONST关系的组合。

最后，MEMCONTENTS给出VARALIAS的结果，对MSTORE操作进行简单的分析，并将结果传播到控制流图中从MSTORE可到达的每个语句。

以上关系有两点值得一提:

• 数据流分析(即HASCONSTANTVALUE、FLOWS、VARALIAS和MEMCONTENTS关系)是最好的，也就是说，既不健全也不完整。这意味着，首先，不能保证找到所有可能的流、别名等:由于复杂的算术、运行时操作、内存负载和存储等，两个变量可能具有相同的值，而不需要分析计算。其次，并非所有推论都能保证成立。例如，已知在一个控制流路径中存在但在另一个控制流路径中不存在的推断将在路径合并时乐观地传播。
  既不健全也不完整的特性延续到我们的整体分析结果中。MadMax既不能保证检测到所有气体漏洞，也不能保证报告的每个气体漏洞都是真正的bug。这种设计选择很好地符合bug检测静态分析的预期目的——分析的价值不是基于它的保证，而是基于它在现实世界中的实用性。⁵
• 关系流和VARALIAS在MadMax分析中无处不在。今后我们将看到的大多数其他关系对于流动或(较弱的)VARALIAS都是传递性闭合的。我们在本文中省略了这种传递闭包Datalog规则，只关注每个有趣概念的种子逻辑。

有了上面的基本循环和数据流分析，我们就可以建立更高级的概念，比如循环的界限。这被定义为LOOPBOUNDBY图3．若均为归纳变量我一个非归纳变量c流到循环退出条件，然后我们推断循环可能被的内容绑定c。这种关系的进一步细化是dynamallybound，它推断哪些循环是通过存储或只有在运行时才知道的其他值绑定的。

图3。推断有界循环和可恢复循环。

最后，我们定义了谓词possibyresumableloop，以匹配似乎实现了以太坊安全编码建议的循环，¹⁷通过检查剩余气体量，节省(永久)存储一个感应变量，并从存储加载相同的感应变量。请注意，这并不是对可恢复循环的完全精确检测—它很可能只是找到刚好匹配这些抽象条件的代码实例，例如，气体检查、存储和感应变量的加载。

然而，这三个条件的存在强烈表明，程序员已经考虑了out- gas异常的可能性，并采取了预防措施，使循环在重新执行契约函数时可以恢复。

5.2.内存布局分析

为动态数据结构忠实地建模以太坊虚拟机内存布局是MadMax的关键部分。这种建模对于降低分析的假阳性率是必要的。寻找气体漏洞的一种直观但naïve的方法可能是标记任何包含“动态绑定”循环的契约，或者迭代次数取决于存储在存储器中或作为外部输入传递的某个值的循环。然而，精确的分析需要更多的复杂性。我们通过实验发现，目前部署的智能合约中，大约有一半都有动态绑定回路，但指望目前部署的智能合约中有一半是脆弱的，这是完全不现实的。相反，对于迭代未绑定数据(即数据结构)的循环，我们需要确定数据结构是否可能被攻击者填充。

以太坊虚拟机没有高级数据结构的概念。相反，对高级数据结构的操作被编译为对可寻址存储的低级操作。solid提供了两种主要的动态大小的数据结构:动态大小的数组和关联数组，即映射。虽然数组和映射都可以动态调整大小，但是没有迭代映射的机制。因此，数组是建模的主要数据结构，以便捕获无边界迭代的循环。

从传统编程语言的角度来看，以太坊的内存布局是非常不寻常的，但如果考虑到执行环境的细节(例如，每个契约使用隔离的256位内存空间，加密哈希作为原语)，则完全合理。主要思想是关键是一个数组。键是保存数组大小的内存位置的地址。与此同时，关键是散列生成保存数组内容的内存位置的地址。

图4描述一个包含两个标量变量和一个二维动态数组的简单契约的存储分配示例。在solid中，固定大小的数据结构按程序顺序从偏移量0开始连续存储在存储器中。数组中的各个元素也被连续地存储在存储器中;但是，元素的起始偏移量需要进行一些计算才能确定。由于其大小不可预测，动态大小的数组类型使用KECCAK256哈希函数(SHA3)来查找数组数据的起始位置。动态数组值本身在存储的某个位置占用了一个空槽p。对于动态数组，此槽存储数组中元素的数量。然而，数组数据位于KECCAK256(p)。通过递归映射上述实现，将数组的实现扩展到任意嵌套的动态数据结构，需要进行递归分析。

图4。数据结构分析输出。

MadMax执行分析(省略)，为智能合约中的内存布局建模和识别动态数据结构。这个分析的输出显示在图5．基于这些关系，我们定义了气体聚焦分析的关键概念，如图6．一个重要的概念是增加存储公共功能。增加并存储在相应存储槽中的存储变量意味着当调用某个公共函数时契约的数组大小会增加。此外，我们还可以找到遍历数组的循环。我们将ARRAYITERATOR定义为一个遍历数组的循环。

图5。给定合同的存储结构和内容(下)(上)。Sha3是keccak256哈希函数。

图6。用于标识存储需求的数据日志规则在公共功能中增加。

5.3.顶级漏洞查询

前面几节的分析概念设置了针对气体集中的漏洞的最终查询。这是通过结合几个不同的概念来实现的。图7以略微简化(并内联为单一规则)的形式显示了MadMax分析的最终输出关系。

图7。对无界大规模操作、钱包损坏和溢出漏洞的顶级查询。

例如，考虑UNBOUNDEDMASSOP逻辑:它检查可以作为公共函数的结果而增长的数组是否具有加载或存储的内容(flow (storeOffsetVar、索引)允许从内容的开始解引用)，在循环中，其边界基于数组大小，并包含一个影响加载或存储的地址的归纳变量。

WALLETGRIEFING查询更精确，需要从动态数组加载加载的值流到调用，调用的结果是throw语句的条件。调用和抛出需要在同一个循环中，循环中还有一个影响加载的地址的归纳变量。

最后，如果将归纳变量强制转换为短整数(理想情况下为一个字节)，则保守地断言有可能发生循环溢出。循环必须被“动态绑定”以变得脆弱，也就是说，迭代次数是由某个运行时值决定的。

回到顶部

6.影响

我们最初的MadMax实验考虑了2018年4月9日以太坊区块链上所有可用的智能合约。我们在一台空闲机器上运行MadMax，该机器配备Intel Xeon E5-2687Wv4 3.00GHz和512GB RAM。由于时间限制，我们为反编译设置了20秒的截止时间—超过该时间，契约将被视为超时。

被标记为漏洞的合同总共包含707万ETH，或约28亿美元。^3.在我们进行区块链抓取时，总共部署了633万个合同实例，它们由91.8k独特程序生成。有4.1%的合约被MadMax标记为容易受到无限迭代的影响，0.12%被钱包损坏，1.2%被标记为循环诱导变量溢出。

为了估计假阳性率，我们手动检查了标记的合同的子集。我们的无偏抽样过程包括使用唯一的字节码程序，并按块哈希顺序选择第一个和最后几个契约。然而，由于需要在网上获得源代码，这就引入了一个偏见因素——没有源代码的合同没有被考虑在内，因为手工检查低级字节码是非常耗时和不可靠的。

我们选择了前13个合同，手工检查显示，这些合同中的11个确实显示了13个明显的漏洞，标记了16个，精度为13/16 = 81%。确切的数字并不重要——更大的样本可能会让它上升或下降几个百分点。重要的是，分析要足够精确，以产生大量真正的漏洞警告。通过手动检查样本合同，我们获得了MadMax会议出版物中详细介绍的MadMax有效性的重要见解。⁷

MadMax对91.8k合约的整个分析只花了不到10个小时，运行了45个并发进程。Gigahorse反编译器的后续进展将这个数字降低了至少2倍。目前，根据具体设置，在反编译过程中，约有4%的合约会出现超时。

请注意，合同中被确认的漏洞并不意味着:(1)利用漏洞是容易的或廉价的，或者(2)漏洞阻塞了合同中的所有Ether。例如，利用一个无界大规模操作漏洞所需的气体可能代价高昂，从而阻止攻击者。但是，这并不影响合同对有动机的恶意行为者的脆弱性。

回到顶部

7.结束讨论

我们提出了MadMax，这是一个用于发现以太坊智能合约中以气体为中心的漏洞的工具。我们发现了以太坊智能合约的新漏洞，并演示了EVM字节码级静态分析工具的第一个成功设计，该工具煞费心机地反编译和重建程序的高级语义。MadMax方法利用了最好的技术和技术:从用于反编译的基于抽象解释的低级分析到用于高级分析的声明性程序分析技术。我们的方法使用区块链上部署的所有智能合约进行了验证，并展示了可伸缩性和具体有效性。从财务角度来看，我们的工具对其中一些智能合约构成了巨大的威胁，尤其是考虑到人工检查样本中警告的高精确度。

在可预见的未来，针对气体的漏洞可能会变得更加重要。气体(或类似的量)是区块链计算的基础，例如，包括在即将到来的Facebook天秤座的设计中。与传统编程领域相比，gas约束下的计算需要不同的编码风格——数据结构上的简单线性循环可能会使契约变得脆弱!今年,Ethereum伊斯坦布尔更新使SLOAD比制造贵四倍，而制造SSTORE更便宜。利用无界操作漏洞涉及许多状态更改操作，从而导致受害者执行更多的状态读取操作。因此攻击者的开销与存储开销与读取开销的比率有关。因此，利用该漏洞的成本将变得更低。此外，Libra的虚拟机将具有状态读取操作，例如ImmBorrowField而且ReadRef．这些操作将与状态写入操作一样昂贵MutBorrowField而且WriteRef，这将使得在Libra中利用无界操作的漏洞比在以太坊中更便宜。

MadMax是第一个发布的用于检测需要跨多个事务协调的威胁的分析。这代表了自动化安全分析的未来趋势:分析将需要考虑独立事务的状态变化，远远早于最终攻击的发生。此外，未来的威胁很可能涉及多合约或整个应用程序的攻击——例如，分散应用程序的区块链外部分与其区块链上(智能合约)部分之间的协调。这是安全分析工具的下一个挑战。在MadMax的情况下，通过假设高级属性(如“安全可恢复循环”)来启用多事务推理。反过来，这是由于分析的声明性，它允许对复杂属性进行简明的、逻辑的说明。同样的说明性方法可能在未来多契约、全应用推理分析的扩展中发挥重要作用。

回到顶部

致谢

这项研究得到了澳大利亚政府的部分支持，通过澳大利亚研究委员会的发现项目资助计划(项目ARC DP180104030)。我们感谢欧洲研究理事会的资助，307334和790340。此外，披露的研究工作部分由REACH HIGH Scholars Programme - post - phd Grants资助。该赠款由欧盟《2014-2020年凝聚力政策业务计划II》(投资人力资本以创造更多机会和促进社会福祉-欧洲社会基金)提供部分资金。

回到顶部

回到顶部

回到顶部

数字图书馆是由计算机协会出版的。版权所有©2020 ACM股份有限公司

---

没有发现记录