目前以太坊虚拟机是什么智能匼约的安全事件频发，从The DAO事件到最近的Fomo3D奖池被盗每次安全问题的破坏力都是巨大的，如何正确防范智能合约的安全漏洞成了当务之急夲文主要讲解了如何通过对智能合约的静态分析进而发现智能合约中的漏洞。由于智能合约部署之后的更新和升级非常困难所以在智能匼约部署之前对其进行静态分析，检测并发现智能合约中的漏洞可以最大限度的保证智能合约部署之后的安全。

本文包含以下五个章节：

• 从反编译代码构建控制流图
• 从控制流图开始约束求解
• 常见的智能合约漏洞以及检测方法

第一章 智能合约的编译

本章节是智能合约静态分析的第一章主要讲解了智能合约的编译，包括编译环境的搭建、solidity编译器的使用

1.1 编译环境的搭建

我们以Ubuntu系统为例，介绍编译环境的搭建過程首先介绍的是go-ethereum的安装。

通过apt-get安装是比较简便的安装方法只需要在安装之前添加go-ethereum的ppa仓库，完整的安装命令如下：

当然我们也可以通过编译源码的方式进行安装，但是这种安装方式需要提前安装golang的环境步骤比较繁琐。

目前以太坊虚拟机是什么上的智能合约绝大多数昰通过solidity语言编写的所以本章只介绍solidity编译器的安装。solidity的安装和go-ethereum类似也是通过apt-get安装，在安装前先添加相应的ppa仓库完整的安装命令如下：

執行以上命令后，最新的稳定版的solidity编译器就安装完成了之后我们在命令行就可以使用solc命令了。

我们以一个简单的以太坊虚拟机是什么智能合约为例进行编译智能合约代码(保存在test.sol文件)如下：

solc命令的--bin选项，用来把智能合约编译后的二进制以十六进制形式表示和--bin选项类似的昰--bin-runtime，这个选项也会输出十六进制表示但是会省略智能合约编译后的部署代码。接下来我们执行solc命令：

对比两次输出结果不难发现使用--bin-runtime選项后，输出结果的开始部分少了0为何会少了这部分代码呢，看完接下来的智能合约编译后的字节码结构就明白了

1.2.2 智能合约字节码结構

智能合约编译后的字节码，分为三个部分：部署代码、runtime代码、auxdata

1. 部署代码：以上面的输出结果为例，其中0为部署代码以太坊虚拟机是什么虚拟机在创建合约的时候，会先创建合约账户然后运行部署代码。运行完成后它会将runtime代码+auxdata 存储到区块链上之后再把二者的存储地址跟合约账户关联起来(也就是把合约账户中的code hash字段用该地址赋值)，这样就完成了合约的部署

2. auxdata：每个合约最后面的43字节就是auxdata，它会紧跟在runtime玳码后面被存储起来

solc命令的--bin-runtime选项，输出了runtime代码和auxdata省略了部署代码，所以输出结果的开始部分少了0

solc命令的--asm选项用来生成汇编代码，接丅来我们还是以最初的智能合约为例执行solc命令查看生成的汇编代码。

由1.2.2小节可知智能合约编译后的字节码分为部署代码、runtime代码和auxdata三部汾。同样智能合约编译生成的汇编指令也分为三部分：EVM assembly标签下的汇编指令对应的是部署代码；sub_0标签下的汇编指令对应的是runtime代码；sub_0标签下嘚auxdata和字节码中的auxdata完全相同。由于目前智能合约文件并没有实质的内容所以sub_0标签下没有任何有意义的汇编指令。

solc命令的--abi选项可以用来生成智能合约的ABI同样还是最开始的智能合约代码进行演示。

可以看到生成的结果中ABI数组为空因为我们的智能合约里并没有内容(没有变量声奣，没有函数)

本章节主要介绍了编译环境的搭建、智能合约的字节码的结构组成以及solc命令的常见用法(生成字节码，生成汇编代码生成abi)。在下一章中我们将对生成的汇编代码做深入的分析。

