作者：高峰 黃紹莽@360 IceSword Lab
博客：https://www.iceswordlab.com

概述

目前，以太坊智能合約的安全事件頻發，從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棧的示意圖：

EVM棧示意圖

2.1.2 以太坊的匯編指令集：

和JVM一樣，EVM執行的也是字節碼。由于操作碼被限制在一個字節以內，所以EVM指令集最多只能容納256條指令。目前EVM已經定義了約142條指令，還有100多條指令可供以后擴展。這142條指令包括算術運算指令，比較操作指令，按位運算指令，密碼學計算指令，棧、memory、storage操作指令，跳轉指令，區塊、智能合約相關指令等。下面是已經定義的EVM操作碼分布圖[1]（灰色區域是目前還沒有定義的操作碼）

EVM指令集

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

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標簽的入口開始,一步步地進行分析：

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

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

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

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

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

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

  7. 在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 分析反編譯代碼

  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標簽的地址。
  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 opcode 0xfe。
  7. 反編譯代碼的00086到0008a行，對應的是匯編代碼中tag_7標簽內的代碼。
  8. 0008b行對應的指令是STOP,執行到此處時整個流程結束。

2.4 總結

本章首先介紹了EVM的存儲結構和以太坊中常用的匯編指令。之后逐行分析了智能合約編譯后的匯編代碼，最后反編譯了智能合約的字節碼，把反編譯的代碼和匯編代碼做了對比分析。相信讀完本章之后，大家基本上能夠看懂智能合約的匯編代碼和反編譯后的代碼。在下一章中，我們將介紹如何從智能合約的反編譯代碼中生成控制流圖(control flow graph)。

第三章 從反編譯代碼構建控制流圖

本章是智能合約靜態分析的第三章，第二章中我們生成了反編譯代碼，本章我們將從這些反編譯代碼出發，一步一步的構建控制流圖。

3.1 控制流圖的概念

3.1.1 基本塊(basic block)

基本塊是一個最大化的指令序列，程序執行只能從這個序列的第一條指令進入，從這個序列的最后一條指令退出。

構建基本塊的三個原則：

  1. 遇到程序、子程序的第一條指令或語句，結束當前基本塊，并將該語句作為一個新塊的第一條語句。
  2. 遇到跳轉語句、分支語句、循環語句，將該語句作為當前塊的最后一條語句，并結束當前塊。
  3. 遇到其他語句直接將其加入到當前基本塊。

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兩條邊。基本塊6的最后一條指令是跳轉指令，該指令會直接跳轉到基本塊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是條件跳轉，根據條件是否成立跳轉到不同的基本塊，于是就形成了兩條邊。基本塊2和基本塊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轉換成數學表達式。第五章中我們通過整數溢出和重入漏洞的案例，詳細分析了如何在約束求解的過程中檢測智能合約中的漏洞。最后，希望讀者在閱讀本文后能有所收獲，如有不足之處歡迎指正。

參考

  1. https://blog.csdn.net/zxhoo/article/details/81865629

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

  3. https://ericpony.github.io/z3py-tutorial/guide-examples.htm

  4. https://github.com/melonproject/oyente

Paper 本文由 Seebug Paper 發布，如需轉載請注明來源。本文地址：http://www.bjnorthway.com/790/