ETHBMC：智能合约的有界模型检查器

 

智能合约的引入极大地推动了加密货币的最新发展。智能合约是生活在区块链上的程序，用于控制资金流向。但是，获得金钱收益的承诺吸引了错误的人，导致了骇人听闻的黑客攻击，导致数百万美元的货币损失。作为响应，开发了一些强大的静态分析工具来解决这些问题。对最近提出的针对以太坊智能合约的八种静态分析器进行了调查，发现它们都无法捕获以太坊生态系统的所有相关功能。例如，发现缺少精确的内存模型，仅部分支持合约间分析。

基于这些见解，介绍了基于符号执行的有界模型检查器的设计和实现，该模型检查器提供了以太坊网络的精确模型。通过一系列实验证明其功能。首先，将其与上述八个工具进行比较，表明即使是相对简单的玩具示例也可以阻碍其他分析器。为了进一步证明精确建模是必不可少的，利用ETHBmc功能进行自动漏洞扫描。对当前活跃在区块链上的大约220万个帐户进行大规模分析，并自动生成5,905个有效输入以触发漏洞。其中1,989个可以随意销毁合约（所谓的自杀合约），而其余的则可以被对手用来任意提取金钱。最后，将大规模分析与之前的两次分析进行了比较，发现比以前的方法有更多的输入（22.8％）。

 

0x01 Introduction

自2008年推出比特币以来，加密货币在学术界和行业中都获得了相当大的关注。 称为区块链的底层技术最初被设计为一种分散的点对点支付协议，而无需受信任的各方。 最近，这项技术还在许多不同领域得到了应用，例如供应链管理，资产转移或医疗保健。 区块链是由网络的所有参与者维护的分布式，仅追加的分类帐。 参与者运行共识协议以将新数据（即所谓的块）附加到分类账，从而使网络中的交易成为可能。

智能合约，直接部署在区块链上的程序允许用户对有关如何以及何时进行交易的复杂规则进行编码。例如，当特定事件发生时，合约可以转移资金。甚至有可能将多个合约链接在一起以表达更复杂的逻辑。这个想法由Szabo于1997年首次提出，但由以太坊于2014年提供了第一个现实世界实现方法。实际的智能合约通常以高级语言编写，以太坊最常使用Solidity。然后，将这些高级语言编译为字节码，该字节码在基于事务的状态机以太坊虚拟机（EVM）上执行。

这提供了很大程度的控制力，并保证了多种用例，例如状态或付款渠道，分散式加密货币交易所和多签名钱包。不利的一面是，智能合约与其他程序一样，也会遭受软件故障的困扰。在传统程序中，这可能“仅”导致崩溃，而在以太坊世界中，一个简单的错误可能会带来更直接的后果（通常是财务方面的后果）。臭名昭著的奇偶校验事件就是一个很好的例子。首先，攻击者利用共享库代码中的错误窃取了价值超过15万的以太坊（以太坊区块链背后的加密货币）。在遭到黑客攻击时，这笔交易的价值约为3000万美元。在第二个事件中，当时被打补丁的库再次被利用，这次导致超过514,000个以太坊（约合1.55亿美元）无法访问。

已经提出了几种以自动化方式检测软件故障的建议。对来自学术界和工业界的此类自动分析工具进行了调查，发现它们都至少缺乏以下类别：（i）合约间推理，（ii）内存建模，尤其是内存复制式操作，或（iii）加密哈希函数的处理。

在本文中解决了这些缺点，并介绍了ETHBMC的设计和实现，ETHBMC是基于符号执行器的智能合约自动分析框架，与最新工具相比，它对EVM内部使用更强大，更精确的推理。 ETHBMC被设计为有界模型检查器，可以根据智能合约的代码检查预定义模型。在模型被违反的情况下，ETHBMC可以自动生成具体的输入以简化进一步的分析（即，生成了一系列交易来证明检测到的漏洞）。因此，ETHBMC是第一种以完全自动化的方式识别奇偶校验漏洞的方法，甚至能够生成第二次利用原始攻击未使用的攻击。

为了证明工具的功能进行了一系列实验，将方法与被调查的分析仪进行了比较。主要目的是，即使是简单的示例也可能妨碍其他方法的不精确分析。接下来，将ETHBMC的功能作为自动生成漏洞利用的手段，扫描以太坊区块链（截至2018年12月）上的所有账户，生成5,905个漏洞利用。从这5905个漏洞中发现1,989个可用于任意破坏合约（所谓的自杀合约），其余的可用于提取金钱。此外，将本研究的大规模分析与该主题的两项先前的工作进行了比较。首先将分析结果与最新的自动漏洞利用生成工具teEther进行比较，证明了本文的方法可以在更短的时间内发现更多漏洞（22.8％），同时还能识别teEther中的假阳性。其次将其与一个可以使人找到自杀合约的执行器MAIAN作比较，并再次发现ETHBMC发现了更多的利用。最后对ETHBMC引入的技术进行消融研究，以定性的方式显示这些改进。在重新扫描易受攻击的合约时会系统地禁用其功能，从而了解不同技术如何对分析结果做出贡献。

为了促进智能合同安全的研究，ETHBMC的代码可在 https://github.com/RUB-SysSec/EthBMC 上获得。

 

0x02 Background

在深入介绍分析过程的技术细节之前，简要介绍了有关加密货币和以太坊虚拟机（EVM）的所需背景信息。

1）加密货币

2008年，中本聪（Satoshi Nakamoto）引入了比特币和区块链的概念，这是一种在对等网络上运行的去中心化分类账。非正式地讲，区块链是一个公共的，仅附加的分类账，用于存储系统中发生的所有事件。参与者运行一个共识协议，该协议可以确保只要网络的大多数行为都是诚实的，总账是正确且安全的。

