28.1引用

Neville Grech, Lexi Brent, Bernhard Scholz, and Yannis Smaragdakis. 2019. Gigahorse: Thorough, Declarative Decompilation of Smart Contracts. In International Conference on Software Engineering (ICSE)

28.2介绍

分布式区块链平台吸引了科学家和公众的注意。区块链技术为任何事务提供了分散的协商一致机制，在过去，这些事务都需要一个可信的集中权威。这一愿景最明显的体现之一是智能合约的开发:图灵完全自主的代理，运行在分布式区块链上，如Ethereum或Cardano。例如，一份明智的合同可以实现贷款政策、数字产品收费计划、拍卖、银行的全套业务，以及管理多方交易的几乎任何其他逻辑。Ethereum是最知名、最流行的区块链平台，支持全功能智能合约。(在撰写本文时，以太坊加密货币的市值为130亿美元。)Ethereum很好地展示了智能合同的潜力，以及它们的技术挑战。开发人员通常用一种称为Solidity的高级语言编写智能合约。

智能合同的开放性，以及它们在处理高价值货币方面的作用，都要求对合同进行彻底的分析和验证。然而，EVM字节码的底层基于堆栈的设计阻碍了这一任务，因为它几乎不像在其他语言(如Java s virtual machine)中那样具有任何抽象。例如，没有函数或调用的概念，编译器转换为EVM字节码需要创建自己的约定来实现堆栈上的本地调用。

最近的研究表明，重点是将智能合约解压缩为更高级别的表示，然后再应用任何进一步的(通常是面向安全的)分析。过去的反编译工作充其量是不完整的。最有名的反编译器(在很大程度上定义了当前的实践)是Porosity，在我们的研究中，在区块链上所有智能合约中，50%的已部署合约都没有产生这种结果。由于将EVM基于堆栈的操作转换为基于寄存器的中间表示的复杂任务，包括Vandal反编译器在内的即将到来的研究工具仍然无法反编译大部分实际合约(约12%)。

这些困难不仅仅是平台的技术特性或现有工具的特性。任何当前或未来的智能合约平台都可能使用低层虚拟机。这些虚拟机的设计针对智能合约的大规模复制执行进行了优化。字节码有效地表示为高效执行和紧凑程序表示而设计的汇编语言，因为字节码必须存储在区块链上。因此，用于智能合约的字节码永远不会是人类可读性或反向编译的最佳选择。

为了有效地反编译，需要对字节码进行重要的程序理解。反编译程序在将字节码重构为高级表示形式之前，需要深入的程序理解。例如，为了识别哪些低级跳转对应于高级函数调用，反编译器必须推断出跳转指令的可能地址，以便能够重构智能合约的控制流。这样的理解是复杂的:一旦调用被识别为调用(而不仅仅是过程内的跳转)，它的反编译精度可以进一步提高，方法是删除不可能的目标.

本文介绍了用于分析以太坊智能合约的Gigahorse工具链。Gigahorse解决了上述挑战，做出了以下贡献:

· 它提供了一种高效的反编译器，比最先进的反编译器具有更高的精度和完整性(例如，在Ethereum区块链上反编译几乎所有现有的合同)。

· Gigahorse为其提供了一个功能齐全的工具套件，提供了用于建筑分析的库，以及用于现有分析的现成客户端。

· Gigahorse方法提供了新的反编译见解(可能对更多平台有价值):当发现更高级别的程序特性时，它们会反馈给更低级别的分析。例如，通过发现函数，可以在本地(更精确地)执行堆栈分析，并总结函数调用对堆栈的影响，从而实现更精确和更可伸缩的分析。

· Gigahorse展示了一种非传统的反编译方法，它支持上述优点:反编译器是使用基于逻辑的(Datalog)规则以声明的方式指定的。

· Gigahorse的评估和它的功能说明了整套智能合同的以太坊区块链。

