跳至主要內容

如何使用曼蒂科爾尋找智能合約中的錯誤

solidity
智能合約
安全性
測試
形式化驗證
進階
Trailofbits
2020年1月13日
16 分鐘閱讀

本教學的目的是展示如何使用曼蒂科爾自動尋找智能合約中的錯誤。

安裝

曼蒂科爾需要 >= Python 3.6。可以透過 pip 或使用 Docker 安裝。

透過 Docker 安裝曼蒂科爾

docker pull trailofbits/eth-security-toolbox
docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox

最後一個指令會在可以存取您目前目錄的 Docker 中執行 eth-security-toolbox。您可以從主機更改檔案，並在 Docker 中對這些檔案執行工具

在 Docker 內部，執行：

solc-select 0.5.11
cd /home/trufflecon/

透過 pip 安裝曼蒂科爾

pip3 install --user manticore

建議使用 solc 0.5.11。

執行腳本

若要使用 Python 3 執行 Python 腳本：

python3 script.py

動態符號執行簡介

動態符號執行簡述

動態符號執行 (DSE) 是一種程式分析技術，它以高度的語義感知來探索狀態空間。這項技術基於「程式路徑」的發現，這些路徑以稱為 path predicates 的數學公式表示。在概念上，這項技術分兩個步驟對路徑謂詞進行操作：

  1. 它們是使用對程式輸入的約束條件建構而成的。
  2. 它們被用來產生會導致相關路徑執行的程式輸入。

這種方法不會產生誤報，因為所有識別出的程式狀態都可以在具體執行期間被觸發。例如，如果分析發現整數溢位，則保證它是可重現的。

路徑謂詞範例

為了深入了解 DSE 的運作方式，請考慮以下範例：

function f(uint a){

  if (a == 65) {
      // 存在錯誤
  }

}

由於 f() 包含兩條路徑，DSE 將建構兩個不同的路徑謂詞：

  • 路徑 1：a == 65
  • 路徑 2：Not (a == 65)

每個路徑謂詞都是一個數學公式，可以交給所謂的 SMT 求解器 (opens in a new tab)，它將嘗試求解該方程式。對於 Path 1，求解器會說可以使用 a = 65 來探索該路徑。對於 Path 2，求解器可以賦予 a 任何非 65 的值，例如 a = 0。

驗證屬性

曼蒂科爾允許完全控制每條路徑的所有執行過程。因此，它允許您對幾乎任何事物添加任意約束條件。這種控制能力允許在合約上建立屬性。

考慮以下範例：

function unsafe_add(uint a, uint b) returns(uint c){
  c = a + b; // 沒有溢位保護
  return c;
}

這裡在函式中只有一條路徑可以探索：

  • 路徑 1：c = a + b

使用曼蒂科爾，您可以檢查溢位，並將約束條件添加到路徑謂詞中：

  • c = a + b AND (c < a OR c < b)

如果可以找到 a 和 b 的賦值，使得上述路徑謂詞可行，這意味著您發現了一個溢位。例如，求解器可以產生輸入 a = 10 , b = MAXUINT256。

如果您考慮一個已修復的版本：

function safe_add(uint a, uint b) returns(uint c){
  c = a + b;
  require(c>=a);
  require(c>=b);
  return c;
}

帶有溢位檢查的相關公式將會是：

  • c = a + b AND (c >= a) AND (c=>b) AND (c < a OR c < b)

這個公式無法求解；換句話說，這是一個證明，證明在 safe_add 中，c 將始終增加。

因此，DSE 是一個強大的工具，可以驗證程式碼上的任意約束條件。

在曼蒂科爾下執行

我們將了解如何使用曼蒂科爾 API 探索智能合約。目標是以下智能合約 example.sol (opens in a new tab)：

執行獨立探索

您可以透過以下指令直接在智能合約上執行曼蒂科爾（project 可以是 Solidity 檔案或專案目錄）：

$ manticore project

您將獲得類似以下的測試案例輸出（順序可能會改變）：

在沒有額外資訊的情況下，曼蒂科爾將使用新的符號交易來探索合約，直到它無法在合約上探索出新路徑為止。曼蒂科爾不會在失敗的交易（例如：回滾之後）之後執行新的交易。

曼蒂科爾會將資訊輸出到 mcore_* 目錄中。除此之外，您會在這個目錄中找到：

  • global.summary：覆蓋率與編譯器警告
  • test_XXXXX.summary：每個測試案例的覆蓋率、最後一個指令、帳戶餘額
  • test_XXXXX.tx：每個測試案例的詳細交易列表

曼蒂科爾在這裡找到了 7 個測試案例，分別對應於（檔案名稱順序可能會改變）：

交易 0交易 1交易 2結果
test_00000000.tx建立合約f(!=65)f(!=65)STOP
test_00000001.tx建立合約回退函式REVERT
test_00000002.tx建立合約RETURN
test_00000003.tx建立合約f(65)REVERT
test_00000004.tx建立合約f(!=65)STOP
test_00000005.tx建立合約f(!=65)f(65)REVERT
test_00000006.tx建立合約f(!=65)回退函式REVERT

探索摘要 f(!=65) 表示使用任何非 65 的值呼叫 f。

如您所見，曼蒂科爾會為每個成功或回滾的交易產生一個獨特的測試案例。

如果您想要快速探索程式碼，請使用 --quick-mode 標誌（它會停用錯誤偵測器、燃料計算等）

透過 API 操作智能合約

本節詳細說明如何透過曼蒂科爾 Python API 操作智能合約。您可以建立一個副檔名為 Python 的新檔案 *.py，並透過將 API 指令（其基礎將在下面說明）加入此檔案中來編寫必要的程式碼，然後使用指令 $ python3 *.py 執行它。您也可以直接在 Python 主控台中執行以下指令，若要執行主控台，請使用指令 $ python3。