以太坊可以在许多方面被视为“比特币2.0”。由Buterin于2013年推出，它是一种具有图灵完备字节码语言的加密货币，可以协调系统中的价值转移。网络中的参与者由一个160位地址标识，该地址从ECDSA非对称密钥对的公共部分派生而来。在以太坊的情况下，这些所谓的帐户可能还会附加代码。这种帐户称为智能合约，将复杂的行为编码为字节码程序。用户可以以Ether的形式互相汇款，或者通过将交易提交到对等网络并用其私钥进行签名来执行智能合约代码，从而证明交易的正确性。尽管智能合约的执行时间受称为gas的参数限制，即保证程序最终终止的费用，但合约可以通过将交易链接在一起或使用多个合约拆分逻辑来实现相当复杂的行为。

2）以太坊虚拟机

以太坊定义了一种专用的，基于堆栈的虚拟机，称为以太坊虚拟机（EVM），用于确定智能合约执行的结果。以太坊在黄皮书中提供了正式规范，其中定义了EVM的整个内部工作方式。该机器对字节码进行操作，其中每个操作数将值弹出或推入数据堆栈，每个值具有256位字长。此外，EVM增强了针对加密货币环境量身定制的多种机制。

World State ：以太坊世界状态是整个系统的状态。在本文的其余部分将其称为环境。它由两部分组成，从帐户地址到帐户状态的映射以及当前块信息。帐户状态是一个元组，其中包含多个信息，例如帐户的当前余额。此外，如果帐户是智能合约，则帐户状态还包含字段代码和存储。代码字段保存智能合约的代码，而存储是用于在多个合约调用之间保留值的永久性存储器。

内存：EVM区分三种不同类型的内存，

•存储：存储是一个持久的键值存储，它将256位键ping到256位值。

•Calldata：交易的数据部分用于向合约提供用户输入。注意，这是一个可字节寻址的数据数组，在执行期间是不变的。

•执行存储器：该存储器是易失性字节数组，仅在整个执行过程中一直保持不变。它在经典计算机程序中像堆一样被使用，例如，在计算过程中存储中间结果。
该设置创建了具有独立指令和数据存储器的哈佛式架构。另外，EVM提供了内存复制式的操作，例如CALLDATACOPY，它将部分调用数据复制到执行存储器中。

3）符号执行和SMT解决

虽然研究的工具是基于多种不同的程序分析技术的，但ETHBMC是基于符号执行的，因此提供了简要的介绍。符号执行最初被设计为一种软件测试技术，但此后已被安全社区用于程序分析。符号执行将所有输入视为符号变量，而不是具体的输入，它们在程序的整个输入域中范围内。直观地讲，对于函数f（x），符号执行不是考虑一个具体的执行轨迹，例如f（10），而是考虑符号输入ϕ。产生符号函数执行f（ϕ），其中ϕ代表整个输入域，例如32位整数，因此探索了程序可以采用的所有可能路径。当到达分支（例如，if语句）时，将执行分支以探索两种可能的路径。为了保持较低的探索状态空间，符号执行器将程序的当前状态以及路径条件（例如，x <= 3）编码为一阶逻辑公式，并使用可满足性模理论（SMT）求解器检查程序路径是否可行，避免进一步探索不可能的路径。

SMT公式用一阶逻辑表示，它是命题逻辑（也称为布尔逻辑）的扩展，它为表达问题提供了多种不同的理论。 SMT求解器通过枚举执行证明：它试图找到约束系统的满意（具体）分配，从而证明可以求解。在对程序的执行进行建模时，此具体分配为程序提供了输入，可用于达到给定状态。当另外将故障条件编码为逻辑公式并为二者找到令人满意的分配（即执行和故障条件）时，此具体分配是触发相应软件故障的程序的输入。

 

0x03 Challenges in Analyzing Smart Contracts

1)智能合约中的常见障碍

(a) Keccak256函数

EVM提供了一条特定指令，用于在执行内存区域上计算keccak哈希。基于实体的智能合约在实现映射数据类型（本质上是像数据结构的哈希表）时会大量使用此指令。而且，该功能可以由智能合约开发人员手动调用，例如，以实现诸如承诺方案之类的密码协议。

List 1演示了keccak函数的简单用法，可以通过keccak256关键字调用该函数。List 2中提供了对该函数的更“隐藏”用法，其中该指令用于计算内存位置。请记住，EVM的存储是单词可寻址内存。固定大小的数据类型具有一个固定的内存插槽。但是，在处理动态数据类型时，即在执行期间其大小可能会增加的类型时，不知道要分配多少个内存插槽。基于实体的智能合约求助于即时计算内存偏移。写入映射时（第3行），相应的内存位置将计算为keccak256（k||p），其中k是映射（映射）的关键，p是在编译时选择的常数。注意，如果可以使用此方案生成有效的哈希冲突，则先前的值将被覆盖。

（b）类似内存复制的指令

EVM无法直接访问调用数据，它只能对执行内存中的数据进行操作，即复制输入数据。在List 3中，字符串是无限制的数据类型，导致EVM利用CALLDATACOPY指令将整个输入复制到执行内存。这与具有固定宽度（例如uint256）的数据类型形成对比，该数据类型可以通过从calldata的普通读取中进行访问。

（c）合约间通信

Kiffer等人最近的一项调查进一步促进了合约间分析的需要，以太坊当前的合约拓扑。他们指出，大多数合约不是由人部署的，而是由其他合约创建的，从而使这些合约成为合约内交互的一部分。

2）奇偶钱包错误

基于这些示例，现在将原始的奇偶校验钱包错误作为真实示例进行检查，在该示例中，需要解决所有以前的问题以获得全面的分析。尽管已经研究了其他类型的智能合约漏洞，但如何以自动化方式检测奇偶校验事件仍然是一个尚未解决的挑战。请注意，本文仅介绍与该分析相关的摘要，对其进行了简化以简化阅读；可以在网上找到完整的源代码清单。