Gigahorse正在为正在进行的免费合同图书馆服务(https://contrt-library.com)提供支持，该服务在Ethereum区块链上提供所有合同的解压缩版本。合同图书馆对Ethereum安全分析师来说是一项很有价值的服务，目前每天接待数十位独立访问者和超过1000次的页面浏览量。

28.3背景

接下来，我们将介绍EVM字节码语言和声明性静态分析的一些背景知识。

28.3.1 Ethereum区块链中的低层面字节码

EVM是一种基于堆栈的低级中间表示(IR)。在智能合约的字节码形式中，符号信息已被数字常量所取代，函数在指令的海洋中被融合在一起，控制流被从堆栈中弹出的跳转地址所混淆。为了突出这个问题，将EVM字节码语言与最著名的字节码(Java (JVM)字节码和更高级别的IR)进行比较是很有意义的。这些差异包括：

· 与JVM字节码不同，EVM没有结构或对象的概念，也没有方法的概念。

· Java字节码有一个丰富的类型系统，EVM字节码只有一个类型:一个256位的单词。

· 在JVM字节码中，堆栈深度在不同的控制流路径下是固定的:执行不能到达具有不同堆栈大小的相同程序点。在EVM字节码中，不存在这样的执行约束，这使得标准控制流构造的识别非常困难。

· 所有控制流的边(即，jump)是变量，而不是常量。跳转的目标是从堆栈中读取的值。因此，即使要确定基本块的连接性，也需要进行值流分析。相反，JVM字节码为每次跳转都有一组明确定义的目标，与值流无关。

· JVM字节码定义了方法调用和返回指令。在EVM字节码中，虽然可以解析对智能合约外部的调用，但是合约内部的函数调用只转换为跳转(根据上面的一点，转换到可变的目的地)。合约的所有功能都融合在一个指令流中，使用低级跳转作为传输控制的手段。

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

28.3.2声明式程序分析

我们的工作基于声明性静态程序分析，应用于智能合约反编译。声明性是指将分析实现为逻辑规则的集合(即(例如，简单的含义)，这将导致推理，进而触发更多的规则推理，直到最小的固定点。Datalog语言是声明性分析方法的最标准载体，包括低级的和高级的。此外，Datalogstyle推理规则已经用于正式的规范任务中，比如Java VM验证器的官方规范。

Datalog与其说是一种编程语言，不如说是一种规范语言，因为计算基于两种结构:逻辑隐含规则和递归。Datalog规则C(z,x) <- A(x,y)， B(y,z)。这意味着如果A(x,y)和B(y,z)都为真，对于某些值x,y,z，那么可以推断出C(z,x)。从语法上讲，左箭头符号(<-)是一个逻辑蕴涵符号，它将推断出的事实(即，规则头)从以前确立的事实(即。，即规则的主体)。

递归是用Datalog表示计算的标准工具。静态分析任务通常是递归的，由多个子算法协作实现一个表示程序语义的联合目标。这些子算法没有明确的步进顺序，而是在一个大的递归定义中引用(yetincomplete)其他子算法的结果。通过这种方式，子算法互相增强结果，彼此受益。

Datalog语言的声明性意味着规则的任何触发顺序和规则s主体的任何计算顺序都将产生相同的最终结果。为了维护这个属性，Datalog中的含义必须严格单调:每个规则的触发只能引入新的事实，而不能妨碍前面的任何推断。

Datalog语言的部分吸引力在于，它目前拥有包括Souffle在内的几个高性能实现。除了高性能计算之外，最新的Datalog引擎还提供了对语言表达性的扩展:可以展示纯粹的声明并引入排序，还可以通过构造函数创建新的值。我们将在技术演示中显式地引用这些非纯声明性工具。

28.4GIGAHORSE编辑规范

在本节中，我们将介绍Gigahorse反编译器的核心构建块。我们使用Datalog作为反编译器的规范语言。Datalog规则被简化了，但在实际的Gigahorse实现中保留了其对应规则的基本复杂性。我们试图在不牺牲本文可读性和可理解性的前提下提供尽可能多的技术细节。在这方面，阐述将是不平衡的:我们在前几个小节中给出了深入的细节，在后面的部分(第三和第四节)中省略了技术细节，这样读者就可以填补空白。

28.4.1反编译步骤概述

接下来，我们将总结Gigahorse反编译器执行的主要反编译操作。为了便于说明，我们描述了一个概念性的逐步过程，即使反编译器规范是声明性的，并且没有显式的操作顺序。从最初的字节码开始，Gigahorse反编译器：

1) 找到基本块边界。下一步的输出是原始字节码，由基本块分割

2) 对基本块的堆栈效果进行局部分析。下一步的输入附加到字节码，每个块对应的堆栈效果摘要。

3) 使用动态控制流图(CFG)结构执行对整个合约上下文和流敏感的数据流分析。此信息用于生成具有全局寄存器的3地址IR。我们将此IR称为global-3-address IR。

4) 启发式地推断函数边界(例如。、进入和退出块，以及函数调用)用于公共函数和私有函数。函数边界允许反编译器将全局CFG转换为本地CFG和调用图。

5) 为所有函数推断函数参数并返回参数，为这些函数引入新变量，并执行过程内流敏感分析来推断这些新变量的流。输出形式是一个函数式的3地址IR，即，所有变量都是局部变量，作用域为。数据通过形式参数、返回参数或外部结构(如存储和内存)传递给函数。

以上所有步骤协同工作，从原始字节码派生高级表示。在本节中，我们将重点介绍步骤2和步骤3，并假设输入已经被解析为基本块中的语句(步骤1)。

原始字节码和我们的两个IRs(全局3地址IR和功能3地址IR)有共同的元素，但在重要方面也有所不同。在对这些的描述中，我们将覆盖某些概念，例如语句或变量。例如，全局3地址IR中的变量是全局变量，而对于函数3地址IR，它们都是局部变量。这两者之间的区别应该从上下文看得很清楚。