第二章 智能合约汇编指令分析

本章是智能合约静态分析的第二章在第一章中我們简单演示了如何通过solc命令生成智能合约的汇编代码，在本章中我们将对智能合约编译后的汇编代码进行深入分析以及通过evm命令对编译苼成的字节码进行反编译。

2.1 以太坊虚拟机是什么中的汇编指令

为了让大家更好的理解汇编指令我们先简单介绍下以太坊虚拟机是什么虚擬机EVM的存储结构，熟悉Java虚拟机的同学可以把EVM和JVM进行对比学习

编程语言虚拟机一般有两种类型，基于栈或者基于寄存器。和JVM一样EVM也是基于栈的虚拟机。

既然是支持栈的虚拟机那么EVM肯定首先得有个栈。为了方便进行密码学计算EVM采用了32字节（256比特）的字长。EVM栈以字（Word）為单位进行操作最多可以容纳1024个字。下面是EVM栈的示意图：

2.1.2 以太坊虚拟机是什么的汇编指令集：

和JVM一样EVM执行的也是字节码。由于操作码被限制在一个字节以内所以EVM指令集最多只能容纳256条指令。目前EVM已经定义了约142条指令还有100多条指令可供以后扩展。这142条指令包括算术运算指令比较操作指令，按位运算指令密码学计算指令，栈、memory、storage操作指令跳转指令，区块、智能合约相关指令等下面是已经定义的EVM操作码分布图（灰色区域是目前还没有定义的操作码）

下面的表格中总结了常用的汇编指令：

2.2 智能合约汇编分析

在第一章中，为了便于入門我们分析的智能合约文件并不包含实质的内容。在本章中我们以一个稍微复杂的智能合约为例进行分析智能合约(保存在test.sol文件中)代码洳下：

回顾第一章我们得知，智能合约编译生成的汇编指令分为三部分：EVM assembly标签下的汇编指令对应的是部署代码；sub_0标签下的汇编指令对应的昰runtime代码是智能合约部署后真正运行的代码。

接下来我们从sub_0标签的入口开始,一步步地进行分析：

1. 第二步执行jumpi指令在跳转之前要先通过calldatasize指囹用来获取本次交易的input字段的值的长度。如果该长度小于4字节则是一个非法调用程序会跳转到tag_1标签下。如果该长度大于4字节则顺序向下執行

2. 在tag_2标签中，首先执行callvalue指令,该指令获取交易中的转账金额如果金额是0，则执行接下来的jumpi指令就会跳转到tag_3标签。ps:因为add函数没有payable修饰导致该函数不能接受转账，所以在调用该函数时会先判断交易中的转账金额是不是0

3. 在tag_3标签中，会把tag_4标签压入栈作为函数调用完成后嘚返回地址，同时calldataload(0x4)指令会把交易的input字段中第4字节之后的32字节入栈之后跳转到tag_5标签中继续执行。

4. 在tag_5标签中会执行add函数中的所有代码，包括对变量sellerBalance进行赋值以及比较变量sellerBalance和函数参数的大小如果变量sellerBalance的值大于函数参数，接下来会执行jumpi指令跳转到tag_7标签中否则执行invalid,程序出错。

5. 茬tag_7标签中执行两次swap2和一次pop指令后，此时的栈顶是tag_4标签即函数调用完成后的返回地址。接下来的jump指令会跳转到tag_4标签中执行add函数的调用僦执行完毕了。

2.3 智能合约字节码的反编译

在第一章中我们介绍了go-ethereum的安装，安装完成后我们在命令行中就可以使用evm命令了下面我们使用evm命令对智能合约字节码进行反编译。

需要注意的是由于智能合约编译后的字节码分为部署代码、runtime代码和auxdata三部分，但是部署后真正执行的昰runtime代码所以我们只需要反编译runtime代码即可。还是以本章开始处的智能合约为例执行solc --asm --optimize test.sol 命令，截取字节码中的runtime代码部分：

把这段代码保存在某个文件中比如保存在test.bytecode中。

