搜索
NFT元宇宙Web3
近期热门

MadMax:分析智能合约的gas世界

Founder

转载请微信联系:huangdiezi,更多DAO、Web3、NFT、Metaverse资讯请关注FastDaily

MadMax:分析智能合约的gas世界

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

以gas为重点的漏洞允许攻击者强迫合同的关键功能耗尽gas–有效地对合同进行永久性拒绝服务攻击。这类漏洞是程序员最难防范的漏洞之一,因为在非攻击情况下,缺气行为可能并不常见,而且对这些漏洞的推理也不简单。

在本文中,我们确定了以gas为重点的漏洞,并提出了MadMax:一种静态程序分析技术,能够以非常高的置信度自动检测以气体为重点的漏洞。MadMax结合了一个智能合约反编译器和Datalog的语义查询。我们的方法抓住了高层次的程序建模概念(如 “动态数据结构存储 “和 “安全可恢复循环”),并提供了高精确度和可扩展性。MadMax在短短10个小时内分析了以太坊区块链中的全部智能合约,并标记出货币价值为数十亿美元的合约中的漏洞。对被标记的合同样本的人工检查显示,81%的抽样警告确实导致了漏洞的出现。

1. 简介

以太坊是一个去中心化的区块链平台,可以执行任意表达的计算型智能合约。智能合约可以捕捉到几乎任何复杂的互动,如响应其他账户的通信,分配或接受资金。这种可编程逻辑的可能性是无限的。它可以编码报酬表、投资假设、利息政策、有条件的交易指令、交易或支付协议以及复杂的定价。几乎任何交易性的多方互动都是可以表达的,不需要中间人或第三方信任。

智能合约通常处理以太币的交易,以太币是以太坊区块链的原生加密货币,目前市值达数百亿美元。智能合约(相对于非计算型 “钱包”)持有流通中的全部以太币的相当一部分,这使得它们成为攻击者的成熟目标。因此,开发人员和审计人员有强烈的动机广泛使用各种工具和编程技术,以尽量减少他们的合同被攻击的风险。

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

一个广泛的合同漏洞系列涉及gas外的行为。gas是以太坊中计算的燃料。由于大规模的复制执行平台,通过向用户收取运行合约的费用来防止浪费他人的资源。每条执行的指令都要花费气体,而气体是用以太币来交易的。由于用户预先支付gas,交易的计算可能超过其分配的气体数量。在这种情况下,以太坊虚拟机(EVM),也就是编译智能合约的运行环境,会提出一个超出gas的异常,并中止该交易。如果一个合约没有预料到(或没有正确处理)可能因气体不足而导致交易中止的情况,那么该合约就有可能出现以gas为重点的漏洞。一个有漏洞的智能合约可能会由于不正确地处理气体外的条件而永远被封锁:重新执行合约的功能将无法取得进展,重新产生气体外的异常,无限期的。因此,虽然攻击者不能直接占用资金,但他们可以对合同造成损害,将其余额锁定,这实际上是一种拒绝服务的攻击。这种攻击可能以间接方式使攻击者受益–例如,损害竞争对手或生态系统,在黑帽社区积累名声,或进行敲诈。

在这项工作中,我们提出了MadMax:1一个静态程序分析框架,用于检测智能合约中以气体为重点的漏洞。MadMax是一个静态分析管道,由一个反编译器(从低级的EVM字节码到结构化的中间语言)和一个基于逻辑的分析规范组成。MadMax效率高、效果好:它在短短10个小时内分析了整个以太坊区块链,并报告了许多持有总价值超过28亿美元的脆弱合约,精度很高,这是从随机样本中确定的。

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

2. 背景

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

使用这种方法,区块链可以起到协调所有多方互动的作用,信任来自大多数对等人,而不是默认交给一个权威机构。