图28-1 我们的域，表示原始字节码的输入关系，计算关系和输出。输入关系编码程序指令和其他环境信息。

28.4.2输入语言

图28-1描述了输入和主要中间关系的模式，以及这个抽象级别上程序表示的域。堆栈索引I的定义在0到1023之间，我们假设对I的所有算术运算都只定义在这个范围内(即，没有溢位或溢位)。注意，原始字节码关系(如PUSH或BINOP)不引用变量，因为EVM是基于堆栈的机器。捕获指令的关系引用唯一的语句标识符。PUSH指令将一个常量推到堆栈的顶部(从0开始)，BINOP操作表示从堆栈中取出前两个操作数并将结果返回到堆栈中的任何二进制操作。由于表示原因，省略了二进制操作的特定形式，但是示例包括ADD、MUL、SHA等。

跳转最快的操作是no-op，它只将语句标识符标记为要跳转到的有效地址。JUMPI指令是一个条件跳转，如果堆栈位置1的元素不为零，则跳转到堆栈最顶层元素的地址。输入关系NEXT按程序顺序返回给定语句标识符的下一个语句标识符。关系块将语句映射到它的块，而BLOCKHEAD和BLOCKTAIL表示块的head和tail语句。最后，输入关系PUSHANDPOPS返回语句或整个块所推送和弹出的堆栈元素的最大数量。更准确地说，对于基本块，这是一个高/低水印的计算:在块中的所有点上，推入元素的平衡减去在程序点上弹出的元素的平衡的最大值和负最小值。

28.4.3本地栈分析

图28-1的底部部分显示了反编译的第2步推断的关系:本地堆栈分析。引入变量的概念(因为在输入表示中不存在变量)，并执行第一个值分析，在每个语句中计算执行堆栈内容的静态抽象。

如果语句推送堆栈上的新元素，则关系LOCALDEFINES将语句与新引入的变量连接起来。关系LOCALSTACKIN和LOCALSTACKOUT分别为每个堆栈位置在执行每个语句之前和之后包含的变量(或堆栈别名)建模。例如，LOCALSTACKOUT(stmt, index, v)表示在语句stmt中，堆栈位置索引包含与变量v相同的值(前面的一些语句刚刚引入)。这些关系的域包括变量和堆栈别名(vi)。，当前基本块推入值范围之外的堆栈索引)是指在基本块开始之前存在于给定堆栈位置的值。这是因为每个基本块都是单独分析的，堆栈值也可以从一个块传递到另一个块。前面定义的输入关系PUSHANDPOP给出了可能的堆栈别名的最大数量。

最后，关系VARIABLEVALUE将一些变量映射到程序常量。任何不存在于此关系中的变量都被认为是动态计算的，其值不在此形式化过程中建模(尽管我们在完整实现中对一些动态操作进行了部分建模)。

描述本地堆栈分析的规则如图28-2所示。LOCALDEFINE的计算通过构造函数NEWFRESHVAR引入了新的变量(每个需要它的语句一个)，后面的部分也使用了这个构造函数。这个构造函数通常被定义为保留传递给它的所有信息。

关系LOCALSTACKIN和LOCALSTACKOUT的计算比较复杂，它们之间的关系是相互递归的。(作为惯例，规则用作通配符，即，它表示任何被忽略的元素。)这两种关系都有简单的基本用例:对于LOCALSTACKOUT，如果一条语句分配了一个新的变量，那么堆栈位置0将保存该变量的值。对于LOCALSTACKIN，如果语句是基本块中的第一个语句，那么可以访问的所有堆栈位置都包含堆栈别名(即，它们的内容仅由适当的堆栈索引表示，而不是由新变量表示)。

LOCALSTACKOUT的递归规则对LOCALSTACKIN适用:在DUP中，指令之后栈顶的值与指令之前栈顶的值相同。在所有指令中，堆栈中未更改的内容将在索引处传播，索引根据指令执行的push和pop进行调整。类似地，LOCALSTACKIN的递归规则仅在相同的基本块中传播前一条语句的所有值。

上面的公式很好地说明了Gigahorse反编译器中的声明式方法。检查规则及其表面上的简单性，甚至很难让自己相信它们计算出了一些有用的东西。然而，它们可以在EVM执行堆栈的每个位置上精确地捕获常量值的完整流。公式小心地将新引入的变量的概念与堆栈位置的值的概念混合起来。新的变量对于反编译成3个地址的表示都是必不可少的，它们可以作为名称来简洁地表示值。

图28-2 在每个基本块中执行局部分析的关系