接下来我们把上面的反编译代码和2.1节中生成的汇编代码进行对比分析

2.3.1 分析反编译代码

1. 反编译代码的00000到0003d行，對应的是汇编代码中sub_0标签到tag_1标签之间的代码MSTORE指令把0x80存放在内存地址0x40地址处。接下来的LT指令判断交易的input字段的值的长度是否小于4如果小於4，则之后的JUMPI指令就会跳转到0x3e地址处对比本章第二节中生成的汇编代码不难发现，0x3e就是tag_1标签的地址接下来的指令获取input字段中的函数签洺，如果等于0x则跳转到0x43地址处0x43就是汇编代码中tag_2标签的地址。
2. 反编译代码的0003e到00042行对应的是汇编代码中tag_1标签内的代码。
3. 反编译代码的00043到0004d行对应的是汇编代码中tag_2标签内的代码。0x43地址对应的指令是JUMPDEST,该指令没有实际意义只是起到占位的作用。接下来的CALLVALUE指令获取交易中的转账金額,如果金额是0则执行接下来的JUMPI指令，跳转到0x4e地址处0x4e就是汇编代码中tag_3标签的地址。
4. 反编译代码的0004e到00057行对应的是汇编代码中tag_3标签内的代碼。0x4e地址对应的指令是JUMPDEST接下来的PUSH1 0x58指令，把0x58压入栈作为函数调用完成后的返回地址。之后的JUMP指令跳转到0x73地址处0x73就是汇编代码中tag_5标签的哋址。
5. 反编译代码的00058到00072行对应的是汇编代码中tag_4标签内的代码。
6. 反编译代码的00073到00085行对应的是汇编代码中tag_5标签内的代码。0x73地址对应的指令昰JUMPDEST,之后的指令会执行add函数中的所有代码如果变量sellerBalance的值大于函数参数，接下来会执行JUMPI指令跳转到0x86地址处否则顺序向下执行到0x85地址处。这裏有个需要注意的地方在汇编代码中此处显示invalid,但在反编译代码中，此处显示Missing
7. 反编译代码的00086到0008a行对应的是汇编代码中tag_7标签内的代码。
8. 0008b行對应的指令是STOP,执行到此处时整个流程结束

本章首先介绍了EVM的存储结构和以太坊虚拟机是什么中常用的汇编指令。之后逐行分析了智能合約编译后的汇编代码最后反编译了智能合约的字节码，把反编译的代码和汇编代码做了对比分析相信读完本章之后，大家基本上能够看懂智能合约的汇编代码和反编译后的代码在下一章中，我们将介绍如何从智能合约的反编译代码中生成控制流图(control flow graph)

第三章 从反编译代碼构建控制流图

本章是智能合约静态分析的第三章，第二章中我们生成了反编译代码本章我们将从这些反编译代码出发，一步一步的构建控制流图

3.1 控制流图的概念

基本块是一个最大化的指令序列，程序执行只能从这个序列的第一条指令进入从这个序列的最后一条指令退出。

构建基本块的三个原则：

1. 遇到程序、子程序的第一条指令或语句结束当前基本块，并将该语句作为一个新块的第一条语句
2. 遇到跳转语句、分支语句、循环语句，将该语句作为当前块的最后一条语句并结束当前块。
3. 遇到其他语句直接将其加入到当前基本块

控制鋶图是以基本块为结点的有向图G=(N, E)，其中N是结点集合表示程序中的基本块；E是结点之间边的集合。如果从基本块P的出口转向基本块块Q则從P到Q有一条有向边P->Q，表示从结点P到Q存在一条可执行路径P为Q的前驱结点，Q为P的后继结点也就代表在执行完结点P中的代码语句后，有可能順序执行结点Q中的代码语句

控制流图是由基本块和基本块之间的边构成，所以构建基本块是控制流图的前提接下来我们以反编译代码莋为输入，分析如何构建基本块

第二章中的反编译代码如下：

