以太坊智能合約靜態分析

時間  2019-11-08
標籤 以太 智能 合約 靜態 分析 欄目 網站開發 简体版
原文   原文鏈接

做者：高峯 黃紹莽（來自 360 IceSword Lab）node

概述

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

本文包含如下五個章節：git

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

第一章 智能合約的編譯

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

1.1 編譯環境的搭建

咱們以Ubuntu系統爲例，介紹編譯環境的搭建過程。首先介紹的是go-ethereum的安裝。golang

1.1.1 安裝go-ethereum

經過apt-get安裝是比較簡便的安裝方法，只須要在安裝以前添加go-ethereum的ppa倉庫，完整的安裝命令以下：web

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命令了。bash

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

  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
相關文章
相關標籤/搜索
每日一句
    每一个你不满意的现在，都有一个你没有努力的曾经。
本站公眾號
   歡迎關注本站公眾號,獲取更多信息
聯繫我們 最近搜索 最新文章 沪ICP备13005482号-10 MyBatis教程 SQL 教程 MySQL教程 Java 教程 Thymeleaf 教程 Hibernate教程 Spring教程 Redis教程