有了堆栈位置内容的模型，反编译器现在可以计算跳转指令的目标(因为这些值是从堆栈中获得的)。全局堆栈分析和控制流图(CFG)构造是分析中计算量最大的部分之一。我们在图28-3(顶部)和它们的定义(底部)中引入了额外的关系。

关系BLOCKIN和BLOCKOUT是LOCALSTACKIN和LOCALSTACKOUT的全局等价，通过根据GLOBALCFG定义的CFG相互传输值来计算。计算GLOBALCFG是这个分析步骤的主要部分。在基本块的第一个语句(由BLOCKHEAD给出)和它的任何前一个语句之间存在一个平凡的CFG边界(反向)。更有趣的是，在任何条件跳转指令(JUMPI)和任何基本块地址(即(常数值)由变量持有，该变量用于表示程序中的跳转目标。这使得CFG构造与全局流分析相互递归，就像使用最先进的框架对具有虚拟调用的高阶语言(如Java)进行程序分析一样。此分析的最终输出嵌入到关系GLOBALCFG和LOCALUSES中。后一个关系表示哪个变量流向哪个语句，其顺序与原始EVM堆栈中的顺序相同。该关系通过解析堆栈别名，有效地连接了基本块之间的值流。这再次很好地展示了声明性规范的紧凑性和强大功能。

图28-3 描述全局堆栈分析和动态控制流图构造的规则。

执行这些分析之后，我们现在可以使用图28-4中列出的模式和规则生成全局3-address代码。这种表示形式采用了Vandal反编译器。在这一点上转换到3地址IR是很简单的。语法糖和次要的细节省略用于表示目的。对元变量使用[和]和隐式非引号引用语言语法。例如，s:[to:= BINOP(x, y)]表示语句s是对x和y的二进制操作，其结果是to，其中x、y和to是引用字节码变量的元变量。分析程序中的变量和分析中的元变量之间的区别从上下文来看是很明显的，因此我们只引用变量。只要有意义，我们就重用来自原始字节码的指令操作码。不定义任何新变量或执行计算的指令(如DUP或JUMPDEST)不在此表示中。每当我们引用语句或它们的标识符S时，我们将引用3地址IR表示中的语句。

图28-4 计算全局3地址IR的规则和关系，是一种重要的中间反编译表示。

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

28.5 重构源函数

Gigahorse反编译的一个基本元素是函数的推理，这些函数在编译为EVM字节码时已经被分解。我们发现这个推理过程与上一节的CFG推理进入了一个良性循环:CFG推理通知函数重构，函数产生更精确的CFG推理。

28.5.1public函数

当前的EVM版本没有函数的概念(调用堆栈将在将来的版本中引入)。但是，所有向下编译到EVM的编程语言都支持函数。ABI(应用程序二进制接口)和EVM引入了公共函数的概念，因此外部合约或用户可以通过指定函数签名的散列来调用公共函数。通过识别由可靠编译器引入的调度模式，Gigahorse反编译器可以找到代码中的所有公共函数项。例如，让我们看看以下简化的全局3地址IR。

我们可以看到有两个公共函数，一个函数描述符0x6fdde03从地址0x139开始，另一个函数描述符0x95ea7b3从地址0x1b4开始。由于ABI是标准的，所以我们希望所有编译器的所有调度模式都能得到满足。对于任何反编译器来说，这种匹配都非常简单。

Gigahorse添加的唯一附加功能是表示上的便利:Gigahorse尝试将函数描述符(如0x95ea7b3)与源级函数签名(如approve(address,uint256))匹配。这可以通过查询现有数据库来实现公共函数签名。这允许在已部署的合约中检测超过三分之二的公共函数的源签名。

28.5.2搜索返回的函数

重构函数的挑战与私有函数有关，私有函数几乎从编译后的代码中消失了。为了检测私有函数，Gigahorse使用了复杂的启发式方法，这需要完整的全局数据流信息传播和CFGs的构建。第一个启发是寻找在堆栈上跨程序传递地址的特定实例，当这些地址随后在运行一个函数后用于进一步跳转时。例如，让我们看看以下简化的全局3地址IR.

这个程序片段首先传递返回地址，然后跳转到。在的末尾，它跳转回之前传递的返回地址。这个函数搜索启发式，因此必须识别(a)一个基本块(返回)跳转到一个有效的非本地派生的地址，该地址(b)起源于可以到达返回基本块的另一个块(调用者)。该启发式被压缩到一个关系中，该关系被进一步细化为FNCALLRET:

· 确保基本块只能属于一个函数。当出现冲突时，我们根据所选函数的总顺序确定选择一个函数。

· 确保只能通过函数调用输入函数。

28.5.3进一步分解函数

在EVM上下文中，检测返回给调用方的函数是不够的。终止(例如halt)函数在智能合约中非常常见，因为智能合约计算通常比较短。因此，Gigahorse使用额外的逻辑来检测不返回的函数。其主要思想是，如果一个基本块可以从两个(或多个)以前确定的不同函数中访问，那么它就位于一个独立的函数中。这是一个直觉上不可避免的规则:如果两个函数都使用相同的代码，那么这个代码也必须被分解成一个可重用的片段，即。,一个函数。(注意，与第IV-B节的技术不同，这种方法只检测调用了多次的源级函数，而只调用了一次的函数内联了一次，并且没有丢失精度。)

更详细地说，检测逻辑标识了通过以下路径可到达的基本块:(a)从两个或多个函数条目开始(例如，对应于先前标识的函数A和B)，其中(b)每个路径都保留在其源函数(分别为A和B)中。这个过程实际上是递归的，当发现更多的函数时，就会出现更多的机会来访问一些基本块。更多的功能。虽然所发现的函数数量是单调增长的，但是逻辑在Datalog语法级别上不是单调的:为了严格描述在单个函数中发生的路径，逻辑需要表示一条路径没有交叉到另一个函数中，即，使用调用图边缘谓词的否定，该谓词的内容在相同的计算中也在增长。由于这个原因，我们在(单调的)Datalog规则之外使用了一个定点循环，这样我们就能够在每一步迭代地重新计算关系，并且每个关系都可以引用前面迭代中的版本。(在实现中，这是通过Gigahorse使用的Souffle Datalog引擎的标准组件设施来实现的。)

完整的算法如图5所示。输入关系PUBLICFUNCTIONCALL按IV-A节的描述派生，而FNCALLRET按IV-B节的描述派生。从这两个关系我们计算我们的算法的输入，即。， CALLGRAPH0和FUNCTIONENTRY0。然后，算法继续在每次迭代中发现新函数(FUNCTIONENTRYn和CALLGRAPHn)，每次都重新计算从函数条目(REACHFROMn)可访问的路径。

计算函数入口上的最小不动点后，即，没有新的函数被发现，我们可以继续计算本地CFGs和调用图。调用图的计算方法是将一个集合放在所有CALLGRAPHn上。对于FUNCTIONENTRY，我们也假设相同。然后计算本地CFGs如下:

也就是说，如果先前推断的CFG边与函数抽象不一致，函数推理可以帮助过滤掉这些边。这种假边的产生是由于任何静态分析固有的不精确性。在我们的规则中，这种不精确性主要出现在控制流连接点，即，因为一个基本块的多个前身将其堆栈内容搞混了，基于图3的逻辑。

28.5.4推断函数参数和局部变量

推断函数边界和本地CFGs对客户端分析非常有益。不仅本地CFGs更精确(如前所述)，而且功能级别的推理支持基于摘要的分析(通常具有很高的可伸缩性和高精度)。为了支持基于摘要的数据流分析，我们需要有局部变量，并最小化全局变量的数量。

图28-5 进一步分解函数的启发式。

Gigahorse通过计算整个函数在执行过程中从堆栈中弹出的调用方提供的元素的数量来推断函数参数的数量。类似地，函数返回参数的数量是通过计算推入调用指令的额外元素(推入和不弹出)的余额来推断的。不幸的是，EVM不能保证堆栈深度在每个程序点都是静态已知的(不像Java VM)。一个很好的实用解决方案是沿着函数的执行路径推断所有可能的push和pop平衡，直到一个有限的上界，并在返回基本块的末尾取这些平衡的最小值。这是一种启发式策略，实验验证了其有效性。

在推断了函数参数和返回值的数量之后，Gigahorse继续使用NEWFRESHVAR构造函数为它们创建新的变量。由于空间原因，这个逻辑被省略了。

最后一个分析步骤是推断(非参数)局部变量和这些变量流向的位置。这是一种类似于在III- D小节检测函数之前引入变量的计算。

分析的主要输出是predicate FUNCTIONALUSES(s: s, i: i, v: v)，对于每个语句，它表示使用了哪些局部变量，以及使用的顺序。使用这个关系，我们可以生成最终的功能3地址IR，类似于图28-4中描述的过程。此时，我们还可以引入附加的操作码PRIVATECALL和PRIVATERETURN，它们替代调用函数或从函数返回的跳转指令。

28.6实现与讨论

前面几节的规范抓住了Gigahorse实现的本质。反编译器的实际Datalog规范有更多的技术细节，包括几百条逻辑规则(超过3K行Datalog，使用Souffle作为执行引擎)和一个小型Python脚手架(大约1K行)，这些规则是从Vanda借来的。与规范相比，完整的实现包含:

· 处理EVM的完整指令集，而不是所提供的最小指令集;

· 还有一些反编译启发式，它们是第三和第四节中讨论的启发式的次要补充

· 贯穿规则的上下文敏感性:概念(如CALLGRAPH)的元素由上下文限定，这允许更精确的静态分析。(我们使用1-call-site上下文，即1-CFA作为默认值。)

· 方便进一步分析客户资料的库;

· 示例客户端。

接下来，我们将更详细地讨论上面的一些内容。

A. 部署

Gigahorse已应用于Ethereum区块链的所有内容，其反编译结果作为免费的合约库服务(https://contract-library)提供。com)。合约图书馆得到了以太坊社区非常积极的回应。

B. 输出和客户端分析

Gigahorse以结构化的形式(即，表，导出为CSV文件)和打印精美的文本。下面的一个非常简单的合约有助于说明这一点。

Gigahorse总共推断出四个函数，其中两个是具有高级函数名称的公共函数。还推断了一个私有函数f0x57。所有低级跳转都已转换为高级控制流和调用/返回。在原始合约字节码中的跳转指令中，只有与return语句对应的跳转指令是多态的.因为它可以返回给两个调用者。Gigahorse可以很容易地检测到这是一个正确的返回函数，它支持更精确的数据流。我们评估集中的其他反编译器，，Vandal和EthIR，没有找到私有函数和调用返回模式。

Gigahorse被设计成一个框架，用于在其高级功能3地址IR的基础上编写与安全相关的分析。为了促进这些客户分析的开发，Gigahorse提供了额外的开发工具。对于在Datalog中实现的客户机分析，我们开发了一个批量分析器，它可以提供用户定义的客户机分析管道。它们是与反编译并行编译和执行的。Gigahorse的客户端分析可以用任何语言编写，方法是读取CSV文件的反编译结果。事实上，我们的客户端分析之一是一个高级的漂亮打印机，它接受反编译器的输出并输出高级的类实体代码，包括函数签名、控制流结构(如if语句)、一些类型和复杂表达式。这是人类检查智能合约的一个有用工具。

此外，Gigahorse还为反编译结果提供了Datalog API，以及针对反编译器输出进行了调优的分析函数库。这些库执行数据流、依赖关系和循环语义分析。数据流分析库能够计算过程内数据流分析或基于摘要的过程间数据流分析。后者是通过前一节描述的功能丰富的反编译实现的。所有的分析都是高度参数化的。用户可以实例化多个版本，每个版本定义自己的传递函数，还可以限制分析的范围(例如，只分析循环内的循环归纳变量)。循环语义分析确定循环和其他控制流结构、它们的退出条件、归纳变量、控制符等。使用所提供的库，我们已经将最近发布的针对与天然气相关的漏洞的MadMax客户端分析移植到Gigahorse反编译器中，得到了类似的结果，但性能更高，并且适用于99.9%以上已部署的智能合同。MadMax的重新实现只包含250行代码，展示了Gigahorse客户端分析基础设施的强大功能。

C. 声明和单调性

Gigahorse的声明性本质是其反编译效率的一个重要推动者。(从理论上说，这一见解可能也适用于其他反编译领域，比如机器码反编译。)逻辑规则允许反编译模式和启发式的简洁表达。也许更重要的是，可以完全独立地指定单独的模式，不需要排序或其他人工依赖。尽管如此，独立的模式可以相互受益，也可以相互补充。反编译模式之间的依赖关系(例如，一个模式需要在另一个模式之前运行)由执行引擎自动确定。反编译模式之间的依赖关系自然出现在我们在前面部分中看到的规范中，例如，调用图通知流分析，反之亦然。我们还看到了一个具有代表性的互补例子在第四部分:一种模式通过跟踪函数被调用并返回到它们的调用站点来检测函数)，而另一种模式检测一个块必须位于一个单独的函数中，因为它可以被两个现有的函数访问。两种模式都不如另一种更完整或更精确。

28.7评估

我们的实验打算回答几个研究问题: RQ1:可扩展性——Gigahorse是一个可伸缩且高效的反编译程序吗? RQ2:完整性/覆盖—反编译代码在多大程度上覆盖了在野外可用的原始代码? RQ3:精确度——反编译代码是否与高级语义完全匹配?

对于大多数研究问题，我们将把Gigahorse与Porosity(提交时最著名、最先进的Ethereum反编译器)和Vandal(最近的研究工具，可能是文献中最接近的可比工具)进行比较。在第VI-E节中，我们还使用关系不太密切的工具进行了一个实验。

我们的实验装置由以太坊区块链上截至2018年4月的所有可用程序组成。这构成了“野外合同”的宇宙集合，约660万份合同部署在91.8K个独特的程序中。

我们使用Intel Xeon E5-2687W v4 3.00GHz和512GB RAM在一台空闲机器上运行所有系统。为了限制(长)运行实验的时间，我们将反编译的截止时间设置为120秒。(如我们所示，对于所有系统，成功反编译合约的反编译时间平均比这个阈值低10倍以上。)任何需要更长时间进行反编译的合约都将被视为超时。所有的实验都是并行进行的。我们的机器有48个逻辑核心，所以我们并行运行45个进程。注意，Gigahorse反编译器还可以配置为在单个合约中实现反编译的parellelize，这是我们在批量分析多个合约时没有启用的选项。

我们强调，我们的评估是定量的，基于几个度量，但是我们通过对许多合约的手工检查确认，度量很好地反映了反编译的实际质量。

RQ1 可扩展性

为了回答这个问题，我们采用了以下指标: 超时/致命错误。，由于超时或致命错误而未能成功解压缩的合同的比例。

根据各自的反编译器检测到的与至少一个函数的合约。

时间即，反编译平均合约所用的时间，不包括超时的时间合约。

根据Gigahorse反编译器计算的功能数量来计算合同大小。

下表总结了前三个指标。(我们使用的惯例是斜体字越低越好，否则越高越好。)

图6 成功的反编译与不成功的反编译对合约大小的影响(函数数量)

Gigahorse速度非常快(比Vandal快4倍多，以获得更高的反编译质量)，并且可扩展到所有合同。Porosity和破坏者都未能对合同的大部分内容进行反编译。可以看出，Porosity是双峰的:对于它设法反编译的合约，或者遇到可伸缩性瓶颈，它的速度非常快。我们的设置给出了Porosity为其平均成功反编译时间(120秒)的100倍，但仍然不允许反编译超过一半的合同。没有正确解压缩的合约在大小上更大，对于Porosity和Vandal图6中的图6，解压缩成功与函数上的合约大小之间的关系(正如Gigahorse所报告的，它的函数推断是最可靠的)。

Gigahorse还拥有最高比例的合同，其中至少检测到一个函数(除了dispatcher函数)。拥有0个函数并不一定证明不完全反编译，但它是一个强有力的指标，特别是当Porosity和Vandal与Gigahorse的数字相背离时，Gigahorse的函数推断非常可靠。

RQ2 完备性

我们采用以下指标:未知的跳转目标，即，没有为非通断情况设定目标的跳转的比例。不可达的代码,即不可达的基本块。每个合约的功能数，由各自的反编译器表示。这些指标的结果如下表所示。

注意，Porosity的输出格式不支持测量不可达代码的跳转目标，因此我们只测量函数。Gigahorse为几乎所有的跳转指令找到跳转目标，这意味着比Vandal更少的代码是不可访问的。检测到的函数(公共函数或私有函数)的数量也要高得多。

RQ3 精确性

为了回答这个问题，我们采用了以下指标:

多态跳跃，为非穿透CFG边缘解析到多个目标的跳转的比例。

非结构化的循环,即具有特殊控制流量结构的回路比例。这表明控制流程图不精确。

具有相反出口条件的循环可能表示控制流图中的不精确。

在算术或赋值中，每个变量的数据流(值)。

在这种情况下，我们只比较Gigahorse和Vandal，因为Porosity无法测量这些指标。

Gigahorse在所有指标上的表现都更好。例如，它计算更少的多态跳转(即。，跳转多个可能的目标)，主要是因为在整个合约分析过程中更好的上下文敏感性。数据流和非结构化循环指标最能说明问题，接下来我们将在客户机分析上下文中讨论它们。

讨论:对客户分析的好处

RQ3显示，对于Gigahorse来说，在算术运算中流向变量的值的数量要少得多。这是由于多种因素造成的:基于摘要的分析、上下文敏感性和更精确的CFGs。数据流关系本身是反编译器的客户端，但它也适用于更高级别的客户端，比如漏洞检测分析。

循环检测也是Gigahorse工具链提供的客户端分析，我们可以看到在推断的CFGs中检测到的非结构化循环更少。由于在编写非结构化循环方面没有可靠的高级构造，所以我们期望一个高质量的CFG实际上没有非结构化循环(Gigahorse就是这种情况)。在这里，Gigahorse提供的上下文敏感性和本地CFGs直接转化为更高质量的客户端分析。

我们将最近的MadMax gas漏洞检测器(Vandal反编译器的主要客户端)移植到Gigahorse。Gigahorse几乎分析了所有的合同，而不是92%的故意破坏合同的案例。客户分析的性能也有利于额外的MadMax客户分析，平均每个合同只需要0.15s的挂钟时间。下表总结了MadMax在Vandal和Gigahorse下进行反编译时标记的漏洞。(对于这个表，默认情况下，数值越高越好，数值越低越好。)

尽管对于自由分析(无界迭代)，Gigahorse精度的提高会导致更低的数字，但是对于更奇特的漏洞模式，Gigahorse完整性的提高(能够分析更多的合同，在最大的可用合同中增加10%)会导致更多的警告。

敏感度分析

接下来，我们将讨论我们实验的几个不同维度，以及这如何影响结果。

a) 不同的Vandal设置:已发表的关于Vandal的工作声称成功反编译合同的比例更高:在我们的实验中为91.8%，而不是88.1%。这些数字很接近，差异是由于设置略有不同造成的。为了证实这一点，我们还尝试了另一种不同的汪达尔设置，以获得最大的反编译能力，并使其在更多的合约中获得成功94.7%，但代价是明显低于我们的实验的精度。