最初的区块链,至少以其流行的形式,是由于比特币平台。11比特币明确是一个特殊用途的加密货币平台。因此,在比特币账本上注册的数据可以被看作是交易方和金额(允许有加密认证的小逻辑)。相比之下,我们感兴趣的区块链表述是以太坊平台流行的表述4,21:注册的账户可以包含智能合约,也就是可以进行任意计算的成熟程序,实现复杂逻辑的编码。

以太坊智能合约编程最常用的是Solidity语言。18 Solidity是一种类似于JavaScript的语言,增强了静态类型、合约作为类的封装结构、合约继承和许多其他功能。

Solidity(或其他高级语言)的抽象水平与直接在以太坊区块链上运行的代码的抽象水平明显不同。相反,以太坊原生支持低级字节码语言–以太坊平台本质上是一个分布式、复制的虚拟机,称为以太坊虚拟机(EVM)。EVM是一个低级堆栈机器,其指令集包括标准算术指令、基本密码学原语(主要是密码学散列)、识别合约和调用不同合约的原语(基于密码学签名)、异常相关指令和气体计算原语等。数据要么存储在区块链上(一个称为存储的内存区域),以持久性数据结构的形式,要么存储在合约本地的暂存器中。

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

MadMax:分析智能合约的gas世界

这段代码的结果是在一个数组的所有位置上进行迭代,将它们设置为零。这种迭代很可能会耗尽能量。(例如,这样的代码是GovernanceMental16智能合约中的漏洞1背后的原因)。迭代在Solidity层面上是隐含的,但在字节码层面上是立即显现的。

  1. 以gas为重点的漏洞

我们接下来将确定一些最常见的以gas为重点的漏洞模式。尽管我们的整个分析工作是在EVM字节码层面上进行的,但我们还是采用了Solidity来说明问题。

以太坊的执行模式激励用户尽量减少指令的执行数量,让他们预先支付执行交易所需的气体。耗尽气体是很常见的,但在大多数情况下,这并不是灾难性的:交易被还原,最终用户用更高的气体预算重新运行它。

然而,以太坊智能合约可以相对容易地达到一个状态,即永远没有足够的气体来运行他们的代码。最常见的原因是以太坊网络的区块气体限制–目前是9M单位的气体,只够写几百次存储(即写到区块链上)。

* 3.1. 无约束的质量操作

以gas为中心的漏洞的最标准形式是无界质量操作。其行为由用户输入决定的循环可能会迭代太多次,超过区块gas限制,或变得太经济昂贵而无法执行。代码可能没有预测到这种可能性,因此未能确保合同在这些条件下能够继续按预期运行。这通常会导致所有必须尝试迭代循环的交易被拒绝服务。考虑一下这个合同。

MadMax:分析智能合约的gas世界

随着账户数量的增加,执行applyInterest的gas需求将上升。很快(在仅仅几百个条目被添加到账户后),该函数将不可能在不引发气体异常的情况下执行:循环指令的成本超过了以太坊块的gas限制。

以太坊编程安全建议17建议程序应避免为无限制数量的客户执行操作(而只是使客户能够从合同中 “拉 “出来)。然而,合约很容易违反这种做法,没有意识到一个循环的迭代只受用户控制的数量的限制。

另一个建议是,当循环确实需要为数量不受限制的客户进行操作时,应该在每次迭代时检查气体的数量,合同应该 “跟踪[它]走了多远,并能够从该点恢复”。17 这种模式很复杂,容易出错,而且(正如我们所确定的)在实践中非常少见。

* 3.2. 非隔离式调用(钱包悲鸣)

契约遇到气外问题的另一种方式是调用外部功能,而这些功能本身可能会抛出一个气外的异常。这个问题的第一个要素是程序员可能没有广泛考虑过的调用。这种调用通常是隐式的,是以太传输的一部分。发送以太涉及到在接收者那边调用一个回退函数。

根据Solidity的基元和推荐的做法,可以说明这个问题。在Solidity中,发送以太是通过发送或传输原语进行的。这些都有不同的方式来处理传输错误。例如,如果发送以太失败,send 会返回 false。

MadMax:分析智能合约的gas世界