Parity钱包分为两个合约，一个是持有大部分代码库的库合约，另一个是用户部署的客户合约。一旦部署，智能合约就不会改变，因此，当更改（或确定）合约时，必须重新部署并因此偿还整个合约。为了减轻用户的负担，在拆分逻辑时，仅需要重新部署库。 EVM提供DELEGATECALL指令，该指令用于在执行时使用另一个帐户的代码。这些指令在仍然使用原始帐户上下文和存储的同时切换了要执行的代码。考虑List 5，假设用户Alice要使用Parity钱包库。她使用存储变量部署她的客户代码（第15-23行），该存储变量包含库合约的帐户地址（第16行）。稍后调用客户合约时，它将交易委托给库代码（第22行），并转发交易的通话数据（msg.data）。请注意，这还意味着如果攻击者可以将合约的控制流重定向到自己喜欢的地址，那么他们就有能力任意执行代码（例如提取所有资金）。

由于区块链上的每个人都可以调用任何合约，因此智能合约开发人员已经发明了所有者的概念，该变量通常在合约创建过程中设置，用于指定合约所有者的地址。对于奇偶校验多重签名钱包，甚至存在在创建钱包（第7-9行）时初始化的一系列所有者（第2行）。尽管变量是在库代码中定义的，但是由于执行上下文位于原始帐户中，因此变量是在客户合约上设置的。

分析障碍：除合约间通信外，Parity钱包还使用keccak功能，既作为普通调用（第11行），也用作映射数据类型（第3行）。在对msg.data（第11行）进行哈希处理时，由于其（理论上是）无限制的大小，因此会将整个数据复制到执行内存中。因此，静态分析器必须能够推理出合约间的通信以分析所分配的合约以及类似于内存复制的指令和加密散列函数以彻底分析支付函数。

攻击者利用了initWallet函数未标记为私有的事实。在Solidity中，这意味着它默认为public，即任何人都可以调用它。因此，攻击者首先调用initWallet函数，使其成为所有者，然后使用付款函数将钱包的所有资金转移到他的帐户中。请注意，攻击者必须执行两次交易，因此仅分析initWallet是不够的，因为实际的攻击发生在pay函数中。

3）最先进的技术

为了对现有方法进行调查，从程序分析领域中基于不同原理选择了各种工具，范围从数据流分析（安全化）到符号执行（Manticore，Mythril，MA IAN，Oyente和teEther），以抽象解释（Van dal和MadMax）。本文无法充分介绍每种技术，但是，有兴趣的读者可以参考Nielson等人的出色著作。

在审查中，发现所有工具都使用某种过度逼近的方法，这可能会引入错误的积极因素。因此将“验证”定义为另一个潜在障碍。也就是说，此后是否正确验证了任何过度逼近？上表给出了本文分析结果的概述。请注意，MadMax基于Vandal，因此它继承了其局限性，下面仅详细讨论Vandal。

（a） Keccak256函数

由于keccak计算的普遍性，本研究分析的大多数工具都提供了某种策略来在分析过程中对其进行处理，但是所有这些工具都不精确。所有工具都支持在具有恒定参数的恒定执行内存区域上计算keccak值（即，每个内存值都是非符号的）。这使他们可以提取相应的内存区域并计算实际的哈希值。

安全考虑在符号计算期间将每个内存位置都视为潜在的依赖项，即使实际上是不可行的。 Mythril在遇到符号偏移量或内存的符号部分时，会将keccak值与新的不受约束的符号位过分近似。当任何内存值或自变量是符号时，Manticore会使用一个调和策略，并将其值固定为常量。但是，它们保留所有先前计算的哈希的映射，并尝试将当前哈希与已看到的哈希进行匹配。同样，teEther在符号执行期间存储一个占位符对象，然后应用一个策略策略来解析所有可见的占位符。 Vandal不会尝试任何具体的或符号处理，但会忽略指令并将结果视为新的符号变量。上述方案的异常点是Oyente，它仅支持具体的keccak计算，但不花力气计算实际值。它宁愿提取内存区域的字符串表示形式，对其进行压缩和base64编码，然后使用此编码作为映射来匹配以后的哈希计算[37]。

本文解决方案：遇到符号keccak值时，使用特殊编码方案。该方案基于keccak是绑定函数的想法，即，当将相同的输入提供给该函数时，它将产生相同的输出。当它们的输入存储区可以相同时，通过向执行添加约束，将不同的keccak计算编码为相同，来利用这种行为。

（b）内存建模

审查显示，没有经过检查的工具完全支持精确的内存模型。一些人采用过分逼近或固执策略来规避关于符号记忆复制式操作，而另一些人则选择不支持它们。更具体地说，MAIAN支持符号读取操作，但会删除任何符号写入或内存复制式操作。 Mythril支持标准的读/写操作，但是在输入复制指令时会遇到麻烦。它正确地处理了具体的问题，但是，例如，当向主题复制操作提供符号偏移量时，它要么删除路径，要么将其大小固定为1。同样，Manticore和teEther完全支持简单的内存操作，但否则请采用concil策略。当遇到任何符号内存写入时，Securify会表现得比较保守，会清除整个内存，因为它不再能推理出具体细节。 Oyente和Vandal都不支持任何基于副本的指令。

本文解决方案：与以前的工作相反，本文采用了完全符号存储模型。将内存表示为图形表示，当从一个内存复制到另一个内存时，连接不同的内存区域。当需要评估给定路径的可行性时，使用众所周知的数组理论以及Falke等人的扩展，将主题图编码为约束解决类似内存复制的操作。

（c）合约间分析

Mythril和Manticore是仅有的两个支持合约间分析的工具，但是，两者都以不精确的方式进行。当合约与另一个合约交互时，下一次执行的输入来自被调用者的执行内存。Mythril和Manticore都支持完全具体的合约调用，即，如果用作调用数据的执行内存部分完全对应于具体值，则执行将照常继续。但是，当相关内存区域中的任何值都是符号性的时，两种工具都采用不同的策略来解决该问题。 Mythril忽略了执行内存的内容，并通过创建一个新的不受约束的数组对象来过度逼近调用数据。相比之下，Manticore采用了一种锥度方法，将任何符号值固定为常数。