b) 其他研究反编译器:除了我们所比较的纯反编译器之外，其他一些最近的研究工具在进一步分析之前执行某种形式的反编译。我们没有尝试与这些工具进行全面的比较，而是在与RQ1相同的设置中对它们的端到端可伸缩性和通用性进行了更有限的实验。我们考虑了EthIR ， Mythril和Rattle。(其中，ETHIR是最接近纯反编译器的。)EthIR可以处理91K独特合同程序中的73%，每个合同的平均时间为11.9秒。大多数失败的合约都会产生错误状态退出。我们自己对基于规则的表示输出的检查证实，EthIR只在每个基本块中执行简单的本地推理。Mythril可以处理91K个唯一合同的40%，平均每个合同的时间为19.1秒;19%的合同退出时出现错误状态。另一方面，在相同的120秒超时时间内，Rattle可以处理91K中69.7%的惟一合约。它在24%的合约上产生非超时错误状态出口。

最近几个月，Eveem系统已经成为Ethereum区块链的反编译器。Eveem提供了一种方便的查询语言和高响应性，以获得积极的用户交互体验。Eveem基于符号执行引擎，与其他智能合约工具(如EthIR)非常相似。与静态分析相比，符号执行方法的完整性较差:它可能会遗漏代码的重要部分，因为没有找到可以执行它们的符号输入。(与此同时，符号执行对于它反编译的代码可能产生更高的精度。)最近的一件轶事说明了这种滞后。在2019年2月的电子讨论中(Security Community Telegram group, 2月10日)，提出了有多少部署的合同调用了3个区块链预编译函数的问题。Eveem给出了8000个答案，而Gigahorse则退回了4万多个合同，这显示出它的代码覆盖率要高得多

