區塊鏈安全--以太坊智慧合約靜態分析

阿新 • • 發佈：2019-01-11

作者：高峰黃紹莽（來自 360 IceSword Lab）

概述

目前，以太坊智慧合約的安全事件頻發，從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指令集

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

操作碼	彙編指令	描述
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兩條邊。基本塊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轉換成數學表示式。第五章中我們通過整數溢位和重入漏洞的案例，詳細分析瞭如何在約束求解的過程中檢測智慧合約中的漏洞。最後，希望讀者在閱讀本文後能有所收穫，如有不足之處歡迎指正。

參考

轉載自：http://blogs.360.cn/post/staticAnalysis_of_smartContract.html

區塊鏈安全--以太坊智慧合約靜態分析

概述

第一章 智慧合約的編譯

1.1 編譯環境的搭建

1.1.1 安裝go-ethereum

1.1.2 安裝solidity編譯器

1.2 solidity編譯器的使用

1.2.1 基本用法

1.2.2 智慧合約位元組碼結構

1.2.3 生成彙編程式碼

1.2.4 生成ABI

1.3 總結

第二章 智慧合約彙編指令分析

2.1 以太坊中的彙編指令

2.1.1 以太坊虛擬機器EVM

2.1.2 以太坊的彙編指令集：

2.2 智慧合約彙編分析

2.2.1 生成彙編程式碼

2.2.2 分析彙編程式碼

2.3 智慧合約位元組碼的反編譯

2.3.1 分析反編譯程式碼

2.4 總結

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

3.1 控制流圖的概念

3.1.1 基本塊(basic block)

3.1.2 控制流圖(control flow graph)

3.2 構建基本塊

3.3 構建基本塊之間的邊

3.4 構建控制流圖

3.5 總結

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

4.1 z3的使用

4.1.1 基本用法

4.1.2 布林運算

4.1.3 位向量

4.1.4 求解器

4.2 使用z3進行約束求解

4.2.1 生成數學表示式

4.2.2 執行數學表示式

4.3 總結

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

5.1 智慧合約中常見的漏洞

5.1.1 整數溢位漏洞

5.1.2 重入漏洞

5.2 漏洞的檢測方法

5.2.1 整數溢位漏洞的檢測

5.2.2 重入漏洞的檢測

總結

參考

相關推薦

第一章智慧合約的編譯

第二章智慧合約彙編指令分析

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

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

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