本文解决方案：利用支持符号复制指令的内存模型来正确地为调用操作建模输入内存。

（d）验证

本节中讨论的所有工具都严重依赖于过度逼近。想强调的是，这是一种常见的方法，对于对抗状态爆炸是必不可少的。尽管如此，这些设计选择显然会导致误报。认识到这些问题，MAIAN和teEther都使用私有链来在受控环境中模拟其错误发现。其他方法均未尝试修剪潜在的误报。

本文解决方案：遵循先前的工作，并模拟每个潜在的错误，将其作为具体的脱机执行以清除误报。

 

0x04 Modelling Ethereum

在下文中概述了作为ETHBMC基础的理论模型。从攻击媒介概述和一般介绍入手，进入环境建模，广泛介绍支持内存复制的内存模型，最后描述对call和keccak指令的处理。

1）攻击者模型

ETHBMC提供了以太坊生态系统的符号化，多账户功能表示，可用于检查任意模型。为了演示其功能，对认为最关键的三个特定攻击媒介进行了建模：首先，是一个想要从分析的合约中提取以太币的攻击者。其次，想要将分析后的合约的控制流重定向到自己的帐户的攻击者。第三，想要自毁分析后的合约的攻击者。请注意，仅要求攻击者能够参与以太坊协议，从而为她提供网络和区块链的实时视图，包括对合约的存储和字节码级别访问（即对世界状态的访问）。

2）高层概述

本研究想尽可能合理地推理智能合约。这涉及到包含多个合约交互的EVM的精确模型。但是，就像所有静态分析器一样，必须选择要精确建模的模型和过高近似的模型。决定既不对共识协议以及gas使用量建模，保证无效交易不会被执行，因此不会影响智能合约状态。而且要分析的代码必须在实践中可执行，即它必须具有合理的耗gas量。

将EVM建模为抽象状态机（ASM）Γ，提供了执行上下文，在该上下文中可以推断合约的执行情况。 ASMΓ以字节码数组Σ作为输入，即合约代码，并从第一条指令开始执行。完成执行后，机器将返回所有停止状态σh的集合，即Γ达到非异常停止条件的所有状态的集合，如黄皮书所定义。

另外定义了一个状态σ=（µ，pc，Π），其中µ表示堆栈，pc是指向下一条指令的程序计数器，Π是给定路径的路径约束集。还将µ[0]定义为堆栈的第一个（最顶部）参数，将µ[1]定义为第二个参数，依此类推。

3）环境建模

想在执行者中建立一个丰富的环境模型（即世界状态）。因此，将帐户状态定义为元组α=（balance, code, storage）。其中balance是一个符号值，表示帐户余额。 code是属于帐户的（可选）代码，storage是256位至256位键值存储，其中包含持久帐户状态（也是可选的）。

另外，将事务（tx）定义为元组（origin, recipient, callvalue, calldata, calldatasize）。 origin是交易的原始帐户地址，recipient是收件人，callvalue是附加在交易中的值，calldata是附加在交易中的（可选）calldata，并且calldatasize是代表变量大小的符号变量。 calldata数组（还是可选的）。

通过添加一个映射帐户来扩展Γ的定义：address→α映射帐户地址到它们各自的状态，即世界状态。此外，介绍了代表系统中所有已发行交易的设置交易。分析特定合约时，设置了一个攻击者帐户和（可能有多个）受害者帐户计数。然后模拟交易链t1，t2，…，tk。对于每笔交易，执行完整的Γ运算，得出停止状态σh。然后，对于每个σi∈σh，分叉执行并继续下一个tj直到tk。

4）内存模型

（a）内存图

该图本身用于跟踪对内存的所有修改。它从一个初始节点开始，并在每次对内存的读/写操作时进行更新。更正式地讲，引入存储所有存储节点的内存图∆ =（V，E），并将其添加到状态定义中，即σ=（µ，pc，Π，∆）。为每个节点分配一个唯一的索引。因此，将索引为i的节点表示为ni。此外为每个节点分配一个标签，即初始化标签或内存更改操作（写，复制或设置），以跟踪创建该节点的操作。

目前，仅考虑一个存储区域，例如存储年龄。从初始节点s0开始，每次创建一个连接到其父节点su的新节点st时，每次遇到对内存的写入（例如SSTORE）时都会更新图形。这为在执行期间的任何状态下提供了唯一的内存映像（类似于编译器理论中已知的静态单分配（SSA）形式）。当将内存布局转换为约束时，从最新的节点st开始，以向后遍历图的方式收集所有内存更新，并根据它们的相应标签将它们编码为逻辑公式。这种方法使本文能够推理符号存储操作。

当考虑多个内存区域（例如执行内存和调用数据）时，为每个区域引入一个初始节点，即图以森林开始，并且只要内存操作仅在单个内存区域上运行就保持不变。它可以通过两种不同的方式进行连接。首先，间接地从一个区域加载并存储到另一个区域，并通过约束隐式链接图的两个部分。其次，直接通过内存复制样式操作（例如CALLDATACOPY），通过节点和边明确地链接图形的两个部分。加载和存储会在系统中引入约束，在将内存区域转换为一阶逻辑时链接它们。复制会在目录林的目标树中引入一个新节点（例如，CALLDATACOPY的执行内存）。该节点连接到内存的源区域和目标区域，并显式链接图形的两个部分。

（b）常规内存操作

在执行期间，对于每个帐户，都会创建一个新的存储节点nj并将相应的索引存储在其帐户状态α.storage←nj中。同样，每次事务都会创建一个新的呼叫数据并存储其标识符。另外，为ASM分配一个执行内存Γ.m←nk。定义对内存的读写如下：

