原创 ETHIR: 以太坊字节码高层次分析框架，相关方法和工具

创建分布式一致性的方法已经产生了一系列用于构建复制事务日志(区块链)的分布式协议。这些技术进步使得分散加密货币的诞生成为可能，比如比特币。比特币最著名的实现之一Ethereum在复制分布式存储中加入了图灵(turing)技术——与基金相关的完整状态计算——即所谓的智能合约交易。

智能合约是存储在区块链中的小程序，可以由协议相关方发起的事务调用它们，并作为自动和可信的中介执行一些业务逻辑。智能合同的典型应用包括多方统计、投票和仲裁机制、拍卖以及带有奖励分配的解谜游戏的实现。为了保持区块链的全局一致性，涉及与智能合约交互的每个事务都在系统中进行复制。Ethereum,复制执行实现通过一个统一的执行后端Ethereum虚拟机(EVM)基于堆栈的操作形式,富含大量的原语,允许合同给对方,指全球区块链状态,启动sub-transactions,甚至创造新的合同动态实例。也就是说，EVM为实现基于以太符的智能合约的多种高级编程语言提供了一个方便的编译目标。与之前低层次的智能合约编写语言不同，在合约的生命周期，以太坊有一个可变的可修改的合约状态。最后，为了解决可能的拒绝服务攻击问题，EVM提出了gas的概念——虚拟机指令的成本字段。

所有这些特性使EVM与一个非常强大的执行形式,同时使它很难正式分析的字节码可能效率低下和漏洞的挑战加剧了智能的关键任务性质的合同,,被部署后,不能修改或采取区块链。

贡献。在这项工作中，我们进一步完善和自动化推理的高级属性的以太坊智能合同。

• 为此，我们提供了一个开源工具EthIR，用于将EVM字节码精确地反编译为基于规则的高级表示形式;EthIR可以通过GitHub访问：: https://github.com/costa-group/ethIR
• 我们的表示法从Oyente生成的CFGs中提供的低层编码为EVM字节码重构了高层控制和数据流。它允许应用为高级语言开发的最先进的分析工具来推断字节码的属性。
• 我们通过对来自区块链的现有合约进行自动资源分析来展示这个应用程序，从而推断它们的循环边界。

27.3从EVM到基于规则的表示

反编译作为其他字节码的目的语言(见,例如,gas分析和优化框架)是在传递一个明确表示程序的控制流标明的延续(通过规则执行)和数据流(通过显式变量,代表了数据存储在堆栈中,在合同领域,在局部变量,以及区块链),因此，分析或转换工具可以直接获得此控制流信息。

27.3.1扩展Oyente生成CFG

给定一些EVM代码，Oyente工具生成一组块，这些块存储表示此类EVM代码的CFG所需的信息。然而，当一个块的跳转地址不是惟一的(取决于程序的流)时，Oyente生成的块有时只存储跳转地址的最后一个值。我们修改了Oyente块的结构，以便包含所有可能的跳转地址，从而重构整个CFG。例如，图27-1显示了合约片段的可靠源代码(左)，以及从中生成的CFG(右)。观察到在Oyente CFG生成的扩展,说明SSTORE或SLOAD注释与合同领域他们操作的标识符(例如,SSTORE操作存储一个值在合同领域被SSTORE 0)。同样,EVM与指令MSTORE和MLOAD说明注释与他们操作的内存地址(地址将被转换成变量尽可能RBR)。如果内存地址不是静态已知的，就不能生成这些注释，在这种情况下，我们用“?”标注相应的指令。

图 27-1 solability代码(左)和EVM代码用于CFG中的process_payment(右)。

最后，当我们有了可靠的代码可用时，我们就能够从散列代码中检索调用的函数的名称(参见Block 152，其中我们在第二个字节码kingBlock中注释了要调用的函数的名称)。这允许我们静态地知道延续块。

27.3.2从CFG到保护规则

将EVM转换为基于规则的表示是通过将Def. 1中的转换应用于CFG中的每个块来完成的。给定给规则-block.x或jump_x-use x的标识符使用的是正在翻译的块中第一个字节码的PC 。我们区分三种情况1)如果最后一个字节码块无条件jump(JUMP),我们生成一个单一的规则,与延续调用块,(2)如果是条件转移(JUMPI)我们生产两个额外的保护规则代表了延续条件成立时,它不,(3)否则,我们继续执行块x + s (s是EVM的大小字节码的块被翻译)。关于变量，我们区分了以下类型。