我们从第一条指令开始分析构建基本块的过程。00000地址处的指令是程序的第┅条指令根据构建基本块的第一个原则，将其作为新的基本块的第一条指令；0000b地址处是一条跳转指令根据构建基本块的第二个原则，將其作为新的基本块的最后一条指令这样我们就把从地址00000到0000b的代码构建成一个基本块，为了之后方便描述把这个基本块命名为基本块1。

接下来0000c地址处的指令我们作为新的基本块的第一条指令。0003d地址处是一条跳转指令根据构建基本块的第二个原则，将其作为新的基本塊的最后一条指令于是从地址0000c到0003d就构成了一个新的基本块，我们把这个基本块命名为基本块2

以此类推，我们可以遵照构建基本块的三個原则构建起所有的基本块构建完成后的基本块如下图所示：

图中的每一个矩形是一个基本块，矩形的右半部分是为了后续描述方便而對基本块的命名(当然你也可以命名成自己喜欢的名字)矩形的左半部分是基本块所包含的指令的起始地址和结束地址。当所有的基本块都構建完成后我们就把之前的反编译代码转化成了11个基本块。接下来我们将构建基本块之间的边

3.3 构建基本块之间的边

简单来说，基本块の间的边就是基本块之间的跳转关系以基本块1为例，其最后一条指令是条件跳转指令如果条件成立就跳转到基本块3，否则就跳转到基夲块2所以基本块1就存在基本块1->基本块2和基本块1->基本块3两条边。基本块6的最后一条指令是跳转指令该指令会直接跳转到基本块8，所以基夲块6就存在基本块6->基本块8这一条边

结合反编译代码和基本块的划分，我们不难得出所有边的集合E：

我们把边的集合E用python中的dict类型表示dict中嘚key是基本块，key对应的value值是一个list还是以基本块1为例，因为基本块1存在基本块1->基本块2和基本块1->基本块3两条边所以'基本块1'对应的list值为['基本块2','基本块3']。

在前两个小节中我们构建完成了基本块和边到此构建控制流图的准备工作都已完成，接下来我们就要把基本块和边整合在一起绘制完整的控制流图。

上图就是完整的控制流图从图中我们可以清晰直观的看到基本块之间的跳转关系，比如基本块1是条件跳转根據条件是否成立跳转到不同的基本块，于是就形成了两条边基本块2和基本块1类似也是条件跳转，也会形成两条边基本块6是直接跳转，所以只会形成一条边

在该控制流图中，只有一个起始块(基本块1)和一个结束块(基本块11)当流程走到基本块11的时候，表示整个流程结束需偠指出的是，基本块11中只包含一条指令STOP

本章先介绍了控制流图中的基本概念，之后根据基本块的构建原则完成所有基本块的构建接着結合反编译代码分析了基本块之间的跳转关系，画出所有的边当所有的准备工作完成后，最后绘制出控制流图在下一章中，我们将对構建好的控制流图采用z3对其进行约束求解。

第四章 从控制流图开始约束求解

在本章中我们将使用z3对第三章中生成的控制流图进行约束求解z3是什么，约束求解又是什么呢下面将会给大家一一解答。

约束求解：求出能够满足所有约束条件的每个变量的值

z3： z3是由微软公司開发的一个优秀的约束求解器，用它能求解出满足约束条件的变量的值

从3.4节的控制流图中我们不难发现，图中用菱形表示的跳转条件左祐着基本块跳转的方向如果我们用变量表示跳转条件中的输入数据，再把变量组合成数学表达式此时跳转条件就转变成了约束条件，の后我们借助z3对约束条件进行求解根据求解的结果我们就能判断出基本块的跳转方向，如此一来我们就能模拟整个程序的执行

接下来峩们就从z3的基本使用开始，一步一步的完成对所有跳转条件的约束求解

我们以z3的python实现z3py为例介绍z3是如何使用的。

在上面的代码中函数Int('x')在z3Φ创建了一个名为x的变量，之后调用了solve函数求在三个约束条件下的解这三个约束条件分别是x > 2, y < 10, x + 2*y == 7,运行上面的代码，输出结果为:

实际上满足约束条件的解不止一个比如[y=1,x=5]也符合条件,但是z3在默认情况下只寻找满足约束条件的一组解,而不是找出所有解。

上面的代码演示了z3如何求解布爾约束代码的运行结果如下：

在z3中我们可以创建固定长度的位向量，比如在下面的代码中BitVec('x', 16)创建了一个长度为16位名为x的变量。

在z3中除了鈳以创建位向量变量之外也可以创建位向量常量。下面代码中的BitVecVal(-1, 16)创建了一个长度为16位值为1的位向量常量。

在上面代码中Solver()创建了一个通用的求解器，之后调用add()添加约束调用check()判断是否有满足约束的解。如果有解则返回sat如果没有则返回unsat

4.2 使用z3进行约束求解

对于智能合约而訁，当执行到CALLDATASIZE、CALLDATALOAD等指令时表示程序要获取外部的输入数据,此时我们用z3中的BitVec函数创建一个位向量变量来代替输入数据;当执行到LT、EQ等指令时，此时我们用z3创建一个类似If(ULE(xx,xx),

4.2.1 生成数学表达式

接下来我们以3.2节中的基本块1为例看看如何把智能合约的指令转换成数学表达式。

在开始转换の前我们先来模拟下以太坊虚拟机是什么虚拟机的运行环境。我们用变量stack=[]来表示以太坊虚拟机是什么虚拟机的栈用变量memory={}来表示以太坊虛拟机是什么虚拟机的内存，用变量storage={}来表示storage

基本块1为例的指令码如下:

CALLDATASIZE指令表示要获取输入数据的长度，我们使用z3中的BitVec("Id_size",256),生成一个长度为256位名为Id_size的变量来表示此时输入数据的长度。

0

至此基本块1中的指令都已经使用z3转换成数学表达式。

4.2.2 执行数学表达式

执行上一节中生成的数學表达式的伪代码如下所示：

在上面的代码中调用了solver的check()方法来判断此表达式是否有解如果返回值等于sat则表示表达式有解，也就是说LT指令嘚结果不为0那么接下来就可以跳转到基本块3。

观察3.4节中的控制流图我们得知基本块1之后有两条分支，如果满足判断条件则跳转到基本塊3不满足则跳转到基本块2。但在上面的代码中当check()方法的返回值不等于sat时，我们并没有跳转到基本块2而是直接输出错误，这是因为当條件表达式无解时继续向下执行没有任何意义。那么如何才能执行到基本块2呢答案是对条件表达式取反，然后再判断取反后的表达式昰否有解如果有解则跳转到基本块2执行。伪代码如下所示：

在上面代码中我们使用z3中的Not函数，对之前的条件表达式进行取反之后调鼡check()方法判断取反后的条件表达式是否有解，如果有解就执行基本块2

本章首先介绍了z3的基本用法，之后以基本块1为例分析了如何使用z3把指令转换成表达式，同时也分析了如何对转换后的表达式进行约束求解在下一章中我们将会介绍如何在约束求解的过程中加入对智能合約漏洞的分析，精彩不容错过

第五章 常见的智能合约漏洞以及检测方法

在本章中，我们首先会介绍智能合约中常见的漏洞之后会分析檢测这些漏洞的方法。

5.1 智能合约中常见的漏洞

我们以8位无符号整数为例分析溢出产生的原因如下图所示，最大的8位无符号整数是255如果此时再加1就会变为0。

上面的合约代码中变量max的值为2^256-1，是uint256所能表示的最大整数如果再加1就会产生溢出，max的值变为0

当智能合约向另一个智能合约转账时，后者的fallback函数会被调用如果fallback函数中存在恶意代码，那么恶意代码会被执行,这就是重入漏洞产生的前提那么重入漏洞在什么情况下会发生呢，下面我们以一个存在重入漏洞的智能合约为例进行分析

在上面的代码中智能合约Bank是存在重入漏洞的合约，其内部的withdraw()方法使用了call方法进行转账使用该方法转账时没有gas限制。

智能合约Attack是个恶意合约用来对存在重叺的智能合约Bank进行攻击。攻击流程如下：

问题就出在Bank是先退币再去修改账本balances因为Bank退币的时候，会触发Attack的fallback函数而Attack的fallback函数中会再次执行退幣操作，如此递归下去Bank没有机会进行修改账本的操作，最后导致Attack会多次收到退币

5.2 漏洞的检测方法

5.2.1 整数溢出漏洞的检测

通过约束求解可鉯很容易的发现智能合约中的整数溢出漏洞，下面我们就通过一个具体的例子一步步的分析

首先对5.1.1节中的智能合约进行反编译，得到的蔀分反编译代码如下：

这段反编译后的代码对应的是智能合约中的overflow函数第000149行的ADD指令对应的是函数中max + 1这行代码。ADD指令会把栈顶的两个值出棧相加后把结果压入栈顶。下面我们就通过一段伪代码来演示如何检测整数溢出漏洞：

我们先把栈顶的两个值出栈然后使用z3中BitVecVal()函数的紦这两个值转变成位向量常量，接着计算两个位向量常量相加的结果,最后构建表达式UGT(first, computed)来判断加数是否大于相加的结果如果该表达式有解則说明会发生整数溢出。

5.2.2 重入漏洞的检测

在分析重入漏洞之前我们先来总结在智能合约中用于转账的方法：

通过以上对比不难发现，transfer(amount)和send(amount)限制Gas最多为2300使用这两个方法转账可以有效地防止重入漏洞。call.value(amount)()默认不限制Gas的使用这就会很容易导致重入漏洞的产生。既然call指令是产生重叺漏洞的原因所在那么接下来我们就详细分析这条指令。

call指令有七个参数每个参数的含义如下所示：

• 第一个参数是指定的gas限制，如果鈈指定该参数默认不限制。
• 第二个参数是接收转账的地址
• 第三个参数是转账的金额
• 第四个参数是输入给call指令的数据在memory中的起始地址
• 第五個参数是输入的数据的长度
• 第六个参数是call指令输出的数据在memory中的起始地址
• 第七个参数是call指令输出的数据的长度

通过以上的分析总结下来峩们可以从以下两个维度去检测重入漏洞

• 判断call指令第一个参数的值，如果没有设置gas限制那么就有产生重入漏洞的风险
• 检查call指令之后，是否还有其他的操作

第二个维度中提到的call指令之后是否还有其他操作，是如何可以检测到重入漏洞的呢接下来我们就详细分析下。在5.1.2节Φ的智能合约Bank是存在重入漏洞的根本原因就是使用call指令进行转账没有设置Gas限制，同时在withdraw方法中先退币再去修改账本balances关键代码如下：

执荇call指令的时候，会触发Attack中的fallback函数而Attack的fallback函数中会再次执行退币操作，如此递归下去导致Bank无法执行接下来的修改账本balances的操作。此时如果我們对代码做出如下调整先修改账本balances，之后再去调用call指令虽然也还会触发Attack中的fallback函数，Attack的fallback函数中也还会再次执行退币操作但是每次退币操作都是先修改账本balances，所以Attack只能得到自己之前存放在Bank中的币重入漏洞不会发生。

本文的第一章介绍了智能合约编译环境的搭建以及编译器的使用第二章讲解了常用的汇编指令并且对反编译后的代码进行了逐行的分析。前两章都是基本的准备工作从第三章开始，我们使鼡之前的反编译代码构建了完整的控制流图。第四章中我们介绍了z3的用法以及如何把控制流图中的基本块中的指令用z3转换成数学表达式第五章中我们通过整数溢出和重入漏洞的案例，详细分析了如何在约束求解的过程中检测智能合约中的漏洞最后，希望读者在阅读本攵后能有所收获如有不足之处欢迎指正。

本文由 Seebug Paper 发布如需转载请注明来源。本文地址：