从EVM字节码到结构化低级IR的反编译器:我们建议直接使用EVMbytecode进行静态编程分析。由于EVM的基于堆栈的低级特性以及最小的控制流结构,分析了EVMbytecode的挑战。
识别以天然气为重点的漏洞:在处理货币交易的智能合约之上有限的基于天然气的执行的语义引入了一类新的漏洞,这种漏洞在其他编程语言范例中不会出现。我们彻底识别出气体漏洞并解释其本质。
高级数据结构和程序构造的抽象:我们构建EVM字节码的高级抽象,以弥合低级EVM和高级漏洞之间的差距。我们表达的分析概念包括安全可恢复的循环,在公共函数的重复调用中大小增加的数据结构,以及低级内存中嵌套动态结构的识别。
验证:我们验证了整个区块链上部署的所有630万份合同的方法。据我们所知,智能合约安全文献中没有其他工作对这么多合约进行过程序分析。我们的分析不需要运行源代码,也不需要外部输入,同时具有高度可扩展性。该分析报告了总价值超过28亿美元的合同的漏洞。尽管不确定大多数漏洞是否真实以及它们可能是多么容易被利用,但是对小样本进行人工检查可以发现80%以上的精确度和特定问题的存在,我们对此进行了详细说明。
以太坊是一个分布式区块链平台,作为智能合约的生态系统:捕获账户交易逻辑的成熟交互程序。与主流语言中的程序不同,gas限制限制了以太坊智能合约的执行:只要gas可用,执行就会继续。因此,gas是一种有价值的资源,攻击者可以对其进行操纵,从而在受害者的智能合约中引发不想要的行为(例如,浪费或阻塞受害者的资金)。当合约(直接或通过其他交互合约)用完gas时,以gas为中心的漏洞利用不想要的行为。对于程序员来说,这些漏洞是最难防范的,因为在非攻击场景中,gas耗尽行为可能是不常见的,而对其进行推理也绝非易事。
在本文中,我们对gas为中心的漏洞进行了分类和识别,并介绍了MadMax:一种静态程序分析技术,可以自动检测具有高度相关性的气体聚焦漏洞。我们的方法结合了基于控制流分析的反编译和声明式程序结构查询。组合分析捕获特定于领域的高级概念(如“动态数据结构存储”和“安全可恢复循环”),并实现高精度和可扩展性。MadMax仅在10小时内就分析了以太坊区块链中的所有智能合约(8%的案例中存在反编译超时),并将货币价值超过28亿美元(高度波动)的合约标记为易受攻击。对标记合同样本的人工检查表明,81%的抽样警告确实会导致漏洞,我们在实验中报告了这些漏洞。
关键词:程序分析、智能合约、安全、区块链
以太坊是一个分散的区块链平台,可以执行任意表达的计算智能合约。开发人员通常用高级语言编写智能合约,编译器将其转换为永久分布式虚拟机的不可变低级evm字节码。智能合约使用以太(ether)进行交易,以太是一种加密货币,目前市值达数百亿美元。智能合约(与非计算性钱包相反)占据了流通中ether总量的相当大一部分,这使得它们成为攻击者的成熟目标。因此,开发人员和审计人员有强烈的动机广泛使用各种工具和编程技术,将合约受到攻击的风险降到最低。因此,智能合约的分析和验证是一项高价值的任务,可能比任何其他编程设置都要重要。货币价值和公共可用性的结合使得早期发现漏洞成为一项至关重要的任务。(检测可能发生在合约部署之后。尽管代码不变性会阻止错误修复,但在攻击者利用它之前发现漏洞可能会使受信任方将易受攻击的资金转移到安全位置。)
有大量合约漏洞涉及gas行为。gas是以太坊计算机的燃料。由于执行平台的大量复制,通过向用户收取运行合约的费用来防止浪费他人的资源。每一条执行的指令都要花费gas,gas与ether加密货币进行交易。由于用户预先支付gas,交易的计算可能会超过其分配的gas。因此,以太坊虚拟机(EVM)引发异常,并中止事务。如果合约不能正确处理可能导致的交易中止,则有可能出现以gas为中心的漏洞。通常,易受攻击的智能合约将永远被阻止,因为不正确地处理gas耗尽条件:重新执行合约的功能将无法取得进展,无法独立地重新产生gas耗尽异常。因此,合约很容易受到拒绝服务攻击的影响,从而锁住了它的账户。
在这项工作中,我们提出了MadMax:一个静态程序分析框架,用于检测智能合约中以gas为中心的漏洞。MadMax是一个静态分析管道,由一个反编译器(从低级EVM字节码到结构化中间语言)和一个基于逻辑的分析规范组成,生成一个高级程序模型。MadMax非常高效且有效:它在10小时内分析了整个以太坊区块链,并报告了从随机样本中确定的、总价值超过28亿美元、精度高的众多脆弱合约。MadMax在智能合约分析程序和验证程序方面独树一帜。这是一种采用尖端静态程序分析技术的方法(例如,数据流分析以及对数据结构的上下文敏感流分析和内存布局建模),而过去的分析师主要关注符号执行或全功能验证功能正确性。正如MadMax所展示的那样,静态程序分析具有独特的优势组合:极高的可扩展性,普遍适用性和潜在漏洞的高覆盖率。
我们推测,由于以下三个主要原因,过去的方法没有采用静态分析技术:a)认为由于市场合约规模较小,静态分析的可靠性是不必要的;b)静态分析虽然彻底,但可能会产生大量的假阳性;全功能、自动化程度较低的验证可能需要验证技术;以及c)在低级别统一应用静态分析技术的困难:将低级别EVM字节码反编译成可管理的表示是一个非常大的挑战。MadMax解决或反驳了这些异议,它为分析低级EVM字节码提供了有效的反编译基板。MadMax展示了高精度,因为它研究了以气体为中心的概念的复杂建模。最后,我们对以太坊区块链的研究(以及MadMax随后的应用)揭示了智能合约可以从静态分析中获益。图1给出了早期指示,通过绘制智能合约大小与持有的以太币。我们可以看到相对复杂的合同(以基本块数量衡量)包含大部分以太网。因此,复杂合约的潜在风险复杂化,因为复杂的合约更难以正确。这一观察结果强烈支持使用静态程序分析,该程序可以很好地扩展到相对复杂的程序。
我们确定了一些最常见的以气体为重点的漏洞模式,并通过示例进行说明。我们将Solidity用于演示目的,即使我们的整个分析工作都在EVM字节码级别。以太坊合约的机制旨在激励用户通过使他们为执行单笔交易所需的gas预付款来最小化执行的指令数量。耗尽gas,但在大多数情况下,这并非灾难性的:交易将被最终用户以更高的gas原并重新运行。不幸的是,这并不总是一种选择。很多时候,预算的gas数量已经在已经部署的其他合同中进行了硬编码,因此无法增加。此外,Solidity的发送或转移实施,可以调用其他智能合约,只能发送2300个单位的gas。最后,以太坊网络具有无法超越的gas因此,合约可能达到一种状态(例如,存储中的数据结构的大小可以增长很多),使得它们将永远不会有足够的gas来运行它们的代码。
无限大运算。以气体为重点的漏洞的最标准形式是无限大运算。其行为由用户输入确定的循环可能迭代太多次,超过块气体限制,或者变得过于经济地执行。该合约可能没有预测到这种可能性,因此未能确保合同能够在这些条件下继续按要求运作。这通常会导致必须尝试迭代循环的所有事务的“拒绝服务”。考虑下面的合同,随着账户数量的增加,执行applyInterest的天然气需求将会增加。最终,在不引起气体不足的情况下,可能无法执行该功能。以太坊编程安全建议建议程序应该避免必须为无限数量的客户执行操作(而只是让客户从合同中撤出)。这种做法通常用付款方式表示(虽然它更普遍适用)。正如我们将要看到的,大量现有的合同,持有非常大的金额,违反了这种做法。进一步的建议是,当环路确实需要为无限数量的客户执行操作时,应检查燃气量每一次迭代和合同应该“跟踪它已经走了多远,并能够从那一点恢复”。
非隔离外部呼叫(钱包诈骗)。除了由于无边界、外部控制的数据结构而耗尽gas之外,由于调用外部功能(其本身可能抛出用完gas异常),合约可能会遇到问题。在直接设置中,这不是一个现实的威胁:对未知方的外部调用是不可信的,因此合约程序员很可能考虑过恶意行为。注意,Solidity原语也被设计为鼓励这种防御设计。但是,当与其他一些复杂因素结合时,此漏洞是现实的:在ether传输时隐式代码调用、在不隔离的情况下处理多个客户端,以及在发送失败时中止的标准做法。问题的根源在于程序本身的灵活性。这种调用通常是隐式的,作为ether传输的一部分。发送ether涉及到在接收者一侧调用回退函数。因此,发送ether可能会失败,因为它调用任意的、可能不受信任的代码。考虑一个简单的代码片段(图3),该代码尝试将投资退回到最低金额以下。
问题在于,send命令还将导致执行选定投资者的回调函数。该合约易受攻击的唯一条件是攻击者将自己设为低于最低阈值的投资者,然后提供一个耗尽gas的回调函数。重要的是,上述循环不足以恢复。从同一点出发并不会带来进展(如果合约仅仅是用光了gas的话就会有进展):失败的发送如果重复,将再次失败。需要对未能发送的错误进行更高级的处理,以便将来执行合约时,将通知较早的ether传输失败(并且不会盲目地重新尝试)。
整数溢出。一种编程错误,通常表现为以gas为中心的漏洞,这是由固化类型推断方法及其可能导致的整数溢出造成的。这是与一般攻击不同的模式,因为迭代不仅是无限的,而且实际上是不终止的,因为整数溢出条件产生了意外值。考虑一下下面显示了一个潜在错误的合约。
var的使用引起了类型推断中的问题。推断类型的变量i是uint8(即,一个字节),因为变量被初始化为0并且uint8是能够保持0的最精确类型,同时与i上的所有操作兼容。不幸的是,这意味着仅仅向受款人增加256个成员就足以导致循环不能终止,很快导致气体耗尽。攻击者可以通过使用适当的公共函数(未显示)添加虚假的收款人来利用此漏洞,直到触发溢出。除了意外的类型推断之外,实际合同中确实存在更多溢出的可能性。正如我们在评估中讨论的那样,当合同设计者试图优化存储要求时,整数溢出也可能会蔓延。
对上述漏洞的最直接利用将导致锁定合同,使其无法使用。攻击者通常需要花费资金来利用漏洞,例如,使用ether来填充动态数据结构。在加密货币生态系统中,执行此类攻击的一些激励措施包括:降低以太币的价格; 在相关子社区中声名鹊起; 破坏竞争对手的合约; 勒索合约持有人(受到攻击的合约或任何其他合约)。
从Vandal反编译器到最终分析输出的MadMax管道如图5所示。主要的MadMax分析使用基于逻辑的规范对Vandal的输出进行操作。分析以Datalog语言实现:基于逻辑的语言,相当于带递归的一阶逻辑。我们还在论文中使用Datalog作为精确指定分析的方法。虽然这里给出的规则形式相对于完整实现而言是简化的,但本质保持不变。MadMax分析由几个分析层组成,逐步推断出有关分析的智能合约的更高级别概念。从地址代码表示开始,首先识别诸如循环,归纳变量和数据流的概念。然后执行内存和动态数据结构的分析,推断出诸如动态数据结构,重新进入时存储增加的合同,嵌套数组等概念。这一步非常简单,因为它需要对EVM动态数据建模表示。最后,推断了以gas为中心的脆弱性分析层面的概念(例如,无界大量存储的循环)。
curton 2019-11-25 22:15