1. 堆栈变量:转换的一个关键因素是将堆栈平铺成变量，即，当它被转换成规则时，块使用的堆栈部分由显式变量s0、s1……表示，其中s1在s0之上，以此类推。得到初始堆栈变量作为参数s0, s1，…， sn，记为。
2. 局部变量:代码中出现的以数字地址表示的本地内存的内容，通过给定地址的MSTORE和MLOAD访问，使用变量l0、l1、…， lr，表示为lr，并作为参数传递。对于转换，我们假设有一个表 lmap，它将不同的本地变量关联到代码中使用的每个数字地址内存。当地址不是数字时，我们使用规则的新变量local表示它，以表明我们没有关于此内存位置的信息。
3. 合约字段:我们用变量g0对字段建模……， gk，表示为gk，作为参数传递。由于这些字段是使用SSTORE访问的，而SLOAD使用的是字段的数量，所以我们将gi与第i字段关联起来。对于本地内存，如果字段的数量不是数字，因为它是未知的(注释为?)我们使用一个新的局部变量来表示它。
4. 区块链数据:我们用变量bc对该数据建模，这些变量要么用md0索引，要么…如果它们是调用的精确信息，比如使用操作码GAS访问的gas，或者是关于区块链的，比如使用操作码number访问的当前块号。所有这些数据都是通过专用的操作码访问的，这些操作码可能会消耗堆栈的一些偏移量，并通常将结果放在堆栈的顶部(尽管其中一些操作码，如CALLDATACOPY，可以在本地内存中存储信息)。

翻译使用一个辅助函数τ每个字节码翻译成相应的高层指令(和更新堆栈的大小m)和τG翻译条件转移的限制。将EVM翻译成的RBR语言的语法如图2所示。我们可以选择将原始字节码指令保存在RBR中，通过简单地将它们封装在nop方法(例如nop(DUPN))中，就可以从原始字节码指令中获得更高级的字节码指令。这与gas分析器将精确的gas消耗分配给转换字节码的高级指令有关。

定义 1. 给定一个带有b1指令的block B，…， bi在CFG中从PC x开始，与局部变量表 lmap，生成的规则是：

方法τ和τG对于一些代表性的字节码：

图27-2 用于翻译EVM的RBR语法

-c 是指令的索引，条件跳转的保护从该索引开始。注意，该条件在索引i-2处结束，并且总是在i-1处有一个PUSH。由于push地址(我们已经在p中有了)和条件的结果被JUMPI使用，所以我们不将它们存储在堆栈变量中。

• m 表示块的堆栈大小。一开始我们有m:= n。
• 变量gs1、gs2和gl、ls1、ls2和ll是每个规则的局部变量，用于表示SLOAD和SSTORE、MLOAD和MSTORE在给定地址不是具体数字时的使用情况。对于SLOAD和MLOAD，我们还使用fresh()来表示新变量的生成器，以安全地表示加载地址的未知值。

例 1. 。例如，通过翻译图27-1右侧的三个块获得的RBR摘录如下(所选指令始终使用nop注释获取它们的字节码)：

27.4案例研究:使用SACO所在EVM中进行边界循环

为了说明我们的框架的适用性，我们分析了EVM代码的数量特性，将其转换为我们的中间表示形式，并使用高级静态分析器SACO对其进行分析。中美合作所能够推断出循环迭代次数的上限。请注意，这是推断智能合同(一个非常有趣的属性)的gas消耗量的第一个关键步骤。SACO的内部表示匹配图27-2的语法在小的语法翻译之后(我们已经解决了实现github中可用的一个名为saco.py的简单翻译程序的问题)。由于SACO所没有位操作(即and、or、xor和not)，我们的翻译器用新的变量替换这些操作，以便分析器忘记关于位变量的信息。在此之后，对于我们的运行示例，我们证明了它包含的6个循环的终止，并为这些循环生成一个线性边界。我们在github中包含了其他智能合约，以及SACO所为它们推断的循环边界。其他高水平的分析程序，如整数转换系统或霍恩子句(如，AproVe, T2, VeryMax, co絮凝)的工作，可以很容易地适应，以及对我们的RBR翻译程序。

27.5相关方法和工具

在过去的两年中，有几种方法通过在最先进的证明助手中建模Ethereum的严格语义，解决了直接在EVM字节码中实现的关于Ethereum合约的完全形式推理的挑战。虽然这些机制支持EVM合约的各种安全性和安全性特性的正式机器辅助证明，但是它们都没有提供对EVM字节码进行完全自动化分析的方法。

同时，其他几种确保Ethereum合约正确性和安全性的方法采用了一种更激进的方法，通过象征性地执行EVM字节码来实现用于检测bug的自动化工具链。然而，低层EVM表示在应用这些工具立即分析更高层的属性时遇到了困难。例如，在Oyente中表示EVM，这是一个流行的分析Ethereum智能合约的工具，它的级别太低，无法实现对高级属性的分析，例如循环复杂度或交换性条件。宙斯，一个通过符号执行wrt分析以太智能合同的工具。客户提供的策略，直接操作可靠的来源。因此，宙斯作为一种分析方法的合理性，依赖于没有正式定义的Solidity语义。