•∆.write（ni，p，v）→nj：将值v写入以存储节点ni为父节点的地址p，返回新节点nj。

•∆.read（ni，p）7→v：从存储器ni的位置p读取值v。

这使对SSTORE指令的建模变得简单：

)

在此示例中，将值µ[1]写入帐户（α.storage）的当前存储区到地址µ[0]。通过在内存存储区∆中创建一个新的内存节点nj来表示这一点。然后将此新存储节点的索引分配为当前帐户存储α.storage。

由于EVM的字长为256位，因此对其他存储器操作进行建模更加困难。但是，calldata和执行存储器都是可字节寻址的存储器。结果必须在256位和8位多块之间转换。

用µ [i] [0]表示µ [i]的最低字节，用µ [i] [31]表示最高（最左边）的字节。将MSTORE建模为对执行存储器的32个8位写入序列，从而相应地移动地址和提取的8位大小的块。从执行存储器中读取数据的方法与此类似，在读取索引移位的同时读取8位块，将结果串联起来。

在对CALLDATALOAD建模时，EVM将calldata定义为理论上无界的数组。因此，当存储操作读取超出范围（即，大于calldatasize的位置）时，EVM只是“读取”零。因此，对于每次从calldata读取的操作，将其包装在ite（IF-THEN ELSE）操作中，该操作会限制在提供的地址超出范围时将负载评估为零。

（c）支持存储器复制和存储器集样式的指令

EVM提供了多个指令，这些指令的行为类似于内存复制。在∆上定义以下函数：

•∆.set∞（ni，p，v）→v：将存储器ni中的所有值（从位置p开始）设置为值v

•∆.copy（ni，p，nj，q，s）→nk：从节点nj复制一个大小为s的块，从位置q开始直到q + s，复制到节点ni，从位置p开始复制直到位置p + s

这些函数可实现内存复制式操作并简化内存初始化。存储寿命和执行内存在生命周期开始时均假定为零。利用set∞函数，可以初始化这些区域。

5）模拟调用

如前所述，EVM提供合约以相互交互。考虑下图，假设模拟了针对合约A的用户交易。

将首先设置一个ASMA以模拟合约A的执行，从而生成A的执行树。现在假设-在执行期间-遇到了对合约B的消息调用。然后设置ASMB，在整个exe中运行割，然后为每个状态σi∈σh划分执行树。这能够为消息调用模拟每个可能的结果。请注意，该技术可以递归地应用于模拟嵌套消息调用。

同样，在执行DELEGATECALL或CALLCODE指令时，会切换ac计数的代码并按上述概述进行操作。当调用另一个帐户时，EVM使用部分执行内存作为新执行的输入。继续运行示例，当执行从ASMA到ASMB的消息调用时，在∆中创建一个新的calldata节点，然后利用复制函数能复制来自ASMA执行存储器的输入。当ASMB的执行完成时，将部分执行内存从ASMB复制到ASMA，作为返回数据。

6）处理Keccak指令

EVM提供了一条特定指令，用于在部分执行存储器上计算keccak-256哈希。然而，过去已经证明这些功能很难进行静态分析。一种常见的技术是使用Ackerman编码，该编码用于编码不可解释的函数。它利用了加密散列函数是绑定函数的事实，即，在相同的输入下，保证该函数产生相同的输出。可以如下利用该属性：

但是，由于EVM在执行内存上计算keccak函数，因此无法直接将这种编码用于本文的目的。遇到keccak计算时，将按以下步骤进行操作：如果所有因变量和内存区域都是常量，则只需计算常量哈希值即可。否则用占位符对象替换结果，该占位符对象存储执行内存的当前映像以及keccak计算的开始和结束地址。当要评估给定执行路径的可行性时，不是直接在输入上编码等式（1），而是为每个内存地址编码。

更正式地说，用三个字段定义元组keccak：（i）keccak.addr，起始内存地址，（ii）keccak.len，要考虑的内存范围的长度，以及（iii）keccak.m，其中是计算时存在的执行内存的索引。使用算法1对所有可能的keccak元组对进行编码。假定要转换为一阶逻辑并添加到路径约束Π的两个不同的元组i和j。首先尝试利用更复杂的编码。但是，在无法争论len参数的情况下（例如，一个参数是不受约束的符号变量），求助于后备编码（第2-3行）。

假设i.len和j.len都是常数，可以使用更复杂的方案。首先，如果i.len 6 = j.len（第4行），可以简单地反驳两个值计算为相同的哈希，因此只需将i 6 = j添加到Π。其次，当两个值匹配时（第6-16行），在用于哈希计算的可能的内存位置（第9-13行）上构造一个嵌套的ITE（IF-THEN-ELSE）表达式。在构造编码时，在每个级别上都会检查是否可以轻易证明两个内存位置相等（第9行），否则可以立即中止（第10行）并将两个keccak值编码为不相等（第15行）。否则将沿着len参数的范围（第8行）进行迭代。遍历每个内存位置（第9-12行），构造条件∆ [im，i.addr + k] = ∆ [jm，j.addr + k]，编码为i的内存位置必须与j相同计算到相同的哈希值。在每次迭代中，将ITE表达式的真实分支分配给循环的前一次迭代的编码，特殊情况是循环的第一次迭代提供i = j。因此，如果后端SMT求解器遍历嵌套编码，并且可以证明所有内存位置都相等，那么它将最终到达最终谓词i = j。但是，如果它证明任何条件都成立，则得出否定谓词i！= j，在构造的每次迭代中都将其赋值。

乍一看，要求两个keccak元组都依赖恒定长度的参数似乎是一个强大的假设。然而实际上，通常是这种情况，例如，在固定大小的数据结构上计算的keccak值始终具有固定的长度，对于计算映射数据类型的内存偏移也是如此，可通过keccak操作对其进行访问。因此，额外地提取了计算的关键部分，以便以后匹配读/写。