另一方面,如果发送以太失败,transfer会引发一个错误(即抛出一个异常)。

重要的是,发送和传输Solidity原语的设计都考虑到了失败。两者都被翻译成EVM字节码级别的常规调用,但给被调用者的gas预算有限,为2300。这几乎不足以让接收者一方执行一些日志代码。。

当地的一个好的做法(也在推荐的Ethereum安全代码模式中使用17)是使用发送原语,总是对结果进行检查,如果发送失败,就抛出一个异常来中止交易。这有效地将发送变成了一个传输和用户想要的任何其他代码。

当异常被抛出在一个循环的中间时,问题就出现了,这个循环还在处理其他的外部账户。合同程序员或审计师可能很容易错过潜在的威胁。例如,循环可能只迭代了有限的次数(例如,一个比赛可能会把钱奖给记分牌上的三个领导者),欺骗程序员,让他以为它的gas消耗是固定的。此外,考虑到一个外部方会故意中止给它钱的交易,这也是反直觉的。最后,通常保守的天真错误处理,急于中止交易的做法,合谋造成了这个问题。

我们可以从一个被称为 “钱包悲痛 “的漏洞20的示例代码中看到这个问题。2 考虑一个简单的循环,试图奖励一个比赛的三个获胜者。

MadMax:分析智能合约的gas世界

问题是,发送命令也将导致赢家的回调函数被执行。契约的漏洞只需要攻击者让自己成为赢家,然后提供一个耗尽气力的回调函数就可以了。发送者合约可能永远无法从这种情况下恢复过来–例如,清除赢家的代码可能只在上述循环结束后出现。

* 3.3. 整数溢出

一个通常表现为以gas为重点的漏洞的编程错误是由可能的整数溢出导致的,通常(但不完全是)由于Solidity类型的推理方法而产生。这是与第3.1节的一般攻击不同的一种模式,因为迭代不仅仅是无界的,而且是字面上的非终止的。

考虑一下下面的合同。

MadMax:分析智能合约的gas世界

使用var会引起一个类型推断问题。(新版本的Solidity静态检测到这个问题。) 变量i的推断类型是uint8(即一个字节),因为该变量被初始化为0,而uint8是最精确的类型,可以保持0同时与i上的所有操作兼容。攻击者可以通过使用适当的公共函数(未显示)增加假的受款人来利用这个漏洞,直到溢出被触发。

4. 反编译EVM字节码

