概述

目前，以太坊智能合約的安全事件頻發，從The DAO事件到最近的Fomo3D獎池被盜，每次安全問題的破壞力都是巨大的，如何正確防范智能合約的安全漏洞成了當務之急。本文主要講解了如何通過對智能合約的靜態分析進而發現智能合約中的漏洞。由于智能合約部署之后的更新和升級非常困難，所以在智能合約部署之前對其進行靜態分析，檢測并發現智能合約中的漏洞，可以最大限度的保證智能合約部署之后的安全。

本文包含以下五個章節：

• 智能合約的編譯
• 智能合約匯編指令分析
• 從反編譯代碼構建控制流圖
• 從控制流圖開始約束求解
• 常見的智能合約漏洞以及檢測方法

第一章 智能合約的編譯

本章節是智能合約靜態分析的第一章，主要講解了智能合約的編譯，包括編譯環境的搭建、solidity編譯器的使用。

1.1 編譯環境的搭建

我們以Ubuntu系統為例，介紹編譯環境的搭建過程。首先介紹的是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等命令。

當然，我們也可以通過編譯源碼的方式進行安裝，但是這種安裝方式需要提前安裝golang的環境，步驟比較繁瑣。

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 solidity ^0.4.25; contract Test { }

執行solc命令：solc --bin test.sol

輸出結果如下：

• ======= test.sol:Test =======
• Binary:
• 6080604052348015600f57600080fd5b50603580601d6000396000f3006080604052600080fd00a165627a7a72305820f633e21e144cae24615a160fcb484c1f9495df86d7d21e9be0df2cf3b4c1f9eb0029

solc命令的--bin選項，用來把智能合約編譯后的二進制以十六進制形式表示。和--bin選項類似的是--bin-runtime，這個選項也會輸出十六進制表示，但是會省略智能合約編譯后的部署代碼。接下來我們執行solc命令：

solc --bin-runtime test.sol

輸出結果如下：

• ======= test.sol:Test =======
• Binary of the runtime part:
• 6080604052600080fd00a165627a7a72305820f633e21e144cae24615a160fcb484c1f9495df86d7d21e9be0df2cf3b4c1f9eb0029

對比兩次輸出結果不難發現，使用--bin-runtime選項后，輸出結果的開始部分少了6080604052348015600f57600080fd5b50603580601d6000396000f300，為何會少了這部分代碼呢，看完接下來的智能合約編譯后的字節碼結構就明白了。

1.2.2 智能合約字節碼結構

智能合約編譯后的字節碼，分為三個部分：部署代碼、runtime代碼、auxdata。

1.部署代碼：以上面的輸出結果為例，其中6080604052348015600f57600080fd5b50603580601d6000396000f300為部署代碼。以太坊虛擬機在創建合約的時候，會先創建合約賬戶，然后運行部署代碼。運行完成后它會將runtime代碼+auxdata 存儲到區塊鏈上。之后再把二者的存儲地址跟合約賬戶關聯起來(也就是把合約賬戶中的code hash字段用該地址賦值)，這樣就完成了合約的部署。

2.runtime代碼：該例中6080604052600080fd00是runtime代碼。

3.auxdata：每個合約最后面的43字節就是auxdata，它會緊跟在runtime代碼后面被存儲起來。

solc命令的--bin-runtime選項，輸出了runtime代碼和auxdata，省略了部署代碼，所以輸出結果的開始部分少了6080604052348015600f57600080fd5b50603580601d6000396000f300。

1.2.3 生成匯編代碼

solc命令的--asm選項用來生成匯編代碼，接下來我們還是以最初的智能合約為例執行solc命令，查看生成的匯編代碼。

執行命令：solc --bin --asm test.sol

輸出結果如下：