另外，当遇到带有常数变量的相等检查时，即keccak == c，其中c为常数，可以立即得出结论，结果必须是不相等的。否则，假设可以计算哈希冲突。换句话说，假设可以计算一个特定的输入，这将导致keccak函数的（恒定）输出。注意：在特定情况下，攻击者可能知道生成c的正确输入。

 

0x05 Design and Implementation

现在，提供了ETHBMC架构的概述，下图提供了图形概述。该工具包含三个主要模块，即符号执行器，检测模块和验证模块。 ETHBMC在大约13,000行Rust代码中实现。

ETHBMC利用其符号执行引擎来探索程序可以到达的可用状态空间。在探索过程中，可以随时将达到此状态所需的必要条件（或约束）转换为一阶逻辑。探索结束后（即执行终止），将使用其他约束对攻击者的目标进行编码。例如，对一个约束进行编码，使攻击者的帐户余额在执行的最后一个状态必须高于在执行的第一个状态。然后，利用后端SMT求解器来求解约束系统。SMT求解器通过枚举执行证明：它试图找到约束系统的满意（具体）分配，从而证明可以求解。对智能合约的完整执行进行建模。因此，既达到有效的暂停状态又满足攻击者模型的令人满意的任务证明了合约中的漏洞。此外，由SMT求解器找到的具体分配是智能合约的有效输入（即交易），最后通过运行具体的脱机执行来验证该漏洞利用是真的。

1）符号执行器

执行器以广度优先搜索方式探索合约。每当执行者需要断言给定代码路径的可满足性时，都会查询后端SMT求解器。本文评估了不同的求解器，发现在此问题域中，Yices2优于其他方法，例如Boolector和Z3 。本文探索所有代码路径，直到它们到达停止状态，或者求解器超时或拒绝该路径。如果在执行过程中遇到循环，则使用循环展开，即执行n次循环，然后退出循环。本研究在限制调用深度方面使用了相同的策略，因为在具有多个帐户的环境中，合约可能会无限循环地相互调用。此外采用了几种标准的符号执行优化技术：恒定折叠，算术重写和约束集缓存。当执行器处于挂起状态时，所有最终状态都将传递到检测模块以进行进一步分析。

2）检测模块

本文使用其他路径约束对攻击者的目标进行编码，例如施加一个附加约束，以指定在执行当前交易后，跟踪者帐户的余额必须高于整个分析开始时的余额。当遇到DELEGATECALL或CALLCODE指令时，创建了一个附加的状态劫持，在这里试图劫持合约的控制流。为劫持添加了一个约束，将CALLCODE / DELEGATECALL的目标地址约束为攻击者的帐户广播。如果这个约束是可以满足的，可以重定向控制流。同样，标记执行SELFDESTRUCT指令的状态，以检测可被外部攻击者破坏的合约。请注意，如果可以使用SELFDESTRUCT指令从帐户中窃取资金，则ETHBMC会检测到这两种情况。如果检测到任何类型的漏洞，则会将相应的状态传递给验证模块。

如果无法检测到任何攻击，则会计算状态改变状态的集合，即经历环境变化的σh子集。只有这些状态才能在执行程序中引发新的路径，其他状态将导致与上一轮中探讨的初始状态相同。因此仅进一步探讨这些状态。

3）验证模块

在最后一步中，试图为每个具有可行攻击路径的状态生成有效的事务。利用SMT求解器生成触发漏洞所需的事务数据。在成功生成攻击数据后，利用go-ethereum工具套件，特别是EVM实用程序，以离线方式模拟攻击。 这能够模拟所有生成的事务并检查它们是否与所需的攻击向量匹配。

 

0x06 Evalution

1）现有技术的实证分析

首先将ETHBMC与前文中检验的静态分析工具进行比较。使将SELFDESTRUCT指令嵌入每个合约中，因为所有工具都为此提供了检测模块。此外，重新创建了检查的奇偶校验帐户黑客程序，以模拟复杂的实际情况。下表列出了本研究的发现。

分析设置：不幸的是无法让MAIAN正常工作；目前，分析器所需的多个库不兼容。作者既没有指定他们在原始文章中使用的版本，也没有回答有关这些问题的多个GitHub问题。同样，本文仅讨论Vandal，因为MadMax继承了其函数。

在撰写本文时，根据工具的最新版本进行了评估。这对应于github commit d7b7fd1上的teEther，版本0.2.4中的Manticore，0.20.0中的Mythril，github commit f7bfee7 上的Vandal，在github commit 8fd230和Oyente上的安全在github上提交6c9d382 。虽然Oyente提供了一种检测暴露的SELFDESTRUCT指令的模式，们在测试过程中发现该模式似乎是固有破坏的。为了进行健全性检查，测试了一个仅带有一个单行函数的简单合约，该函数可以自毁合约（即List 1中没有周围的if子句）。 Oyente将合约标记为不脆弱。因此将其从实验中排除。

为了进行评估，将所有合约编译为字节码，并将其用作不同分析器的输入。这保证了所有工具之间的比较是公平的，没有人可以利用源代码信息获得好处。

Keccak256函数：从简单的合约测试开始，即对分析器建模哈希函数（即List 1）的能力进行测试。合约将哈希输入与随机选择的常数值进行比较。 如果攻击者想通过检查（第2行），他们将不得不提供一个预映像。由于keccak是一种加密安全的哈希函数，因此在实践中这是不可行的，并且合约也不容易受到攻击。

Manticore，Securify和ETHBMC正确地将合约标识为安全的，所有其他工具均报告存在漏洞。但是，根据源代码审查，teEther应该可以通过实验。在合约的第一次通过中，teEther使用二进制切片来查找导致潜在脆弱状态的路径。在第二条路径中，它象征性地执行这些路径，以查找可能达到此状态的输入。但是，对于此实验，teEther报告它找不到包含SELFDESTRUCT指令的潜在路径。根据理解，它仅应在第二遍中放弃可利用合约的可能性。因此，对于该实验，将teEther列为不正确的。