我们以gas为重点的漏洞分析的第一步是反编译,将EVM字节码的抽象水平提高到结构化的中间语言(IR):控制流图(CFG)在三地址代码上。反编译步骤本身就是一种静态分析,因为EVM字节码是低级别的:比起结构化的IR(例如Java字节码或.NET 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和低级跳转的这种等价性以前就被观察到了–最明确的是Tielecke。

控制流分析也是对价值流进行上下文敏感(call-site sensitive)静态分析的原始建议之一:对于k-CFA分析,每个调用目标都要对每个调用者(即调用指令)、调用者的调用者等进行单独分析,最大深度为k。

因此,反编译采用了控制流分析的标准形式,13被表述为抽象解释。上下文的敏感性适应了输入合同的复杂性,往往导致分析有很深的上下文(例如,k = 12)。最终结果是一个使用图1所列模式的三地址代码。为了表述的目的,采用了语法糖和小细节的删减。语言语法使用[ 和 ] 加引号,元变量隐含地不加引号。例如,s:[to:= BINOP(x, y)] 表示语句s是对x和y的一些二进制操作,其结果是to,其中x、y和to是指字节码变量的元变量。被分析程序中的变量和分析中的元变量之间的区别在上下文中是很清楚的;因此,我们在下文中只提到 “变量”。当语句标识符s不影响规则时,我们省略它。我们还使用*作为通配符,也就是说,它表示任何变量,这一点被忽略了。

MadMax:分析智能合约的gas世界

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

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

5. 核心MadMax分析

主要的MadMax分析使用基于逻辑的规范对反编译的输出进行操作。该分析在Datalog语言中实现:一种基于逻辑的语言,相当于带有递归的一阶逻辑。8该分析由几个层次组成,逐步推断出关于被分析智能合约的更高层次的概念。从图1的三个地址代码表示开始,循环、归纳变量和数据流等概念首先被识别。然后,对内存和动态数据结构进行分析,推断出诸如动态数据结构、重新进入时存储量增加的合约、嵌套数组等概念。最后,推断出以气体为重点的漏洞的分析水平的概念(例如,具有无限制的大量存储的循环)。

* 5.1. 流动和循环分析

以太坊以气体为重点的漏洞往往需要对底层合约有一个高层次的语义理解。在表达更深层次的语义之前,需要进行各种初步的低层次分析。因此,MadMax分析的第一步是推导出循环和数据流信息。这就产生了几个关系,在此基础上,进一步的分析步骤被建立。图2给出了这些关系,以及一些额外的领域和输入环境的定义。我们不提供这些关系的Datalog规则–它们的实现,尽管并不总是直接的,但是是标准的。例如,它类似于标准Datalog分析公式14或Java字节码的框架中的流程计算,如JChord9, 10和Doop.2。

MadMax:分析智能合约的gas世界

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

图2中的前三个计算关系(INLOOP、INDUCTIONVAR和LOOPEXITCOND)编码了结构化循环中的有用概念。请注意,低级别的程序中的循环不一定是结构化的;例如,可能没有一个主导所有循环语句的循环头。然而,Solidity和其他EVM语言经常产生结构化循环,作为其编译过程的一部分。循环分析发现诱导变量,即在每个迭代中以可预测的(但不一定是静态已知的)数量递增的变量。

接下来的四个关系捕捉了数据流分析。关系FLOWS表达了变量之间的数据流依赖关系。在其最简单的形式中,FLOWS只是BINOP输入关系的反相闭合;也就是说,它忽略了存储和内存加载和存储指令。然而,人们可以给出更复杂的FLOWS定义而不影响其余的分析。VARALIAS是一个类似的关系,但限制性更强,用于变量之间的直接分配,没有进一步的算术。因此,HASCONSTANTVALUE做了一个简单的常数传播:它只是VARALIAS与输入CONST关系的组合。

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

关于上述关系,有两点值得一提。

数据流分析(即关系HASCONSTANTVALUE、FLOWS、VARALIAS和MEMCONTENTS)是尽力而为的,也就是说,既不健全也不完整。这意味着,首先,不是所有可能的流量、别名等都能保证被找到:两个变量可能因为复杂的算术、运行时操作、内存加载和存储等而持有相同的值,而分析中却没有计算到这一点。第二,不是所有的推论都能保证成立。例如,一个已知在一个控制流路径中成立但在另一个路径中不成立的推论,在路径合并时将被乐观地传播。

这种既不健全也不完整的特性延续到了我们的整体分析结果。MadMax既不保证检测到所有的气体漏洞,也不保证报告的每个气体漏洞都是真正的漏洞。这种设计选择与检测漏洞的静态分析的预期目的非常一致–分析的价值不是基于它的保证,而是基于它在现实世界中的实用性。

关系FLOWS和VARALIAS在MadMax分析中是普遍存在的。此后我们将看到的大多数其他关系都是相对于FLOWS或(较弱的)VARALIAS而言的传递性封闭。我们在论述中略去了这种传递性封闭的Datalog规则,只关注每个有趣概念的种子逻辑。

有了上述基本的循环和数据流分析,我们可以建立更高层次的概念,比如循环的边界。这在图3中被定义为LOOPBOUNDBY。如果一个归纳变量i和一个非归纳变量c都流向一个循环的退出条件,那么我们推断该循环可能被c的内容所约束。这个关系的进一步细化是DYNAMICALLYBOUND,它推断哪些循环被存储或其他一些只有在运行时才知道的值所约束。

MadMax:分析智能合约的gas世界

图3. 推断约束循环和可恢复循环。

最后,我们定义了谓词POSSIBLYRESUMABLELOOP,以匹配那些似乎实现了以太坊安全编码建议17的循环,即检查剩余气体的数量,保存到(永久)存储的诱导变量,并从存储中加载相同的诱导变量。请注意,这并不是对可恢复循环的完全精确的检测–它很可能是在寻找刚好符合这些抽象条件的代码实例,例如,气体检查、存储和加载诱导变量。

然而,这三个条件的存在非常有力地表明,程序员已经考虑到了气体泄漏异常的可能性,并采取了预防措施,使循环在重新执行合约函数时可以恢复。

* 5.2. 内存布局的分析

对动态数据结构的Ethereum VM内存布局进行忠实建模是MadMax的一个关键部分。这种建模对于减少分析的假阳性率是必要的。找到气体漏洞的一个直观但幼稚的方法可能是标记任何包含 “动态绑定 “的循环的合同,或者循环的迭代次数取决于存储的某些值或作为外部输入传递。然而,精确的分析需要更多的复杂性。我们通过实验发现,目前部署的合同中约有一半有动态绑定的循环–但期望目前部署的智能合同中有一半是脆弱的,这完全是不现实的。相反,对于在无界数据(即数据结构)上迭代的循环,我们需要确定该数据结构是否可能被攻击者填充过。

以太坊虚拟机没有高层数据结构的概念。相反,对高层数据结构的操作被编译成对可寻址存储的低层操作。Solidity提供两种主要的动态大小的数据结构:动态大小的数组和关联数组,也就是地图。尽管数组和地图都可以动态调整大小,但没有机制可以对地图进行迭代。因此,数组是要建模的主要数据结构,以捕捉无边界迭代的循环。

从传统编程语言的角度来看,以太坊的内存布局是非常非传统的,尽管如果考虑到执行环境的具体情况(即,每个合约有一个隔离的256位内存空间,加密散列作为一个基元),这是完全合理的。主要的想法是,一个密钥代表一个数组。密钥是持有数组大小的内存位置的地址。同时,密钥经过散列处理后,可以得到保存数组内容的内存位置的地址。

图4描述了一个有两个标量变量和一个二维动态数组的简单合约的存储分配实例。Solidity中的固定大小的数据结构是连续存储的,因为这些结构在程序中出现,从偏移量0开始。 数组中的单个元素也是连续存储的;但是,元素的起始偏移量需要经过一些计算才能确定。由于它们的大小不可预测,动态大小的数组类型使用KECCAK256哈希函数(SHA3)来寻找数组数据的起始位置。动态数组值本身在存储中的某个位置p占据一个空槽,对于动态数组来说,这个槽存储了数组中的元素数量。而数组数据则位于KECCAK256(p)处。通过对上述实现的递归映射,数组的实现被扩展到任意嵌套的动态数据结构,这就需要进行递归分析。

MadMax:分析智能合约的gas世界

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

MadMax执行了一项分析(elided),用于建模内存布局和识别智能合约中的动态数据结构。该分析的输出结果显示在图5中。基于这些关系,我们定义了以气体为重点的分析的关键概念,如图6所示。一个重要的概念是
INCREASEDSTORAGEONPUBLICFUNCTION。存储变量增加并存储在其相应的存储槽中,意味着当某些公共函数被调用时,合约的数组大小会增加。此外,我们可以找到迭代数组的循环。我们将ARRAYITERATOR定义为一个在数组上迭代的循环。

MadMax:分析智能合约的gas世界

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

MadMax:分析智能合约的gas世界

图6. 用于识别存储需求增加的公共职能的Datalog规则。

* 5.3. 最高级别的脆弱性查询

前面几节的分析概念建立了以气体为重点的漏洞的最终查询。这些都是通过结合几个不同的概念而变得精确的。图7显示了MadMax分析的最终输出关系,其形式稍有简化(并精简为单一规则)。

MadMax:分析智能合约的gas世界

图7. 对无界大规模操作、钱包悲鸣和溢出漏洞的顶层查询。

例如,考虑UNBOUNDEDMASSOP逻辑:它检查一个可以作为公共函数的结果而增长大小的数组是否有内容被加载或存储(FLOWS(storeOffsetVar, index)允许从内容的开头解读),在一个循环内,其边界是基于数组的大小,并且包含一个影响加载或存储地址的诱导变量。

WALLETGRIEFING查询甚至更精确,要求从动态数组加载,将加载的值流向一个调用,其结果是一个抛出语句的条件。调用和抛出需要在同一个循环中,这个循环也有一个影响加载地址的诱导变量。

最后,如果诱导变量被转换为一个短的整数或最好是一个字节,循环溢出就会被保守地断定为可能。循环必须是 “动态绑定 “的,也就是说,迭代的次数是由一些运行时的值决定的。

6. 影响

我们最初的MadMax实验考虑了2018年4月9日以太坊区块链上的所有智能合约。我们在一台拥有英特尔至强E5-2687Wv4 3.00GHz和512GB内存的闲置机器上运行MadMax。由于时间限制,我们将反编译的截止时间设定为20秒–超过这个时间,合约就被认为超时了。

被标记为漏洞的合约合计包含707万个ETH,或大约28亿美元。3 在我们进行区块链刮擦时,总共有633万个合约实例被部署,由9180个独特的程序产生。其中4.1%的合约被MadMax标记为容易受到无界迭代的影响,0.12%的合约被钱包破坏,1.2%的合约被循环诱导变量溢出。

为了估计假阳性率,我们手动检查了被标记的合同的一个子集。我们的无偏抽样过程包括采取独特的字节码程序,并按区块哈希顺序选择第一个和最后几个合同。然而,由于需要在网上提供源代码,所以引入了一个偏差因素–没有源代码的合同不在考虑之列,因为手工检查低级字节码是非常耗时和不可靠的。

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

整个MadMax对91.8千份合同的分析花了不到10小时,运行了45个并发进程。随后的Gigahorse反编译器的进步使这个数字至少下降了2倍。

请注意,合同中确认的漏洞并不意味着。(1)利用漏洞很容易或很便宜,或者(2)漏洞阻断了合约中的所有以太。例如,利用无界质量操作漏洞所需的气体可能是昂贵的,使攻击者望而却步。然而,这并不影响合约对有动机的恶意行为者的脆弱性质。

. 总结讨论

我们介绍了MadMax,这是一个用于寻找Ethereum智能合约中以气体为重点的漏洞的工具。我们发现了Ethereum智能合约的新漏洞,并展示了在EVM字节码水平上首次成功设计的静态分析工具,该工具可以费力地反编译并重建程序的高层次语义。MadMax方法利用了最好的技术和工艺:从基于抽象解释的低级分析反编译到用于高级分析的声明性程序分析技术。我们的方法使用区块链上所有部署的智能合约进行了验证,并展示了可扩展性和具体有效性。我们的工具对其中一些智能合约提出的威胁在金融方面是压倒性的,特别是考虑到人工检查样本中警告的高精确度。

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

MadMax是第一个公布的检测需要跨多个交易协调的威胁的分析。这代表了自动化安全分析的未来趋势:分析需要考虑到独立交易的状态变化,早在最终攻击可以实施之前。此外,未来的威胁可能涉及多合约或整个应用程序的攻击–例如,去中心化应用程序的非区块链部分和其区块链(智能合约)部分之间的协调。对于安全分析工具来说,这是一个具有挑战性的下一个前沿领域。在MadMax的案例中,多交易推理是通过设定高级属性来实现的,比如 “安全的可恢复循环”。反过来,这也是通过分析的声明性来实现的,它允许对复杂的属性进行简洁的逻辑说明。同样的声明性方法很可能在未来将分析扩展到多合同、整个应用推理中发挥重要作用。

编辑于 2022-02-09 03:39
「 真诚赞赏,手留余香 」
赞赏

发表评论已发布0

手机APP 意见反馈 返回顶部 返回底部