======= test.sol:Test ======= EVM assembly: ... */ "test.sol":28:52 contract Test { mstore(0x40, 0x80) callvalue /* "--CODEGEN--":8:17 */ dup1 /* "--CODEGEN--":5:7 * iszero tag_1 jumpi /* "--CODEGEN--":30:31 */ 0x0 /* "--CODEGEN--":27:28 */ dup1 /* "--CODEGEN--":20:32 */ revert /* "--CODEGEN--":5:7 */ tag_1: ... */ "test.sol":28:52 contract Test { pop dataSize(sub_0) dup1 dataOffset(sub_0) 0x0 codecopy 0x0 return stop sub_0: assembly { ... */ /* "test.sol":28:52 contract Test { mstore(0x40, 0x80) 0x0 dup1 revert auxdata: 0xa165627a7a72305820f633e21e144cae24615a160fcb484c1f9495df86d7d21e9be0df2cf3b4c1f9eb0029 }

由1.2.2小節可知，智能合約編譯后的字節碼分為部署代碼、runtime代碼和auxdata三部分。同樣，智能合約編譯生成的匯編指令也分為三部分：EVM assembly標簽下的匯編指令對應的是部署代碼；sub_0標簽下的匯編指令對應的是runtime代碼；sub_0標簽下的auxdata和字節碼中的auxdata完全相同。由于目前智能合約文件并沒有實質的內容，所以sub_0標簽下沒有任何有意義的匯編指令。

1.2.4 生成ABI

solc命令的--abi選項可以用來生成智能合約的ABI，同樣還是最開始的智能合約代碼進行演示。

執行solc命令：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]（灰色區域是目前還沒有定義的操作碼）

下面的表格中總結了常用的匯編指令：

操作碼匯編指令描述

0x00	STOP	結束指令
0x01	ADD	把棧頂的兩個值出棧，相加后把結果壓入棧頂
0x02	MUL	把棧頂的兩個值出棧，相乘后把結果壓入棧頂
0x03	SUB	從棧中依次出棧兩個值arg0和arg1，用arg0減去arg1，再把結果壓入棧頂
0x10	LT	把棧頂的兩個值出棧，如果先出棧的值小于后出棧的值則把1入棧，反之把0入棧
0x11	GT	和LT類似，如果先出棧的值大于后出棧的值則把1入棧，反之把0入棧
0x14	EQ	把棧頂的兩個值出棧，如果兩個值相等則把1入棧，否則把0入棧
0x15	ISZERO	把棧頂值出棧，如果該值是0則把1入棧，否則把0入棧
0x34	CALLVALUE	獲取交易中的轉賬金額
0x35	CALLDATALOAD	獲取交易中的input字段的值
0x36	CALLDATASIZE	獲取交易中input字段的值的長度
0x50	POP	把棧頂值出棧
0x51	MLOAD	把棧頂出棧并以該值作為內存中的索引，加載內存中該索引之后的32字節到棧頂
0x52	MSTORE	從棧中依次出棧兩個值arg0和arg1，并把arg1存放在內存的arg0處
0x54	SLOAD	把棧頂出棧并以該值作為storage中的索引，加載該索引對應的值到棧頂
0x55	SSTORE	從棧中依次出棧兩個值arg0和arg1，并把arg1存放在storage的arg0處
0x56	JUMP	把棧頂值出棧，并以此值作為跳轉的目的地址
0x57	JUMPI	從棧中依次出棧兩個值arg0和arg1，如果arg1的值為真則跳轉到arg0處，否則不跳轉
0x60	PUSH1	把1個字節的數值放入棧頂
0x61	PUSH2	把2個字節的數值放入棧頂
0x80	DUP1	復制當前棧中第一個值到棧頂
0x81	DUP2	復制當前棧中第二個值到棧頂
0x90	SWAP1	把棧中第一個值和第二個值進行調換
0x91	SWAP2	把棧中第一個值和第三個值進行調換

2.2 智能合約匯編分析

在第一章中，為了便于入門，我們分析的智能合約文件并不包含實質的內容。在本章中我們以一個稍微復雜的智能合約為例進行分析。智能合約(保存在test.sol文件中)代碼如下：

pragma solidity ^0.4.25; contract Overflow { uint private sellerBalance=0; function add(uint value) returns (bool, uint){ sellerBalance += value; assert(sellerBalance >= value); } }

2.2.1 生成匯編代碼

執行solc命令：solc --asm --optimize test.sol，其中--optimize選項用來開啟編譯優化

輸出的結果如下：

• EVM assembly:
• ... */ "test.sol":26:218 contract Overflow {
• mstore(0x40, 0x80)
• /* "test.sol":78:79 0 */
• 0x0
• /* "test.sol":51:79 uint private sellerBalance=0 */
• dup1
• sstore
• ... */ "test.sol":26:218 contract Overflow {
• callvalue
• /* "--CODEGEN--":8:17 */
• dup1
• /* "--CODEGEN--":5:7 */
• iszero
• tag_1
• jumpi
• /* "--CODEGEN--":30:31 */
• 0x0
• /* "--CODEGEN--":27:28 */
• dup1
• /* "--CODEGEN--":20:32 */
• revert
• /* "--CODEGEN--":5:7 */
• tag_1:
• ... */ "test.sol":26:218 contract Overflow {
• pop
• dataSize(sub_0)
• dup1
• dataOffset(sub_0)
• 0x0
• codecopy
• 0x0
• return
• stop
• sub_0: assembly {
• ... */ /* "test.sol":26:218 contract Overflow {
• mstore(0x40, 0x80)
• jumpi(tag_1, lt(calldatasize, 0x4))
• and(div(calldataload(0x0), 0x100000000000000000000000000000000000000000000000000000000), 0xffffffff)
• 0x1003e2d2
• dup2
• eq
• tag_2
• jumpi
• tag_1:
• 0x0
• dup1
• revert
• ... */ /* "test.sol":88:215 function add(uint value) returns (bool, uint){
• tag_2:
• callvalue
• /* "--CODEGEN--":8:17 */
• dup1
• /* "--CODEGEN--":5:7 */
• iszero
• tag_3
• jumpi
• /* "--CODEGEN--":30:31 */
• 0x0
• /* "--CODEGEN--":27:28 */
• dup1
• /* "--CODEGEN--":20:32 */
• revert
• /* "--CODEGEN--":5:7 */
• tag_3:
• pop
• ... */ /* "test.sol":88:215 function add(uint value) returns (bool, uint){
• tag_4
• calldataload(0x4)
• jump(tag_5)
• tag_4:
• /* 省略部分代碼 */
• tag_5:
• /* "test.sol":122:126 bool */
• 0x0
• /* "test.sol":144:166 sellerBalance += value */
• dup1
• sload
• dup3
• add
• dup1
• dup3
• sstore
• /* "test.sol":122:126 bool */
• dup2
• swap1
• /* "test.sol":184:206 sellerBalance >= value */
• dup4
• gt
• iszero
• /* "test.sol":177:207 assert(sellerBalance >= value) */
• tag_7
• jumpi
• invalid
• tag_7:
• ... */ /* "test.sol":88:215 function add(uint value) returns (bool, uint){
• swap2
• pop
• swap2
• jump // out
• auxdata: 0xa165627a7a7230582067679f8912e58ada2d533ca0231adcedf3a04f22189b53c93c3d88280bb0e2670029
• }

回顧第一章我們得知，智能合約編譯生成的匯編指令分為三部分：EVM assembly標簽下的匯編指令對應的是部署代碼；sub_0標簽下的匯編指令對應的是runtime代碼，是智能合約部署后真正運行的代碼。

2.2.2 分析匯編代碼

接下來我們從sub_0標簽的入口開始,一步步地進行分析：

最開始處執行mstore(0x40, 0x80)指令,把0x80存放在內存的0x40處。

第二步執行jumpi指令，在跳轉之前要先通過calldatasize指令用來獲取本次交易的input字段的值的長度。如果該長度小于4字節則是一個非法調用，程序會跳轉到tag_1標簽下。如果該長度大于4字節則順序向下執行。

接下來是獲取交易的input字段中的函數簽名。如果input字段中的函數簽名等于"0x1003e2d2"，則EVM跳轉到tag_2標簽下執行,否則不跳轉，順序向下執行tag_1。ps:使用web3.sha3("add(uint256)")可以計算智能合約中add函數的簽名，計算結果為0x1003e2d21e48445eba32f76cea1db2f704e754da30edaf8608ddc0f67abca5d0,之后取前四字節"0x1003e2d2"作為add函數的簽名。

在tag_2標簽中，首先執行callvalue指令,該指令獲取交易中的轉賬金額，如果金額是0，則執行接下來的jumpi指令，就會跳轉到tag_3標簽。ps:因為add函數沒有payable修飾，導致該函數不能接受轉賬，所以在調用該函數時會先判斷交易中的轉賬金額是不是0。

在tag_3標簽中，會把tag_4標簽壓入棧，作為函數調用完成后的返回地址，同時calldataload(0x4)指令會把交易的input字段中第4字節之后的32字節入棧，之后跳轉到tag_5標簽中繼續執行。

在tag_5標簽中，會執行add函數中的所有代碼，包括對變量sellerBalance進行賦值以及比較變量sellerBalance和函數參數的大小。如果變量sellerBalance的值大于函數參數，接下來會執行jumpi指令跳轉到tag_7標簽中，否則執行invalid,程序出錯。

在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代碼部分：

• 608060405260043610603e5763ffffffff7c01000000000000000000000000000000000000000000000000000000006000350416631003e2d281146043575b600080fd5b348015604e57600080fd5b5060586004356073565b60408051921515835260208301919091528051918290030190f35b6000805482018082558190831115608657fe5b9150915600

把這段代碼保存在某個文件中，比如保存在test.bytecode中。

接下來執行反編譯命令：evm disasm test.bytecode

得到的結果如下：

• 00000: PUSH1 0x80
• 00002: PUSH1 0x40
• 00004: MSTORE
• 00005: PUSH1 0x04
• 00007: CALLDATASIZE
• 00008: LT
• 00009: PUSH1 0x3e
• 0000b: JUMPI
• 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
• 0003e: JUMPDEST
• 0003f: PUSH1 0x00
• 00041: DUP1
• 00042: REVERT
• 00043: JUMPDEST
• 00044: CALLVALUE
• 00045: DUP1
• 00046: ISZERO
• 00047: PUSH1 0x4e
• 00049: JUMPI
• 0004a: PUSH1 0x00
• 0004c: DUP1
• 0004d: REVERT
• 0004e: JUMPDEST
• 0004f: POP
• 00050: PUSH1 0x58
• 00052: PUSH1 0x04
• 00054: CALLDATALOAD
• 00055: PUSH1 0x73
• 00057: JUMP
• 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
• 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
• 00085: Missing opcode 0xfe
• 00086: JUMPDEST
• 00087: SWAP2
• 00088: POP
• 00089: SWAP2
• 0008a: JUMP
• 0008b: STOP

接下來我們把上面的反編譯代碼和2.1節中生成的匯編代碼進行對比分析。

2.3.1 分析反編譯代碼

反編譯代碼的00000到0003d行，對應的是匯編代碼中sub_0標簽到tag_1標簽之間的代碼。MSTORE指令把0x80存放在內存地址0x40地址處。接下來的LT指令判斷交易的input字段的值的長度是否小于4，如果小于4，則之后的JUMPI指令就會跳轉到0x3e地址處。對比本章第二節中生成的匯編代碼不難發現，0x3e就是tag_1標簽的地址。接下來的指令獲取input字段中的函數簽名，如果等于0x1003e2d2則跳轉到0x43地址處。0x43就是匯編代碼中tag_2標簽的地址。

反編譯代碼的0003e到00042行，對應的是匯編代碼中tag_1標簽內的代碼。

反編譯代碼的00043到0004d行，對應的是匯編代碼中tag_2標簽內的代碼。0x43地址對應的指令是JUMPDEST,該指令沒有實際意義，只是起到占位的作用。接下來的CALLVALUE指令獲取交易中的轉賬金額,如果金額是0，則執行接下來的JUMPI指令，跳轉到0x4e地址處。0x4e就是匯編代碼中tag_3標簽的地址。

反編譯代碼的0004e到00057行，對應的是匯編代碼中tag_3標簽內的代碼。0x4e地址對應的指令是JUMPDEST。接下來的PUSH1 0x58指令，把0x58壓入棧，作為函數調用完成后的返回地址。之后的JUMP指令跳轉到0x73地址處。0x73就是匯編代碼中tag_5標簽的地址。

反編譯代碼的00058到00072行，對應的是匯編代碼中tag_4標簽內的代碼。

反編譯代碼的00073到00085行，對應的是匯編代碼中tag_5標簽內的代碼。0x73地址對應的指令是JUMPDEST,之后的指令會執行add函數中的所有代碼。如果變量sellerBalance的值大于函數參數，接下來會執行JUMPI指令跳轉到0x86地址處，否則順序向下執行到0x85地址處。這里有個需要注意的地方，在匯編代碼中此處顯示invalid,但在反編譯代碼中，此處顯示Missing opcode 0xfe。

反編譯代碼的00086到0008a行，對應的是匯編代碼中tag_7標簽內的代碼。

0008b行對應的指令是STOP,執行到此處時整個流程結束。

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中的代碼語句[2]。

3.2 構建基本塊

控制流圖是由基本塊和基本塊之間的邊構成，所以構建基本塊是控制流圖的前提。接下來我們以反編譯代碼作為輸入，分析如何構建基本塊。

第二章中的反編譯代碼如下：

• 00000: PUSH1 0x80
• 00002: PUSH1 0x40
• 00004: MSTORE
• 00005: PUSH1 0x04
• 00007: CALLDATASIZE
• 00008: LT
• 00009: PUSH1 0x3e
• 0000b: JUMPI
• 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
• 0003e: JUMPDEST
• 0003f: PUSH1 0x00
• 00041: DUP1
• 00042: REVERT
• 00043: JUMPDEST
• 00044: CALLVALUE
• 00045: DUP1
• 00046: ISZERO
• 00047: PUSH1 0x4e
• 00049: JUMPI
• 0004a: PUSH1 0x00
• 0004c: DUP1
• 0004d: REVERT
• 0004e: JUMPDEST
• 0004f: POP
• 00050: PUSH1 0x58
• 00052: PUSH1 0x04
• 00054: CALLDATALOAD
• 00055: PUSH1 0x73
• 00057: JUMP
• 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
• 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
• 00085: Missing opcode 0xfe
• 00086: JUMPDEST
• 00087: SWAP2
• 00088: POP
• 00089: SWAP2
• 0008a: JUMP
• 0008b: STOP

我們從第一條指令開始分析構建基本塊的過程。00000地址處的指令是程序的第一條指令，根據構建基本塊的第一個原則，將其作為新的基本塊的第一條指令；0000b地址處是一條跳轉指令，根據構建基本塊的第二個原則，將其作為新的基本塊的最后一條指令。這樣我們就把從地址00000到0000b的代碼構建成一個基本塊，為了之后方便描述，把這個基本塊命名為基本塊1。

接下來0000c地址處的指令，我們作為新的基本塊的第一條指令。0003d地址處是一條跳轉指令，根據構建基本塊的第二個原則，將其作為新的基本塊的最后一條指令。于是從地址0000c到0003d就構成了一個新的基本塊，我們把這個基本塊命名為基本塊2。

以此類推，我們可以遵照構建基本塊的三個原則構建起所有的基本塊。構建完成后的基本塊如下圖所示：

圖中的每一個矩形是一個基本塊，矩形的右半部分是為了后續描述方便而對基本塊的命名(當然你也可以命名成自己喜歡的名字)。矩形的左半部分是基本塊所包含的指令的起始地址和結束地址。當所有的基本塊都構建完成后，我們就把之前的反編譯代碼轉化成了11個基本塊。接下來我們將構建基本塊之間的邊。

3.3 構建基本塊之間的邊

簡單來說，基本塊之間的邊就是基本塊之間的跳轉關系。以基本塊1為例，其最后一條指令是條件跳轉指令，如果條件成立就跳轉到基本塊3，否則就跳轉到基本塊2。所以基本塊1就存在基本塊1->基本塊2和基本塊1->基本塊3兩條邊?；緣K6的最后一條指令是跳轉指令，該指令會直接跳轉到基本塊8，所以基本塊6就存在基本塊6->基本塊8這一條邊。

結合反編譯代碼和基本塊的劃分，我們不難得出所有邊的集合E：

• {
• '基本塊1': ['基本塊2','基本塊3'],
• '基本塊2': ['基本塊3','基本塊4'],
• '基本塊3': ['基本塊11'],
• '基本塊4': ['基本塊5','基本塊6'],
• '基本塊5': ['基本塊11'],
• '基本塊6': ['基本塊8'],
• '基本塊7': ['基本塊8'],
• '基本塊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是條件跳轉，根據條件是否成立跳轉到不同的基本塊，于是就形成了兩條邊?；緣K2和基本塊1類似也是條件跳轉，也會形成兩條邊。基本塊6是直接跳轉，所以只會形成一條邊。

在該控制流圖中，只有一個起始塊(基本塊1)和一個結束塊(基本塊11)。當流程走到基本塊11的時候，表示整個流程結束。需要指出的是，基本塊11中只包含一條指令STOP。

3.5 總結

本章先介紹了控制流圖中的基本概念，之后根據基本塊的構建原則完成所有基本塊的構建，接著結合反編譯代碼分析了基本塊之間的跳轉關系，畫出所有的邊。當所有的準備工作完成后，最后繪制出控制流圖。在下一章中，我們將對構建好的控制流圖，采用z3對其進行約束求解。

第四章 從控制流圖開始約束求解

在本章中我們將使用z3對第三章中生成的控制流圖進行約束求解。z3是什么，約束求解又是什么呢？下面將會給大家一一解答。

約束求解：求出能夠滿足所有約束條件的每個變量的值。

z3： z3是由微軟公司開發的一個優秀的約束求解器，用它能求解出滿足約束條件的變量的值。

從3.4節的控制流圖中我們不難發現，圖中用菱形表示的跳轉條件左右著基本塊跳轉的方向。如果我們用變量表示跳轉條件中的輸入數據，再把變量組合成數學表達式，此時跳轉條件就轉變成了約束條件，之后我們借助z3對約束條件進行求解，根據求解的結果我們就能判斷出基本塊的跳轉方向，如此一來我們就能模擬整個程序的執行。

接下來我們就從z3的基本使用開始，一步一步的完成對所有跳轉條件的約束求解。

4.1 z3的使用

我們以z3的python實現z3py為例介紹z3是如何使用的[3]。

4.1.1 基本用法

• from z3 import *
• x = Int('x')
• y = Int('y')
• solve(x > 2, y < 10, x + 2*y == 7)

在上面的代碼中，函數Int('x')在z3中創建了一個名為x的變量，之后調用了solve函數求在三個約束條件下的解，這三個約束條件分別是x > 2,?y < 10,?x + 2*y == 7,運行上面的代碼，輸出結果為:

• [y = 0, x = 7]

實際上滿足約束條件的解不止一個，比如[y=1,x=5]也符合條件,但是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的變量。

• from z3 import *
• x = BitVec('x', 16)
• y = BitVec('y', 16)
• solve(x + y > 5)

在z3中除了可以創建位向量變量之外，也可以創建位向量常量。下面代碼中的BitVecVal(-1, 16)創建了一個長度為16位，值為1的位向量常量。

• from z3 import *
• a = BitVecVal(-1, 16)
• b = BitVecVal(65535, 16)
• print simplify(a == b)

4.1.4 求解器

• from z3 import *
• x = Int('x')
• y = Int('y')
• s = Solver()
• s.add(x > 10, y == x + 2)
• 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)的表達式。

4.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: JUMPI

PUSH指令是入棧指令，執行兩次入棧后，stack的值為[0x80,0x40]

MSTORE執行之后，stack為空，memory的值為{0x40:0x80}

CALLDATASIZE指令表示要獲取輸入數據的長度，我們使用z3中的BitVec("Id_size",256),生成一個長度為256位，名為Id_size的變量來表示此時輸入數據的長度。

LT指令用來比較0x04和變量Id_size的大小，如果0x04小于變量Id_size則值為0，否則值為1。使用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轉換成數學表達式。

4.2.2 執行數學表達式

執行上一節中生成的數學表達式的偽代碼如下所示：

• from z3 import *
• Id_size = BitVec("Id_size",256)
• exp = If(ULE(4, Id_size), 0, 1) != 0
• solver = Solver()
• solver.add(exp)
• if solver.check() == sat:
• print "jump to BasicBlock3"
• else:
• print "error "

在上面的代碼中調用了solver的check()方法來判斷此表達式是否有解，如果返回值等于sat則表示表達式有解，也就是說LT指令的結果不為0，那么接下來就可以跳轉到基本塊3。

觀察3.4節中的控制流圖我們得知，基本塊1之后有兩條分支，如果滿足判斷條件則跳轉到基本塊3，不滿足則跳轉到基本塊2。但在上面的代碼中，當check()方法的返回值不等于sat時，我們并沒有跳轉到基本塊2，而是直接輸出錯誤，這是因為當條件表達式無解時，繼續向下執行沒有任何意義。那么如何才能執行到基本塊2呢，答案是對條件表達式取反，然后再判斷取反后的表達式是否有解，如果有解則跳轉到基本塊2執行。偽代碼如下所示：

• Id_size = BitVec("Id_size",256)
• exp = If(ULE(4, Id_size), 0, 1) != 0
• negated_exp = Not(If(ULE(4, Id_size), 0, 1) != 0)
• solver = Solver()
• solver.push()
• solver.add(exp)
• if solver.check() == sat:
• print "jump to BasicBlock3"
• else:
• print "error"
• solver.pop()
• solver.push()
• solver.add(negated_exp)
• if solver.check() == sat:
• print "falls to BasicBlock2"
• else:
• print "error"

在上面代碼中，我們使用z3中的Not函數，對之前的條件表達式進行取反，之后調用check()方法判斷取反后的條件表達式是否有解，如果有解就執行基本塊2。

4.3 總結

本章首先介紹了z3的基本用法，之后以基本塊1為例，分析了如何使用z3把指令轉換成表達式，同時也分析了如何對轉換后的表達式進行約束求解。在下一章中我們將會介紹如何在約束求解的過程中加入對智能合約漏洞的分析，精彩不容錯過。

第五章 常見的智能合約漏洞以及檢測方法

在本章中，我們首先會介紹智能合約中常見的漏洞，之后會分析檢測這些漏洞的方法。

5.1 智能合約中常見的漏洞

5.1.1 整數溢出漏洞

我們以8位無符號整數為例分析溢出產生的原因，如下圖所示，最大的8位無符號整數是255，如果此時再加1就會變為0。

Solidity語言支持從uint8到uint256，uint256的取值范圍是0到2^256-1。如果某個uint256變量的值為2^256-1，那么這個變量再加1就會發生溢出，同時該變量的值變為0。

• pragma solidity ^0.4.20;
• contract Test {
• function overflow() public pure returns (uint256 _overflow) {
• uint256 max = 2**256-1;
• return max + 1;
• }
• }

上面的合約代碼中，變量max的值為2^256-1，是uint256所能表示的最大整數，如果再加1就會產生溢出，max的值變為0。

5.1.2 重入漏洞

當智能合約向另一個智能合約轉賬時，后者的fallback函數會被調用。如果fallback函數中存在惡意代碼，那么惡意代碼會被執行,這就是重入漏洞產生的前提。那么重入漏洞在什么情況下會發生呢，下面我們以一個存在重入漏洞的智能合約為例進行分析。

• pragma solidity ^0.4.20;
• contract Bank {
• address owner;
• mapping (address => uint256) balances;
• constructor() public payable{
• owner = msg.sender;
• }
• function deposit() public payable {
• balances[msg.sender] += msg.value;
• }
• function withdraw(address receiver, uint256 amount) public{
• require(balances[msg.sender] > amount);
• require(address(this).balance > amount);
• // 使用 call.value()()進行ether轉幣時，沒有Gas限制
• receiver.call.value(amount)();
• balances[msg.sender] -= amount;
• }
• function balanceOf(address addr) public view returns (uint256) {
• return balances[addr];
• }
• }
• contract Attack {
• address owner;
• address victim;
• constructor() public payable {
• owner = msg.sender;
• }
• function setVictim(address target) public{
• victim = target;
• }
• function step1(uint256 amount) public payable{
• if (address(this).balance > amount) {
• victim.call.value(amount)(bytes4(keccak256("deposit()")));
• }
• }
• function step2(uint256 amount) public{
• victim.call(bytes4(keccak256("withdraw(address,uint256)")), this,amount);
• }
• // selfdestruct, send all balance to owner
• function stopAttack() public{
• selfdestruct(owner);
• }
• function startAttack(uint256 amount) public{
• step1(amount);
• step2(amount / 2);
• }
• function () public payable {
• if (msg.sender == victim) {
• // 再次嘗試調用Bank合約的withdraw函數，遞歸轉幣
• victim.call(bytes4(keccak256("withdraw(address,uint256)")), this,msg.value);
• }
• }
• }

在上面的代碼中，智能合約Bank是存在重入漏洞的合約，其內部的withdraw()方法使用了call方法進行轉賬，使用該方法轉賬時沒有gas限制。 智能合約Attack是個惡意合約，用來對存在重入的智能合約Bank進行攻擊。攻擊流程如下：

• Attack先給Bank轉幣
• Bank在其內部的賬本balances中記錄Attack轉幣的信息
• Attack要求Bank退幣
• Bank先退幣再修改賬本balances

問題就出在Bank是先退幣再去修改賬本balances。因為Bank退幣的時候，會觸發Attack的fallback函數，而Attack的fallback函數中會再次執行退幣操作，如此遞歸下去，Bank沒有機會進行修改賬本的操作，最后導致Attack會多次收到退幣。

5.2 漏洞的檢測方法

5.2.1 整數溢出漏洞的檢測

通過約束求解可以很容易的發現智能合約中的整數溢出漏洞，下面我們就通過一個具體的例子一步步的分析。

首先對5.1.1節中的智能合約進行反編譯，得到的部分反編譯代碼如下：

• 000108: PUSH1 0x00
• 000110: DUP1
• 000111: PUSH32 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
• 000144: SWAP1
• 000145: POP
• 000146: PUSH1 0x01
• 000148: DUP2
• 000149: ADD
• 000150: SWAP2
• 000151: POP
• 000152: POP
• 000153: SWAP1
• 000154: JUMP

這段反編譯后的代碼對應的是智能合約中的overflow函數，第000149行的ADD指令對應的是函數中max + 1這行代碼。ADD指令會把棧頂的兩個值出棧，相加后把結果壓入棧頂。下面我們就通過一段偽代碼來演示如何檢測整數溢出漏洞：

• def checkOverflow():
• first = stack.pop(0)
• second = stack.pop(0)
• first = BitVecVal(first, 256)
• second = BitVecVal(second, 256)
• computed = first + second
• solver.add(UGT(first, computed))
• if check_sat(solver) == sat:
• print "have overflow"

我們先把棧頂的兩個值出棧，然后使用z3中BitVecVal()函數的把這兩個值轉變成位向量常量，接著計算兩個位向量常量相加的結果,最后構建表達式UGT(first, computed)來判斷加數是否大于相加的結果，如果該表達式有解則說明會發生整數溢出[4]。

5.2.2 重入漏洞的檢測

在分析重入漏洞之前，我們先來總結在智能合約中用于轉賬的方法：

• address.transfer(amount): 當發送失敗時會拋出異常，只會傳遞2300Gas供調用，可以防止重入漏洞

• address.send(amount): 當發送失敗時會返回false，只會傳遞2300Gas供調用，可以防止重入漏洞

• address.gas(gas_value).call.value(amount)(): 當發送失敗時會返回false，傳遞所有可用Gas進行調用(可通過 gas(gas_value) 進行限制)，不能有效防止重入

通過以上對比不難發現，transfer(amount)和send(amount)限制Gas最多為2300，使用這兩個方法轉賬可以有效地防止重入漏洞。call.value(amount)()默認不限制Gas的使用，這就會很容易導致重入漏洞的產生。既然call指令是產生重入漏洞的原因所在，那么接下來我們就詳細分析這條指令。

call指令有七個參數，每個參數的含義如下所示：

call(gas, address, value, in, insize, out, outsize)

• 第一個參數是指定的gas限制，如果不指定該參數，默認不限制。
• 第二個參數是接收轉賬的地址
• 第三個參數是轉賬的金額
• 第四個參數是輸入給call指令的數據在memory中的起始地址
• 第五個參數是輸入的數據的長度
• 第六個參數是call指令輸出的數據在memory中的起始地址
• 第七個參數是call指令輸出的數據的長度

通過以上的分析，總結下來我們可以從以下兩個維度去檢測重入漏洞

• 判斷call指令第一個參數的值，如果沒有設置gas限制，那么就有產生重入漏洞的風險
• 檢查call指令之后，是否還有其他的操作。

第二個維度中提到的call指令之后是否還有其他操作，是如何可以檢測到重入漏洞的呢？接下來我們就詳細分析下。在5.1.2節中的智能合約Bank是存在重入漏洞的，根本原因就是使用call指令進行轉賬沒有設置Gas限制，同時在withdraw方法中先退幣再去修改賬本balances，關鍵代碼如下：

• receiver.call.value(amount)();
• balances[msg.sender] -= amount;

執行call指令的時候，會觸發Attack中的fallback函數，而Attack的fallback函數中會再次執行退幣操作，如此遞歸下去，導致Bank無法執行接下來的修改賬本balances的操作。此時如果我們對代碼做出如下調整，先修改賬本balances，之后再去調用call指令，雖然也還會觸發Attack中的fallback函數，Attack的fallback函數中也還會再次執行退幣操作，但是每次退幣操作都是先修改賬本balances，所以Attack只能得到自己之前存放在Bank中的幣，重入漏洞不會發生。

• balances[msg.sender] -= amount;
• receiver.call.value(amount)();

總結

本文的第一章介紹了智能合約編譯環境的搭建以及編譯器的使用，第二章講解了常用的匯編指令并且對反編譯后的代碼進行了逐行的分析。前兩章都是基本的準備工作，從第三章開始，我們使用之前的反編譯代碼，構建了完整的控制流圖。第四章中我們介紹了z3的用法以及如何把控制流圖中的基本塊中的指令用z3轉換成數學表達式。第五章中我們通過整數溢出和重入漏洞的案例，詳細分析了如何在約束求解的過程中檢測智能合約中的漏洞。最后，希望讀者在閱讀本文后能有所收獲，如有不足之處歡迎指正。

參考

以太坊虛擬機介紹_zxh的專欄-CSDN博客_以太坊虛擬機

http://cc.jlu.edu.cn/G2S/Template/View.aspx

Z3Py Guide

GitHub - enzymefinance/oyente: An Analysis Tool for Smart Contracts

本文鏈接：區塊鏈安全-以太坊智能合約靜態分析 - 360 核心安全技術博客

總結

以上是生活随笔為你收集整理的区块链安全-以太坊智能合约静态分析的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。