由于映射数据类型的普遍性，将继续使用List 2中列出的合约进行分析，一个攻击者可以通过首先调用createUser，提供自己的帐户地址作为输入，然后与她调用destruct来利用该合约分配的ID。只有teEther和ETHBMC才能找到脆弱状态。

内存复制操作：下一个实验旨在测试执行者对内存复制式操作的处理方式。使用List 3中所示的协定。由于输入定义为字符串，因此使用类似于memcopy的指令将calldata复制到内存中。

乍一看，Securify似乎通过了实验，报告了一个易受攻击的状态。但是，这与前文中的源代码审查直接冲突，因为发现它只是忽略了像memcopy这样的指令。因此进行了第二次验证实验，如下所示：

运行该实验两次，一次按原样进行，另一次对第2行的条件取反，导致Securify将这两个实例标记为易受攻击。这证实了对Securify不能正确推理此程序的怀疑，因为上述实例显然是不容易受到攻击的。对所有工具重复此实验，但结果没有改变。除teEther和ETHBMC之外的所有工具都无法找到易受攻击的状态。

合约间分析：对Mythril进行合约间分析非常困难；该工具支持合约间分析，但是合约必须已经部署在区块链上。因此将它们排除在此测试之外，仅让Manticore进行评估，因为其他工具均不支持合约间分析。使用两个合约库和Target来模拟该实验，以反映List 4中给出的示例。假设Target是要分析的合约， Manticore和ETHBMC都为该示例找到正确的输入。

Mythril提供了一种链上分析模式，可以从链上下载所有必要的实时信息。不幸的是，它仅支持当前最新块的分析。本文扩展了该工具以使其能够处理过去的块，并且当前正在将该补丁提交到上游存储库。但是，在分析奇偶合约时，Mythril不报告任何漏洞。

ETHBMC确实支持类似于Mythril的模式：在特定块中提取存储信息，并使用它们预先配置环境。当到达任何基于调用的指令时，提取任何常量参数并加载相应的接收者合约。 ETHBMC完成分析并正确报告两种利用合约的方式。在实际的奇偶校验代码中，构造函数和初始化代码分为两个函数。因此，攻击者可以直接调用暴露的构造函数或初始化方法。 ETHBMC会为这两个漏洞生成有效的攻击代码。

Manticore不支持任何类型的在线分析。因此，在相应的块中提取存储参数，并利用两个帐户的API来建立测试环境。处理完第一笔交易后，Manticore报告它尚未检测到任何可以进一步探究的状态，并完成了分析而未报告任何问题。

2）大规模分析

为了进一步评估ETHBMC，对截至2018年12月24日在Google BigQuery上列出的所有2,194,650个帐户进行了大规模扫描。将扫描分为三个阶段，使得可以将其与之前的两个大规模大规模进行直接比较进行的实验：第一次是Krupp和Rossow，第二次是Nikolic等。 Kruppand Rossow提出了teEther，它将二进制切片与符号执行结合使用。该工具侧重于提取以太币，以及重定向控制流。 Nikolicet等开发了可以执行自杀合约（即任何人都可以销毁）的MAIAN。下表中列出了本研究的发现，下面将对其进行详细讨论。请注意，例如在奇偶校验中，ETHBMC经常发现多种利用同一漏洞的方法，因此，在分析中列出了在分析过程中发现的不同漏洞数量。

实验设计：由于运行存档节点，因此可以在任何给定的块高度上自由地重新创建帐户环境。利用此功能首先重新创建Krupp和Rossow进行扫描的环境，然后分析其数据集列出的所有帐户。随后，提取了Nikolic扫描时出现的所有合约地址。由于希望避免不必要的合约重新扫描，因此继续仅扫描teEther和MAIAN帐户集之间的差异。通过收集所有新创建的帐户以及帐户状态在两个区块之间变化的所有帐户来计算此差异，从而对区块链的观点“更新”到较新的区块。最后，使用相同的方法来计算MAIAN扫描与截至2018年12月在Google BigQuery上列出的所有帐户之间的差异，从而提供了当前以太坊漏洞态势的完整视图。请注意，同时选择了teEther和MAIAN扫描，因为这两种工具均提供了误报修剪功能，因此可以进行合理的比较。

由于分析的规模，必须对ETHBMC施加一些限制。分析配置为使用30分钟超时。此外，将循环执行绑定到一个迭代中，对于后端SMT求解器使用两分钟的超时时间，并且最多只能加载10,000个存储变量。当一个账户链上的余额为零时，假设10个以太币的替代物，因此模型检查器可以推断提取的以太币。此外，将交易深度限制为三笔交易，并在执行过程中引入了额外的限制，以将内存复制操作的大小限制为256，从而模仿teEther的行为。

在实验中使用了一些机器：大学内部云中的20个虚拟机，运行6个2.5 Ghz虚拟化内核，每个内核分配12 GB内存。此外，在两台服务器上运行了12个ETHBMC实例，每个实例均配备了Intel Xeon E5-2667和96GB内存。扫描2,193,697个唯一帐户占用了整个群集大约3.5个月的时间，大约相当于39个CPU年。

本研究联系了teEther的作者，获得了他们的实验数据，并在同一日期（2017年11月30日）对他们的数据集列出的所有784,344个账户进行了分析。注意，在分析过程中，Krupp和Rossow首先假定了一个空的存储空间。这与仅单个合约分析结合在一起，使他们可以跳过对重复合约代码的分析，从而减少了38,757个合约的初始分析集。他们首先分析了此减少的合约集的漏洞。当他们的工具将某个帐户标记为易受攻击时，他们便在更大的集合中搜索了共享此合约代码的所有计数。随后，他们将重新对这些帐户进行分析，同时还提取相应的环境（例如，这些帐户的存储变量）。但是，请注意，此快捷方式可能会错过易受攻击的合约，因为它们可能会根据初始化的存储变量和与之交互的帐户而有所不同。为避免这种情况，分别扫描所有784,344个帐户，提取初始存储变量以及分析期间发现的被调用帐户。想强调的是，两次扫描都针对同一套合约，本文只是在方法上有所不同。

