Ethereum智能合约静态分析(上)

概述目前以太坊智能合约的安全事件频发从The DAO事件到最近的Fomo3D奖池被盗每次安全问题的破坏力都是巨大的如何正确防范智能合约的安全漏洞成了当务之急。本文主要讲解了如何通过对智能合约的静态分析进而发现智能合约中的漏洞。由于智能合约部署之后的更新和升级非常困难所以在智能合约部署之前对其进行静态分析检测并发现智能合约中的漏洞可以最大限度的保证智能合约部署之后的安全。本文包含以下五个章节:智能合约的编译智能合约汇编指令分析从反编译代码构建控制流图从控制流图开始约束求解常见的智能合约漏洞以及检测方法第一章 智能合约的编译本章节是智能合约静态分析的第一章主要讲解了智能合约的编译包括编译环境的搭建、solidity编译器的使用。1.1 编译环境的搭建我们以Ubuntu14.0系统为例介绍编译环境的搭建过程。首先介绍的是go-ethereum的安装。1.1.1 安装go-ethereum通过apt-get安装是比较简便的安装方法只需要在安装之前添加go-ethereum的ppa仓库完整的安装命令如下sudo apt-get install software-properties-common sudo add-apt-repository -y ppa:ethereum/ethereum sudo apt-get update sudo apt-get install ethereum安装成功后我们在命令行下就可以使用geth,evm,swarm,bootnode,rlpdump,abigen等命令。1.1.2 安装solidity编译器目前以太坊上的智能合约绝大多数是通过solidity语言编写的所以本章只介绍solidity编译器的安装。solidity的安装和go-ethereum类似也是通过apt-get安装在安装前先添加相应的ppa仓库。完整的安装命令如下sudo add-apt-repository ppa:ethereum/ethereum sudo apt-get update sudo apt-get install solc执行以上命令后最新的稳定版的solidity编译器就安装完成了。之后我们在命令行就可以使用solc命令了。1.2 solidity编译器的使用1.2.1 基本用法我们以一个简单的以太坊智能合约为例进行编译智能合约代码(保存在test.sol文件)如下pragma solidity0.4.220.6.0;contract Test{}执行solc命令solc --bin test.sol输出结果如下: test.sol:Test Binary:6080604052348015600f57600080fd5b50603e80601d6000396000f3fe6080604052600080fdfea265627a7a72315820dfcce7188335fc0675e145984734f0c2fdcec5d1c62290a9a63e8f3b58844d6764736f6c634300050b0032solc命令的--bin选项用来把智能合约编译后的二进制以十六进制形式表示。和--bin选项类似的是--bin-runtime这个选项也会输出十六进制表示但是会省略智能合约编译后的部署代码。接下来我们执行solc命令solc --bin-runtime test.sol test.sol:Test Binary of the runtime part:6080604052600080fdfea265627a7a72315820dfcce7188335fc0675e145984734f0c2fdcec5d1c62290a9a63e8f3b58844d6764736f6c634300050b0032对比两次输出结果不难发现使用--bin-runtime选项后输出结果的开始部分少了6080604052348015600f57600080fd5b50603e80601d6000396000f3fe为何会少了这部分代码呢看完接下来的智能合约编译后的字节码结构就明白了。1.2.2 智能合约字节码结构智能合约编译后的字节码分为三个部分部署代码、runtime代码、auxdata。部署代码以上面的输出结果为例其中6080604052348015600f57600080fd5b50603e80601d6000396000f3fe为部署代码。以太坊虚拟机在创建合约的时候会先创建合约账户然后运行部署代码。运行完成后它会将runtime代码auxdata 存储到区块链上。之后再把二者的存储地址跟合约账户关联起来(也就是把合约账户中的code hash字段用该地址赋值)这样就完成了合约的部署。runtime代码该例中6080604052600080fdfe是runtime代码。auxdata每个合约最后面的52字节就是auxdata它会紧跟在runtime代码后面被存储起来。solc命令的–bin-runtime选项输出了runtime代码和auxdata省略了部署代码所以输出结果的开始部分少了6080604052348015600f57600080fd5b50603e80601d6000396000f3fe。1.2.3 生成汇编代码solc命令的--asm选项用来生成汇编代码接下来我们还是以最初的智能合约为例执行solc命令查看生成的汇编代码。执行命令solc --bin --asm test.sol输出结果如下:(env) etherether-virtual-machine:~$ solc --bin --asm test.sol test.sol:Test EVM assembly: ... */ test.sol:36:56 contract Test { mstore(0x40, 0x80) callvalue /* --CODEGEN--:8:17 */ dup1 /* --CODEGEN--:5:7 */ iszero tag_1 jumpi /* --CODEGEN--:30:31 */ 0x00 /* --CODEGEN--:27:28 */ dup1 /* --CODEGEN--:20:32 */ revert /* --CODEGEN--:5:7 */ tag_1: ... */ test.sol:36:56 contract Test { pop dataSize(sub_0) dup1 dataOffset(sub_0) 0x00 codecopy 0x00 return stop sub_0: assembly { ... */ /* test.sol:36:56 contract Test { mstore(0x40, 0x80) 0x00 dup1 revert auxdata: 0xa265627a7a72315820dfcce7188335fc0675e145984734f0c2fdcec5d1c62290a9a63e8f3b58844d6764736f6c634300050b0032 } Binary: 6080604052348015600f57600080fd5b50603e80601d6000396000f3fe6080604052600080fdfea265627a7a72315820dfcce7188335fc0675e145984734f0c2fdcec5d1c62290a9a63e8f3b58844d6764736f6c634300050b0032由1.2.2小节可知智能合约编译后的字节码分为部署代码、runtime代码和auxdata三部分。同样智能合约编译生成的汇编指令也分为三部分EVM assembly标签下的汇编指令对应的是部署代码sub_0标签下的汇编指令对应的是runtime代码sub_0标签下的auxdata和字节码中的auxdata完全相同。由于目前智能合约文件并没有实质的内容所以sub_0标签下没有任何有意义的汇编指令。1.2.4 生成ABIsolc命令的--abi选项可以用来生成智能合约的ABI同样还是最开始的智能合约代码进行演示。执行solc命令solc --abi test.sol输出结果如下(env) etherether-virtual-machine:~$ solc --abi test.sol test.sol:Test Contract JSON ABI []可以看到生成的结果中ABI数组为空因为我们的智能合约里并没有内容(没有变量声明没有函数)。1.3 总结本章节主要介绍了编译环境的搭建、智能合约的字节码的结构组成以及solc命令的常见用法(生成字节码生成汇编代码生成abi)。在下一章中我们将对生成的汇编代码做深入的分析。第二章 智能合约汇编指令分析本章是智能合约静态分析的第二章在第一章中我们简单演示了如何通过solc命令生成智能合约的汇编代码在本章中我们将对智能合约编译后的汇编代码进行深入分析以及通过evm命令对编译生成的字节码进行反编译。2.1 以太坊中的汇编指令为了让大家更好的理解汇编指令我们先简单介绍下以太坊虚拟机EVM的存储结构熟悉Java虚拟机的同学可以把EVM和JVM进行对比学习。2.1.1 以太坊虚拟机EVM编程语言虚拟机一般有两种类型基于栈或者基于寄存器。和JVM一样EVM也是基于栈的虚拟机。既然是支持栈的虚拟机那么EVM肯定首先得有个栈。为了方便进行密码学计算EVM采用了32字节256比特的字长。EVM栈以字Word为单位进行操作最多可以容纳1024个字。下面是EVM栈的示意图2.1.2 以太坊的汇编指令集和JVM一样EVM执行的也是字节码。由于操作码被限制在一个字节以内所以EVM指令集最多只能容纳256条指令。目前EVM已经定义了约142条指令还有100多条指令可供以后扩展。这142条指令包括算术运算指令比较操作指令按位运算指令密码学计算指令栈、memory、storage操作指令跳转指令区块、智能合约相关指令等。我们会在后面的文章里逐步讨论这些指令下面是已经定义的EVM操作码分布图1灰色区域是目前还没有定义的操作码下面的表格中总结了常用的汇编指令22.2 智能合约汇编分析在第一章中为了便于入门我们分析的智能合约文件并不包含实质的内容。在本章中我们以一个稍微复杂的智能合约为例进行分析。智能合约(保存在test.sol文件中)代码如下pragma solidity0.4.220.6.0;contract Overflow{uintprivatesellerBalance0;functionadd(uint value)returns(bool,uint){sellerBalancevalue;assert(sellerBalancevalue);}}2.2.1 生成汇编代码执行solc命令solc --asm --optimize test.sol其中--optimize选项用来开启编译优化 test.sol:Overflow EVM assembly: ... */ test.sol:36:237 contract Overflow { mstore(0x40, 0x80) /* test.sol:90:91 0 */ 0x00 /* test.sol:61:91 uint private sellerBalance 0 */ dup1 sstore ... */ test.sol:36:237 contract Overflow { callvalue /* --CODEGEN--:8:17 */ dup1 /* --CODEGEN--:5:7 */ iszero tag_1 jumpi /* --CODEGEN--:30:31 */ 0x00 /* --CODEGEN--:27:28 */ dup1 /* --CODEGEN--:20:32 */ revert /* --CODEGEN--:5:7 */ tag_1: ... */ test.sol:36:237 contract Overflow { pop dataSize(sub_0) dup1 dataOffset(sub_0) 0x00 codecopy 0x00 return stop sub_0: assembly { ... */ /* test.sol:36:237 contract Overflow { mstore(0x40, 0x80) callvalue /* --CODEGEN--:8:17 */ dup1 /* --CODEGEN--:5:7 */ iszero tag_1 jumpi /* --CODEGEN--:30:31 */ 0x00 /* --CODEGEN--:27:28 */ dup1 /* --CODEGEN--:20:32 */ revert /* --CODEGEN--:5:7 */ tag_1: ... */ /* test.sol:36:237 contract Overflow { pop jumpi(tag_2, lt(calldatasize, 0x04)) shr(0xe0, calldataload(0x00)) dup1 0x1003e2d2 eq tag_3 jumpi tag_2: 0x00 dup1 revert /* test.sol:100:234 function add(uint value) public returns (bool, u... */ tag_3: tag_4 0x04 dup1 calldatasize sub /* --CODEGEN--:13:15 */ 0x20 /* --CODEGEN--:8:11 */ dup2 /* --CODEGEN--:5:16 */ lt /* --CODEGEN--:2:4 */ iszero tag_5 jumpi /* --CODEGEN--:29:30 */ 0x00 /* --CODEGEN--:26:27 */ dup1 /* --CODEGEN--:19:31 */ revert /* --CODEGEN--:2:4 */ tag_5: pop /* test.sol:100:234 function add(uint value) public returns (bool, u... */ calldataload tag_6 jump // in tag_4: 0x40 dup1 mload swap3 iszero iszero dup4 mstore 0x20 dup4 add swap2 swap1 swap2 mstore dup1 mload swap2 dup3 swap1 sub add swap1 return tag_6: /* test.sol:141:145 bool */ 0x00 /* test.sol:163:185 sellerBalance value */ dup1 sload dup3 add dup1 dup3 sstore /* test.sol:141:145 bool */ dup2 swap1 /* test.sol:203:225 sellerBalance value */ dup4 gt iszero /* test.sol:196:226 assert(sellerBalance value) */ tag_8 jumpi invalid tag_8: /* test.sol:100:234 function add(uint value) public returns (bool, u... */ swap2 pop swap2 jump // out auxdata: 0xa265627a7a723158206f1decff33248a28a8f5d0dc01111fb08dd914cd30bc2245da3904b8fbbd90c564736f6c634300050b0032 }回顾第一章我们得知智能合约编译生成的汇编指令分为三部分EVM assembly标签下的汇编指令对应的是部署代码sub_0标签下的汇编指令对应的是runtime代码是智能合约部署后真正运行的代码。2.2.2 分析汇编代码接下来我们从sub_0标签的入口开始,一步步地进行分析最开始处执行mstore(0x40, 0x80)指令,把0x80存放在内存的0x40处。接着执行callvalue指令,该指令获取交易中的转账金额如果金额是0则执行接下来的jumpi指令就会跳转到tag_1标签。在tag_1标签中POP指令操作码0x50从栈顶弹出一个元素执行jumpi指令在跳转之前要先通过calldatasize指令用来获取本次交易的input字段的值的长度。如果该长度小于4字节则是一个非法调用程序会跳转到tag_2标签下。如果该长度大于4字节则顺序向下执行。接下来是获取交易的input字段中的函数签名。如果input字段中的函数签名等于0x1003e2d2则EVM跳转到tag_3标签下执行,否则不跳转顺序向下执行tag_2。ps:使用web3.sha3(add(uint256))可以计算智能合约中add函数的签名计算结果为0x1003e2d21e48445eba32f76cea1db2f704e754da30edaf8608ddc0f67abca5d0,之后取前四字节0x1003e2d2作为add函数的签名。在tag_3标签中通过calldatasize指令用来获取本次交易的input字段的值的长度x,x-4是否小于0x32。若小于jumpi指令就会跳转到tag_5标签。否则就会跳转到tag_4标签。在tag_5标签中栈顶出栈CALLDATALOAD获取交易中input字段的值。例如calldataload(0x4)指令会把交易的input字段中第4字节之后的32字节入栈。执行jump跳转到tag_6。在tag_6中会执行add函数包括对变量sellerBalance进行赋值以及比较变量sellerBalance和函数参数的大小。如果变量sellerBalance的值大于函数参数(value)接下来会执行jumpi指令跳转到tag_8标签中否则执行invalid程序出错。在tag_8标签中执行两次swap2和一次pop指令后此时的栈顶是tag_4标签即函数调用完成后的返回地址。接下来的jumpi指令会跳转到tag_4标签中执行add函数的调用就执行完毕了。2.3 智能合约字节码的反编译在第一章中我们介绍了go-ethereum的安装安装完成后我们在命令行中就可以使用evm命令了。下面我们使用evm命令对智能合约字节码进行反编译。需要注意的是由于智能合约编译后的字节码分为部署代码、runtime代码和auxdata三部分但是部署后真正执行的是runtime代码所以我们只需要反编译runtime代码即可。还是以本章开始处的智能合约为例执行solc --bin-runtime test.sol命令截取字节码中的runtime代码部分:6080604052348015600f57600080fd5b506004361060285760003560e01c80631003e2d214602d575b600080fd5b605660048036036020811015604157600080fd5b81019080803590602001909291905050506077565b60405180831515151581526020018281526020019250505060405180910390f35b600080826000808282540192505081905550826000541015609457fe5b91509156fe把这段代码保存在某个文件中比如保存在test.bytecode中。接下来执行反编译命令evm disasm test.bytecode得到的结果如下00000: PUSH1 0x80 00002: PUSH1 0x40 00004: MSTORE 00005: CALLVALUE 00006: DUP1 00007: ISZERO 00008: PUSH1 0x0f 0000a: JUMPI 0000b: PUSH1 0x00 0000d: DUP1 0000e: REVERT 0000f: JUMPDEST 00010: POP 00011: PUSH1 0x04 00013: CALLDATASIZE 00014: LT 00015: PUSH1 0x28 00017: JUMPI 00018: PUSH1 0x00 0001a: CALLDATALOAD 0001b: PUSH1 0xe0 0001d: SHR 0001e: DUP1 0001f: PUSH4 0x1003e2d2 00024: EQ 00025: PUSH1 0x2d 00027: JUMPI 00028: JUMPDEST 00029: PUSH1 0x00 0002b: DUP1 0002c: REVERT 0002d: JUMPDEST 0002e: PUSH1 0x56 00030: PUSH1 0x04 00032: DUP1 00033: CALLDATASIZE 00034: SUB 00035: PUSH1 0x20 00037: DUP2 00038: LT 00039: ISZERO 0003a: PUSH1 0x41 0003c: JUMPI 0003d: PUSH1 0x00 0003f: DUP1 00040: REVERT 00041: JUMPDEST 00042: DUP2 00043: ADD 00044: SWAP1 00045: DUP1 00046: DUP1 00047: CALLDATALOAD 00048: SWAP1 00049: PUSH1 0x20 0004b: ADD 0004c: SWAP1 0004d: SWAP3 0004e: SWAP2 0004f: SWAP1 00050: POP 00051: POP 00052: POP 00053: PUSH1 0x77 00055: JUMP 00056: JUMPDEST 00057: PUSH1 0x40 00059: MLOAD 0005a: DUP1 0005b: DUP4 0005c: ISZERO 0005d: ISZERO 0005e: ISZERO 0005f: ISZERO 00060: DUP2 00061: MSTORE 00062: PUSH1 0x20 00064: ADD 00065: DUP3 00066: DUP2 00067: MSTORE 00068: PUSH1 0x20 0006a: ADD 0006b: SWAP3 0006c: POP 0006d: POP 0006e: POP 0006f: PUSH1 0x40 00071: MLOAD 00072: DUP1 00073: SWAP2 00074: SUB 00075: SWAP1 00076: RETURN 00077: JUMPDEST 00078: PUSH1 0x00 0007a: DUP1 0007b: DUP3 0007c: PUSH1 0x00 0007e: DUP1 0007f: DUP3 00080: DUP3 00081: SLOAD 00082: ADD 00083: SWAP3 00084: POP 00085: POP 00086: DUP2 00087: SWAP1 00088: SSTORE 00089: POP 0008a: DUP3 0008b: PUSH1 0x00 0008d: SLOAD 0008e: LT 0008f: ISZERO 00090: PUSH1 0x94 00092: JUMPI 00093: Missing opcode 0xfe 00094: JUMPDEST 00095: SWAP2 00096: POP 00097: SWAP2 00098: JUMP 00099: Missing opcode 0xfe接下来我们把上面的反编译代码和2.1节中生成的汇编代码进行对比分析。2.3.1 分析反编译代码反编译代码的00000到0000e行对应的是汇编代码中sub_0标签到tag_1标签之间的代码。MSTORE指令把0x80存放在内存地址0x40地址处。接下来的CALLVALUE指令获取交易中的转账金额,如果金额是0则执行接下来的JUMPI指令跳转到0x0f地址处。0x0f就是汇编代码中tag_1标签的地址。反编译代码的0000f到00027行对应的是汇编代码中tag_1标签内的代码。接下来的CALLDATASIZE指令判断交易的input字段的值的长度是否小于4如果小于4则之后的JUMPI指令就会跳转到0x28地址处。对比本章第二节中生成的汇编代码不难发现0x28就是tag_2标签的地址。若不小于就会继续向下执行接下来的指令获取input字段中的函数签名如果等于0x1003e2d2则跳转到0x2d地址处。0x2d就是汇编代码中tag_3标签的地址。反编译代码的00028到0002c行对应的是汇编代码中tag_2标签内的代码。反编译代码的0002d到00040行对应的是汇编代码中tag_3标签内的代码。0x2d地址对应的指令是JUMPDEST,该指令没有实际意义只是起到占位的作用。PUSH1 0x56指令把0x58压入栈作为函数调用完成后的返回地址(tag_4标签的地址)。接下来的CALLDATASIZE指令判断交易的input字段的值的长度是否小于36CALLDATASIZE - 4 0x20。0x41就是汇编代码中tag_5标签的地址。反编译代码的00041到00055行对应的是汇编代码中tag_5标签内的代码。CALLDATALOAD获取交易中input字段的值PUSH1 0x77执行JUMP跳转到0x77地址tag_6标签的地址。反编译代码的00056到00076行对应的是汇编代码中tag_4标签内的代码。反编译代码的00077到00093行对应的是汇编代码中tag_6标签内的代码。0x77地址对应的指令是JUMPDEST,之后的指令会执行add函数中的所有代码。如果sellerBalance Value Value为真表明存在上溢。若正常情况下执行LT指令结果为0入栈接下来会执行ISZERO指令JUMPI指令跳转到0x94地址处否则顺序向下执行到0x93地址处。这里有个需要注意的地方在汇编代码中此处显示invalid,但在反编译代码中此处显示Missing opcode 0xfe。反编译代码的00094到00099行对应的是汇编代码中tag_8标签内的代码。2.4 总结本章首先介绍了EVM的存储结构和以太坊中常用的汇编指令。之后逐行分析了智能合约编译后的汇编代码最后反编译了智能合约的字节码把反编译的代码和汇编代码做了对比分析。相信读完本章之后大家基本上能够看懂智能合约的汇编代码和反编译后的代码。在下一章中我们将介绍如何从智能合约的反编译代码中生成控制流图(control flow graph)。第三章 从反编译代码构建控制流图本章是智能合约静态分析的第三章第二章中我们生成了反编译代码本章我们将从这些反编译代码出发一步一步的构建控制流图。3.1 控制流图的概念3.1.1 基本块(basic block)基本块是一个最大化的指令序列程序执行只能从这个序列的第一条指令进入从这个序列的最后一条指令退出。构建基本块的三个原则遇到程序、子程序的第一条指令或语句结束当前基本块并将该语句作为一个新块的第一条语句。遇到跳转语句、分支语句、循环语句将该语句作为当前块的最后一条语句并结束当前块。遇到其他语句直接将其加入到当前基本块。3.1.2 控制流图(control flow graph)控制流图是以基本块为结点的有向图G(N, E)其中N是结点集合表示程序中的基本块E是结点之间边的集合。如果从基本块P的出口转向基本块块Q则从P到Q有一条有向边P-Q表示从结点P到Q存在一条可执行路径P为Q的前驱结点Q为P的后继结点。也就代表在执行完结点P中的代码语句后有可能顺序执行结点Q中的代码语句3。3.2 构建基本块控制流图是由基本块和基本块之间的边构成所以构建基本块是控制流图的前提。接下来我们以反编译代码作为输入分析如何构建基本块。反编译代码示例如下1 00000: PUSH1 0x80 00002: PUSH1 0x40 00004: MSTORE 00005: PUSH1 0x04 00007: CALLDATASIZE 00008: LT 00009: PUSH1 0x3e 0000b: JUMPI 2 0000c: PUSH4 0xffffffff 00011: PUSH29 0x0100000000000000000000000000000000000000000000000000000000 0002f: PUSH1 0x00 00031: CALLDATALOAD 00032: DIV 00033: AND 00034: PUSH4 0x1003e2d2 00039: DUP2 0003a: EQ 0003b: PUSH1 0x43 0003d: JUMPI 3 0003e: JUMPDEST 0003f: PUSH1 0x00 00041: DUP1 00042: REVERT 4 00043: JUMPDEST 00044: CALLVALUE 00045: DUP1 00046: ISZERO 00047: PUSH1 0x4e 00049: JUMPI 5 0004a: PUSH1 0x00 0004c: DUP1 0004d: REVERT 6 0004e: JUMPDEST 0004f: POP 00050: PUSH1 0x58 00052: PUSH1 0x04 00054: CALLDATALOAD 00055: PUSH1 0x73 00057: JUMP 7 00058: JUMPDEST 00059: PUSH1 0x40 0005b: DUP1 0005c: MLOAD 0005d: SWAP3 0005e: ISZERO 0005f: ISZERO 00060: DUP4 00061: MSTORE 00062: PUSH1 0x20 00064: DUP4 00065: ADD 00066: SWAP2 00067: SWAP1 00068: SWAP2 00069: MSTORE 0006a: DUP1 0006b: MLOAD 0006c: SWAP2 0006d: DUP3 0006e: SWAP1 0006f: SUB 00070: ADD 00071: SWAP1 00072: RETURN 8 00073: JUMPDEST 00074: PUSH1 0x00 00076: DUP1 00077: SLOAD 00078: DUP3 00079: ADD 0007a: DUP1 0007b: DUP3 0007c: SSTORE 0007d: DUP2 0007e: SWAP1 0007f: DUP4 00080: GT 00081: ISZERO 00082: PUSH1 0x86 00084: JUMPI 9 00085: Missing opcode 0xfe 10 00086: JUMPDEST 00087: SWAP2 00088: POP 00089: SWAP2 0008a: JUMP 11 0008b: STOP我们从第一条指令开始分析构建基本块的过程。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{ 基本块1: [基本块2,基本块3], 基本块2: [基本块3,基本块4], 基本块3: [基本块11], 基本块4: [基本块5,基本块6], 基本块5: [基本块11], 基本块6: [基本块8], 基本块7: [基本块11], 基本块8: [基本块9,基本块10], 基本块9: [基本块11], 基本块10: [基本块7] }我们把边的集合E用python中的dict类型表示dict中的key是基本块key对应的value值是一个list。还是以基本块1为例因为基本块1存在基本块1-基本块2和基本块1-基本块3两条边所以基本块1对应的list值为[基本块2,基本块3]。3.4 构建控制流图在前两个小节中我们构建完成了基本块和边到此构建控制流图的准备工作都已完成接下来我们就要把基本块和边整合在一起绘制完整的控制流图。上图就是完整的控制流图从图中我们可以清晰直观的看到基本块之间的跳转关系比如基本块1是条件跳转根据条件是否成立跳转到不同的基本块于是就形成了两条边。基本块2和基本块1类似也是条件跳转也会形成两条边。基本块6是直接跳转所以只会形成一条边。在该控制流图中只有一个起始块(基本块1)和一个结束块(基本块11)。当流程走到基本块11的时候表示整个流程结束。需要指出的是基本块11中只包含一条指令STOP。3.5 总结本章先介绍了控制流图中的基本概念之后根据基本块的构建原则完成所有基本块的构建接着结合反编译代码分析了基本块之间的跳转关系画出所有的边。当所有的准备工作完成后最后绘制出控制流图。在下一章中我们将对构建好的控制流图采用z3对其进行约束求解。第四章 从控制流图开始约束求解在本章中我们将使用z3对第三章中生成的控制流图进行约束求解。z3是什么约束求解又是什么呢下面将会给大家一一解答。约束求解求出能够满足所有约束条件的每个变量的值。z3 z3是由微软公司开发的一个优秀的约束求解器用它能求解出满足约束条件的变量的值。从3.4节的控制流图中我们不难发现图中用菱形表示的跳转条件左右代表着基本块跳转的方向。如果我们用变量表示跳转条件中的输入数据再把变量组合成数学表达式此时跳转条件就转变成了约束条件之后我们借助z3对约束条件进行求解根据求解的结果我们就能判断出基本块的跳转方向如此一来我们就能模拟整个程序的执行。4.1 z3的使用我们以z3的python实现z3py为例介绍z3是如何使用4。Python windows: pip install z34.1.1 基本用法fromz3import*xInt(x)yInt(y)solve(x2,y10,x2*y7)在上面的代码中函数Int(x)在z3中创建了一个名为x的变量之后调用了solve函数求在三个约束条件下的解这三个约束条件分别是x 2, y 10, x 2*y 7,运行上面的代码输出结果为:[y 0, x 7]实际上满足约束条件的解不止一个比如[y1,x5]也符合条件,但是z3在默认情况下只寻找满足约束条件的一组解,而不是找出所有解。4.1.2 布尔运算from z3 import * p Bool(p) q Bool(q) r Bool(r) solve(Implies(p, q), r Not(q), Or(Not(p), r))上面的代码演示了z3如何求解布尔约束代码的运行结果如下[q False, p False, r True]4.1.3 位向量在z3中我们可以创建固定长度的位向量比如在下面的代码中BitVec(x, 16)创建了一个长度为16位名为x的变量。fromz3import*xBitVec(x,16)yBitVec(y,16)solve(xy5)4.1.4 求解器fromz3import*xInt(x)yInt(y)sSolver()s.add(x10,yx2)print s print s.check()在上面代码中Solver()创建了一个通用的求解器之后调用add()添加约束调用check()判断是否有满足约束的解。如果有解则返回sat如果没有则返回unsat。4.2 使用z3进行约束求解对于智能合约而言当执行到CALLDATASIZE、CALLDATALOAD等指令时表示程序要获取外部的输入数据,此时我们用z3中的BitVec函数创建一个位向量变量来代替输入数据;当执行到LT、EQ等指令时此时我们用z3创建一个类似If(ULE(xx,xx), 0, 1)的表达式。注If(ULE(x,y), 0, 1) (x y) ? 0: 14.2.1 生成数学表达式接下来我们以3.2节中的基本块1为例看看如何把智能合约的指令转换成数学表达式。在开始转换之前我们先来模拟下以太坊虚拟机的运行环境。我们用变量stack[]来表示以太坊虚拟机的栈用变量memory{}来表示以太坊虚拟机的内存用变量storage{}来表示storage。基本块1为例的指令码如下:00000: PUSH1 0x80 00002: PUSH1 0x40 00004: MSTORE 00005: PUSH1 0x04 00007: CALLDATASIZE 00008: LT 00009: PUSH1 0x3e 0000b: JUMPIPUSH指令是入栈指令执行两次入栈后stack的值为[0x40,0x80](左侧栈顶)MSTORE执行之后stack为空memory的值为{0x40:0x80}CALLDATASIZE指令表示要获取输入数据的长度我们使用z3中的BitVec(Id_size,256),生成一个长度为256位名为Id_size的变量来表示此时输入数据的长度。LT指令用来比较0x04和变量Id_size的大小如果变量Id_size小于0x04则值为1否则值为0。使用z3转换成表达式则为If(ULE(4, Id_size), 0, 1)JUMPI是条件跳转指令是否跳转到0x3e地址处取决于上一步中LT指令的结果即表达式If(ULE(4, Id_size), 0, 1)的结果。如果结果不为0则跳转否则不跳转使用z3转换成表达式则为:If(ULE(4, Id_size), 0, 1) ! 0。至此基本块1中的指令都已经使用z3转换成数学表达式。执行数学表达式执行上一节中生成的数学表达式的伪代码如下所示:from z3import*Id_sizeBitVec(Id_size,256)expIf(ULE(4,Id_size),0,1)!0solverSolver()solver.add(exp)ifsolver.check()sat:printjump to BasicBlock3else:printerror 在上面的代码中调用了solver的check()方法来判断此表达式是否有解如果返回值等于sat则表示表达式有解也就是说LT指令的结果不为0那么接下来就可以跳转到基本块3。观察3.4节中的控制流图我们得知基本块1之后有两条分支如果满足判断条件则跳转到基本块3不满足则跳转到基本块2。但在上面的代码中当check()方法的返回值不等于sat时我们并没有跳转到基本块2而是直接输出错误这是因为当条件表达式无解时继续向下执行没有任何意义。那么如何才能执行到基本块2呢答案是对条件表达式取反然后再判断取反后的表达式是否有解如果有解则跳转到基本块2执行。伪代码如下所示Id_sizeBitVec(Id_size,256)expIf(ULE(4,Id_size),0,1)!0negated_expNot(If(ULE(4,Id_size),0,1)!0)solverSolver()solver.push()solver.add(exp)ifsolver.check()sat:printjump to BasicBlock3else:printerrorsolver.pop()solver.push()solver.add(negated_exp)ifsolver.check()sat:printfalls to BasicBlock2else:printerror在上面代码中我们使用z3中的Not函数对之前的条件表达式进行取反之后调用check()方法判断取反后的条件表达式是否有解如果有解就执行基本块2。Ethereum智能合约静态分(下)https://blog.csdn.net/weixin_43405220/article/details/100553931https://paper.seebug.org/790/ ↩︎https://blog.csdn.net/zxhoo/article/details/81865629 ↩︎程序控制流图 ↩︎https://ericpony.github.io/z3py-tutorial/guide-examples.htm ↩︎