28.8相关工作

由于智能合同开发的高风险范式所固有的安全问题，对智能合同的分析和验证近年来受到了广泛的关注。

a) 智能合约的反编译器:Vandal是一个用Python编写的开源框架，由反编译器、区块链scraper和一组用Souffle Datalog编写的可扩展漏洞分析组成。我们在之前的章节中已经广泛地将Gigahorse与Vandal进行了比较。Porosity是用c++实现的从EVM字节码到类固态源(类似于我们的漂亮打印机输出)的高级反编译器。基于跟踪工具的以太字节码高级分析的EthIR框架。它的反编译输出引入了每个基本块的局部变量。使分析变得无关紧要。注意，EthIR框架从Oyente跟踪中重构了一些高级控制和数据流片段。控制流图中没有被Oyente跟踪覆盖的片段仍然没有被EthIR发现。Mythril是Ethereum智能合约的安全分析工具。Mythril在符号执行引擎(Laser-EVM)的帮助下执行反编译。它生成用于生成中间表示的跟踪，因此它与EthIR有类似的不完整性问题。同样，ratt也以SSA形式构建了一个IR，并对其进行程序分析。

b) 智能合约分析框架:以前关于智能合约安全性分析的工作可以根据其底层技术进行分类，包括符号执行、形式验证和抽象解释。有些工作并不一定需要反编译。系统包括Oyente、MAIAN、GASPER和Grossman等人最近的工作使用符号执行/跟踪语义方法。因此，它们只分析单个执行跟踪。Bhargavan等人的正式验证工具检测漏洞，包括不检查外部地址调用的返回值，以及使用F*重入。类似地，FSolidM框架检查可重入性和事务排序漏洞。它还可以检测编码模式，如以前的工作中概述的时间约束和授权问题。MAIAN framework发现了一些合约漏洞，包括无限期锁定资金、向任意用户泄漏资金以及扼杀智能合约。ZEUS系统对一组策略进行策略检查，包括重入、未选中的发送、失败的发送、整数溢出、事务状态依赖/顺序和块状态依赖。

c) Java字节码反编译:有大量的Java反编译器。Krakatoa反编译器使用转换管道从Java字节码恢复Java程序。Gigahorse使用类似的技术，通过符号执行将基于堆栈的操作转换为三个地址代码。Prolog用于指定Java字节码反编译器。一篇评估论文比较了各种Java反编译器的性能。

28.8结论

我们介绍了Gigahorse，一个用于反编译和分析Ethereum智能合约二进制文件的工具链。Gigahorse利用声明式程序分析来生成高效的反编译程序。由于不同抽象层之间存在反馈循环，反编译技术是独特的。我们还展示了Datalog非常适合在不牺牲性能的情况下简洁地描述这种机制。此外，Gigahorse工具链是一个包含高参数程序分析库和安全客户端分析的完整框架。

本文由南京大学软件学院2016级徐光耀翻译转述