分析成功完成了大部分合约（91.21％），只有很少的超时（2.41％）。相比之下，teEther成功分析了85.65％的合约。由于本文的分析具有大规模性质，因此在分析过程中确实遇到了多个错误（6.38％）。有些是由于EVM（一种用于验证的框架）中的错误导致的。一些与本研究有关，无法从区块链加载帐户，这是目前仍在调查的问题。但是，无论如何将相应的帐户标记为错误，从分析中将其排除在外。

经过两个阶段的分析，Krupp和Rossow报告了1,532个易受攻击的帐户。在分析中，发现了2,856个易受攻击的合约，可以从中提取以太的1,681个合约，可以重定向的51个控制流以及可以随时杀死的1,431个（即自杀合约）。请注意，一个帐户可以标记为多个类别，例如255个帐户都被标记为可以提取以太币的suicidaland。在评估过程中，teEtherauthors列出了容易受到劫持的控制流的帐户。一旦攻击者可以重定向控制流，他们就可以轻松地从帐户中提取所有资金。

当前的漏洞情况：最后一次扫描显示，截至2018年12月，以太坊区块链上共有4,301个易受攻击的活跃合约。分为2708个可提取以太币的合约，97个可重定向其控制流的账户和1924个合约可以随意破坏自己。

3）性能分析

本文展示了ETHBMC扩展到大型数据集的能力。但是，在分析单个合约时，也对它的性能感兴趣。从数据集中随机抽取了10,000个合约，并对本文分析时间进行了研究。请注意，如果合约与其他合约互动，仍将从区块链加载它们。结果如下图所示。

在这10,000个合约中，在前5秒成功分析了5,577个合约，并在5到10秒后成功分析了另外2,006个（即，在10秒内总计7,583个）。此后，已解决合约的数量逐渐增加，在前2分钟内解决了10,000个合约中的8,471个。 30分钟后，已成功分析了10,000个帐户中的9,031个，即90％左右，这反映了在大规模分析中的效果。请注意在图中一起绘制了错误和超时，以更好地表示。

 

0x07 Discusion

接下来讨论ETHBMC的基本假设和局限性。

环境模型：尽管环境模型很精确，但仍然必须对其施加一些限制。当执行与环境中其他帐户交互的指令（例如，BALANCE或CALL指令）时，仅将当前加载的环境中的帐户视为有效目标。否则，将不得不将以太坊生态系统中的每个账户视为有效目标。尽管可以简单地对整个执行过程进行符号化建模，但这也会带来一个弊端，即这种帐户群甚至永远不可能。因此，决定只考虑提供给环境或在实时分析中发现的帐户。另外，不为帐户创建建模。

限制条件：在评估过程中，必须对本文的框架施加一些限制，例如边界循环和设置时间限制。尽管其中一些限制无法完全取消，例如，总是必须对循环施加上限，但提高超时限制或循环计数可能会导致发现程序中更深处的错误。这同样适用于合约调用，即ETHBMC无法找到需要三个以上事务的错误。此外，目前仅为一个攻击者帐户建模。但是，由于使用智能合约对复杂的系统进行建模，因此实际上包括其他攻击者或用户帐户可能会导致发现交互，而只有在多方使用该合约时才会触发交互。请注意，由于ETHBMC已经支持完整的环境，因此具有以这种方式使用的功能。

扩展到其他漏洞：本文模型检查方法可以通过将新漏洞建模为约束来检测新的攻击媒介。此外，EthBMC可以用来为合约提供正式担保。分析师可以将合约的正确行为建模为约束系统。然后在标准模型检查过程中，将使用EthBMC来检查是否存在既可以达到的状态，又可以满足约束系统的条件。这些属性证明违反了正确的行为。可达性评估该状态在实践中是可行的。正确行为的约束系统是所有可行程序状态的子集，当发现此子集以外的状态（即取反）时（在实践中也是可行的），发现违反了此行为。

可扩展性：可以为可伸缩性做出类似的论点，再次以keccak为例。使用严格的编码方案对这些计算进行编码，由于增加了复杂性，因此需要更长的分析时间。如果简单地假设计算可以有任何结果，即过高地近似，这将使推理变得直截了当。在检查诸如MadMax之类的工具的分析时间时，可以证明这一点：尽管在第一分钟内解决了约80％的所有合约，但这些工具在前20秒中分析了约90％。在智能合约的正常开发周期中，开发人员可以快速迭代许多版本的合约，他们可以使用“更快”的工具。最后，在部署到区块链之前，可以使用ETHBMC进行最终的精确分析。

影响：对EthBMC可能产生的实际影响进行公正的评估非常困难。由于以太坊系统对外界完全透明，因此攻击者可以监控区块链并在账户中包含诱人数量的以太币时从账户中提取资金。因此，对发现的每个易受害帐户的最高记录值进行了分析，从而为本研究确定了潜在影响的上限。这样产生的最大影响约为155,000个以太坊。但是，EthBMC可以重新创建Parity hack。如果当时使用该工具，那么本可以提取超过370,000个以太坊。以2020年2月底的汇率计算，这分别相当于约4000万美元和8900万美元。

 

0x08 Conclusion

在本文中首先介绍了用于智能合约的最新静态分析工具。证明了所有这些工具都至少在一个类别中采用了不精确的推理。认识到这些缺陷后，介绍了ETHBMC，它是一种符号执行器，能够捕获合约间的关系，加密哈希函数和内存复制式操作。通过评估以前的几项工作的实施来证明了它的有效性，并表明ETHBMC的准确性明显优于它们。另外，介绍了当前合约前景的漏洞分析，以及对ETHBMC内部工作的多项研究。