建立帳戶

您應該做的第一件事是使用以下指令初始化一個新的區塊鏈：

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

使用 m.create_account (opens in a new tab) 建立非合約帳戶：

user_account = m.create_account(balance=1000)

可以使用 m.solidity_create_contract (opens in a new tab) 部署 Solidity 合約：

摘要

執行交易

曼蒂科爾支援兩種類型的交易：

  • 原始交易：探索所有函式
  • 具名交易：僅探索一個函式

原始交易

使用 m.transaction (opens in a new tab) 執行原始交易：

m.transaction(caller=user_account,
              address=contract_account,
              data=data,
              value=value)

交易的呼叫者、地址、資料或值可以是具體的或符號的：

例如：

symbolic_value = m.make_symbolic_value()
symbolic_data = m.make_symbolic_buffer(320)
m.transaction(caller=user_account,
              address=contract_address,
              data=symbolic_data,
              value=symbolic_value)

如果資料是符號的，曼蒂科爾將在交易執行期間探索合約的所有函式。查看 Ethernaut CTF 實戰 (opens in a new tab) 文章中的回退函式說明，將有助於了解函式選擇的運作方式。

具名交易

可以透過函式名稱來執行函式。 若要從 user_account 以 0 顆以太幣和一個符號值執行 f(uint var)，請使用：

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var, caller=user_account, value=0)

如果未指定交易的 value，則預設為 0。

摘要

  • 交易的參數可以是具體的或符號的
  • 原始交易將探索所有函式
  • 可以透過名稱呼叫函式

工作區

m.workspace 是用作所有產生檔案的輸出目錄：

print("Results are in {}".format(m.workspace))

終止探索

若要停止探索，請使用 m.finalize() (opens in a new tab)。一旦呼叫此方法，就不應發送進一步的交易，並且曼蒂科爾會為每個探索過的路徑產生測試案例。

摘要：在曼蒂科爾下執行

將前面所有步驟放在一起，我們得到：

您可以在 example_run.py (opens in a new tab) 中找到上述所有程式碼

取得拋出異常的路徑

我們現在將為在 f() 中引發異常的路徑產生特定的輸入。目標仍然是以下智能合約 example.sol (opens in a new tab)：

pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

使用狀態資訊

執行的每條路徑都有其區塊鏈狀態。狀態要麼是就緒 (ready)，要麼是被終止 (killed)，這意味著它到達了 THROW 或 REVERT 指令：

for state in m.all_states:
    # 對狀態進行操作

您可以存取狀態資訊。例如：

  • state.platform.get_balance(account.address)：帳戶的餘額
  • state.platform.transactions：交易列表
  • state.platform.transactions[-1].return_data：最後一筆交易回傳的資料

最後一筆交易回傳的資料是一個陣列，可以使用 ABI.deserialize 將其轉換為一個值，例如：

data = state.platform.transactions[0].return_data
data = ABI.deserialize("uint", data)

如何產生測試案例

使用 m.generate_testcase(state, name) (opens in a new tab) 產生測試案例：

m.generate_testcase(state, 'BugFound')

摘要

  • 您可以使用 m.all_states 迭代狀態
  • state.platform.get_balance(account.address) 回傳帳戶的餘額
  • state.platform.transactions 回傳交易列表
  • transaction.return_data 是回傳的資料
  • m.generate_testcase(state, name) 為狀態產生輸入

摘要：取得拋出異常的路徑

您可以在 example_run.py (opens in a new tab) 中找到上述所有程式碼

請注意，我們本可以產生一個簡單得多的腳本，因為 terminated_state 回傳的所有狀態在其結果中都有 REVERT 或 INVALID：這個範例只是為了示範如何操作 API。

加入約束條件

我們將了解如何約束探索。我們將假設 f() 的文件指出該函式永遠不會以 a == 65 呼叫，因此任何帶有 a == 65 的錯誤都不是真正的錯誤。目標仍然是以下智能合約 example.sol (opens in a new tab)：

pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

運算子

Operators (opens in a new tab) 模組有助於操作約束條件，除此之外它還提供：

  • Operators.AND,
  • Operators.OR,
  • Operators.UGT（無號大於）,
  • Operators.UGE（無號大於或等於）,
  • Operators.ULT（無號小於）,
  • Operators.ULE（無號小於或等於）。

若要匯入該模組，請使用以下指令：

from manticore.core.smtlib import Operators

Operators.CONCAT 用於將陣列串接到一個值。例如，交易的 return_data 需要更改為一個值，以便與另一個值進行檢查：

last_return = Operators.CONCAT(256, *last_return)

約束條件

您可以在全域或針對特定狀態使用約束條件。

全域約束條件

使用 m.constrain(constraint) 加入全域約束條件。 例如，您可以從一個符號地址呼叫合約，並將此地址限制為特定值：

symbolic_address = m.make_symbolic_value()
m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
m.transaction(caller=user_account,
              address=contract_account,
              data=m.make_symbolic_buffer(320),
              value=0)

狀態約束條件

使用 state.constrain(constraint) (opens in a new tab) 將約束條件加入特定狀態。 它可用於在探索狀態後對其進行約束，以檢查其上的某些屬性。

檢查約束條件

使用 solver.check(state.constraints) 來了解約束條件是否仍然可行。 例如，以下內容將約束 symbolic_value 不等於 65，並檢查狀態是否仍然可行：

state.constrain(symbolic_var != 65)
if solver.check(state.constraints):
    # 狀態是可行的

摘要：加入約束條件

將約束條件加入先前的程式碼中，我們得到：

您可以在 example_run.py (opens in a new tab) 中找到上述所有程式碼