Manticoreを使ってスマートコントラクトのバグを特定する方法

Solidityスマートコントラクトセキュリティテストフォーマルな検証

上級

Trailofbits

セキュアなコントラクトの構築(opens in a new tab)

2020年1月13日

19 分の読書 minute read

このチュートリアルでは、Manticoreを使用してスマートコントラクトのバグを自動で特定する方法を学びます。

インストール

Manticoreを使用するには、Python 3.6 が必要です。 pipでインストールすることも、Dockerを使用してインストールすることもできます。

DockerでManticoreをインストールする場合

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でManticoreをインストールする場合

pip3 install --user manticore

solc 0.5.11を推奨します。

スクリプトを実行する

Python 3では、以下のPythonスクリプトを実行します：

python3 script.py

動的シンボリック実行の概要

動的シンボリック実行とは何か

動的シンボリック実行（DSE）は、高度な意味認識に基づき状態空間を探索するプログラム解析手法です。この手法は、path predicatesと呼ばれる数式で表される「プログラム・パス」を発見するものです。概念的には、この手法は2つのステップによりパス述語を操作します：

プログラムの入力に対する制約を参照して、プログラム・パスを構築します。
プログラム・パスは、関連パスを実行させるプログラムの入力を生成します。

このアプローチでは、具体値で実行する際に、特定されたすべてのプログラムの状態をトリガーしうるという意味で誤検出が発生しません。例えば、解析において整数のオーバーフローが特定された場合、このオーバーフローは確実に再現可能です。

パス述語の具体例

DSEの仕組みを理解するために、以下の例を考えてみましょう。

1function f(uint a){
2
3  if (a == 65) {
4      // A bug is present
5  }
6
7}
 コピー

f()には2つのパスが含まれているため、DSEにより、2つの異なるパス述語が構築されます。

第1のパス： a == 65
第2のパス： Not (a == 65)

それぞれのパス述語は、いわゆるSMTソルバー(opens in a new tab)に投入できる数式であり、SMTソルバーはこの等式を解決しようとします。 第1のパスでは、ソルバーは、このパスがa = 65で探索可能だと返します。 第2のパスでは、ソルバーは、aに対し、65以外の任意の値を与えることができます（例： a = 0）。

プロパティを検証する

Manticoreでは、各パスの実行全体を完全に制御できます。このため、ほぼすべての事項に対して任意の制限を加えることができます。この制御を通じて、コントラクトのプロパティを作成することができます。

次の例を考えてみましょう：

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // no overflow protection
3  return c;
4}
 コピー

この関数を探索するには、1つのパスしか存在しません。

パス1： c = a + b

Manticoreを使用することで、オーバーフローの有無を確認し、パス述語に制限を加えられます。

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

上記の述語パスが実行可能となるaおよびbの値を見つけられる場合、オーバーフローが特定できたことになります。例えば、ソルバーは、a = 10 , b = MAXUINT256という入力を生成できます。

次に、上記を修正したコードを見てみましょう：

1function safe_add(uint a, uint b) returns(uint c){
2  c = a + b;
3  require(c>=a);
4  require(c>=b);
5  return c;
6}
 コピー

オーバーフローを確認するために数式は、以下のようになるでしょう：

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

この数式は解くことができません。言い換えれば、safe_addにおいて、cの値が常に増加することを証明しています。

このように、DSEはコード上の任意の制限について検証できるパワフルなツールです。

Manticoreで実行する

以下に、Manticore APIを用いて、スマートコントラクトを探索する方法を紹介します。対象となるスマートコントラクトは、example.sol(opens in a new tab)です。

1pragma solidity >=0.4.24 <0.6.0;
2
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
すべて表示
 コピー

スタンドアロンの探索を実行する

以下のコマンドから、スマートコントラクト上で直接Manticoreを実行できます（projectは、Solidityファイルでもプロジェクトディレクトリでも構いません）。

$ manticore project

実行すると、以下のようなテストケースが出力されます（順番は異なる可能性があります）：

1...
2... m.c.manticore:INFO: Generated testcase No. 0 - STOP
3... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
4... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
5... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
6... m.c.manticore:INFO: Generated testcase No. 4 - STOP
7... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
8... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
9... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
10...
すべて表示

Manticoreは、追加情報が提供されない限り、新規のシンボリック・トランザクションを使って、コントラクト上で新規パスが発見されるまでコントラクトを探索します。 Manticoreでは、トランザクションが失敗した場合（例：状態が元に戻された後）は、新規のトランザクションを実行しません。

Manticoreでは、 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)」は、f が 65 以外の値で呼び出されたことを意味します。

ご覧のように、Manticoreでは、すべての成功した／元に戻されたトランザクションにつき、固有のテストケースを生成します。

高速な探索を行いたい場合は、--quick-modeフラグを使用してください（バグ検出、ガス代計算等が省略されます）。

Manticore APIを使ってスマートコントラクトを操作する

このセクションでは、Manticore Python APIを使ってスマートコントラクトを操作する方法について詳しく説明します。 Pythonの拡張子である*.pyを持つ新規ファイルを作成し、APIコマンド（基本知識については以下で説明します）をファイルに追加して必要なコードを書いてから、$ python3 *.pyコマンドで実行します。また、Pythonのコンソールから直接コマンドを実行することもできます。コンソールを起動する際のコマンドは、$ python3です。

アカウントを作成する

まず、以下のコマンドを持つ新規のブロックチェーンを立ち上げる必要があります。

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
 コピー

m.create_account(opens in a new tab)により、コントラクトではないアカウントが作成されます。

1user_account = m.create_account(balance=1000)
 コピー

Solidityで作成したコントラクトについては、m.solidity_create_contract(opens in a new tab)でデプロイします。

1source_code = '''
2pragma solidity >=0.4.24 <0.6.0;
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
10'''
11# Initiate the contract
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
すべて表示
 コピー

まとめ

m.create_account(opens in a new tab)とm.solidity_create_contract(opens in a new tab)を使用して、ユーザーアカウントとコントラクトアカウントを作成できます。

トランザクションを実行する

Manticoreは、2種類のトランザクションに対応しています：

生トランザクション：すべての関数を探索します。
名前付きトランザクション：1つの関数だけを探索します。

生トランザクション

生トランザクションは、m.transaction(opens in a new tab)で実行されます。

1m.transaction(caller=user_account,
2              address=contract_account,
3              data=data,
4              value=value)
 コピー

呼び出し元、アドレス、データ、トランザクションの値は、具体値あるいはシンボリック値のどちらでも構いません：

m.make_symbolic_value(opens in a new tab)は、シンボリック値を生成します。
m.make_symbolic_buffer(size)(opens in a new tab)は、シンボリックなバイト配列を生成します。

以下の例を確認してください：

1symbolic_value = m.make_symbolic_value()
2symbolic_data = m.make_symbolic_buffer(320)
3m.transaction(caller=user_account,
4              address=contract_address,
5              data=symbolic_data,
6              value=symbolic_value)
 コピー

データがシンボリック値の場合、Manticoreは、トランザクションの実行時にコントラクトに含まれるすべての関数を探索します。関数がどのように選択されるかを理解するには、Hands on the Ethernaut CTF(opens in a new tab)の記事におけるフォールバック関数についての説明を参照してください。

名前付きトランザクション

関数は、名前から実行できます。 f(uint var)につき、シンボリック値を用いて、user_accountから、0 etherで実行する場合、以下を使用します：

1symbolic_var = m.make_symbolic_value()
2contract_account.f(symbolic_var, caller=user_account, value=0)
 コピー

トランザクションのvalueを指定しない場合、デフォルトでは0になります。

まとめ

トランザクションの引数は、具体値またはシンボリック値のどちらでもよい。
生トランザクションは、すべての関数を探索する。
関数は、名前で呼び出すことができる。

ワークスペース

m.workspaceは、生成されたすべてのファイルにおける出力ディレクトリとして使用されるディレクトリです。

1print("Results are in {}".format(m.workspace))
 コピー

探索を終了する

探索を停止するには、m.finalize()(opens in a new tab)を使用します。このメソッドが呼び出された時点で、さらにトランザクションは送信されなくなり、Manticoreは探索済みの各パスにつきテストケースを生成します。

Manticoreを使った実行のまとめ

上記のステップをまとめると、以下のようになります：

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14print("Results are in {}".format(m.workspace))
15m.finalize() # stop the exploration
すべて表示
 コピー

紹介したすべてのコードは、example_run.py(opens in a new tab)でアクセスできます。

スローイングパスを取得する

次に、 f()において例外を発生させるパスに対する、特定のインプットを生成します。ここでも、対象となるスマートコントラクトはexample.sol(opens in a new tab)です。

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
 コピー

状態情報を使用する

実行された各パスには、それぞれのブロックチェーンの状態が含まれています。状態は、readyまたはkilledのどちらかです。killedは、THROWまたはREVERTに達したことを意味します。

m.ready_states(opens in a new tab)：readyに該当する状態のリスト（REVERT/INVALIDを実行しなかった状態）
m.killed_states(opens in a new tab)：killedに該当する状態のリスト
m.all_states(opens in a new tab)：すべての状態

1for state in m.all_states:
2    # do something with state
 コピー

状態情報は、アクセス可能です。以下の例をご覧ください：

state.platform.get_balance(account.address)：アカウント残高
state.platform.transactions：トランザクションのリスト
state.platform.transactions[-1].return_data：最後のトランザクションで返されたデータ

最後のトランザクションによって返されるデータは配列ですが、以下のようにABI.deserializeで値に変換できます：

1data = state.platform.transactions[0].return_data
2data = ABI.deserialize("uint", data)
 コピー

テストケースの生成方法

テストケースを生成するには、「m.generate_testcase(state, name)(opens in a new tab)」を使用します。

1m.generate_testcase(state, 'BugFound')
 コピー

まとめ

状態は、m.all_statesでイテレートできる
state.platform.get_balance(account.address)は、アカウント残高を返す
state.platform.transactionsは、トランザクションのリストを返す
transaction.return_dataは、返されたデータを示す
m.generate_testcase(state, name)は、状態に対する入力を生成する

スローイングパス取得のまとめ

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14## Check if an execution ends with a REVERT or INVALID
15for state in m.terminated_states:
16    last_tx = state.platform.transactions[-1]
17    if last_tx.result in ['REVERT', 'INVALID']:
18        print('Throw found {}'.format(m.workspace))
19        m.generate_testcase(state, 'ThrowFound')
すべて表示
 コピー

紹介したすべてのコードは、example_run.py(opens in a new tab)でアクセスできます。

terminated_stateが返したすべての状態は結果の値がREVERTまたはINVALIDであるため、上記よりも簡略なスクリプトを作成することもできました。上記のスクリプト例は、Manticore APIの操作方法を説明することを目的としたものです。

制約を追加する

次に、探索を制限する方法について確認しましょう。ここでは、f()のドキュメンテーションにおいて、この関数は決してa == 65で呼び出されることはないと記載されていると想定します。このため、a == 65のバグは、実際にはバグではありません。ここでも、対象のスマートコントラクトはexample.sol(opens in a new tab)です。

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
 コピー

演算子

演算子(opens in a new tab)モジュールは、制約を容易に操作する上で役立ちます。特に、以下の操作を提供します：

Operators.AND
Operators.OR
Operators.UGT（符号なし大なり）
Operators.UGE（符号なし以上）
Operators.ULT（符号なし小なり）
Operators.ULE（符号なし、以下）

このモジュールをインポートするには、以下を使用します：

1from manticore.core.smtlib import Operators
 コピー

Operators.CONCATは、配列に値を連結するために使用します。例えば、トランザクションのreturn_dataは、他の値に対して検証可能な値に変更する必要があります：

1last_return = Operators.CONCAT(256, *last_return)
 コピー

制約

制約の対象は、グローバルあるいは特定の状態のみのどちらでも構いません。

グローバル制約

グローバル制約を追加するには、m.constraint(constraint)を使用します。例えば以下のように、シンボリックアドレスからコントラクトを呼び出し、このアドレスを特定の値に制限することができます：

1symbolic_address = m.make_symbolic_value()
2m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
3m.transaction(caller=user_account,
4              address=contract_account,
5              data=m.make_symbolic_buffer(320),
6              value=0)
 コピー

状態に対する制約

特定の状態に対して制約を追加するには、state.constrain(constraint)(opens in a new tab)を使用します。特定の状態における一部のプロパティをチェックしてから、状態に制限を追加することができます。

制約を確認する

制約が実行可能かどうかを確認するには、solver.check(state.constraints)を使用します。例えば以下では、symbolic_valueが「65」以外の値でなければならないという制約を追加した上で、状態が実行可能かどうかをチェックします。

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # state is feasible
 コピー

制約追加のまとめ

これまでのコードに制約を追加すると、以下のようになります：

1from manticore.ethereum import ManticoreEVM
2from manticore.core.smtlib.solver import Z3Solver
3
4solver = Z3Solver.instance()
5
6m = ManticoreEVM()
7
8with open("example.sol") as f:
9    source_code = f.read()
10
11user_account = m.create_account(balance=1000)
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
13
14symbolic_var = m.make_symbolic_value()
15contract_account.f(symbolic_var)
16
17no_bug_found = True
18
19## Check if an execution ends with a REVERT or INVALID
20for state in m.terminated_states:
21    last_tx = state.platform.transactions[-1]
22    if last_tx.result in ['REVERT', 'INVALID']:
23        # we do not consider the path were a == 65
24        condition = symbolic_var != 65
25        if m.generate_testcase(state, name="BugFound", only_if=condition):
26            print(f'Bug found, results are in {m.workspace}')
27            no_bug_found = False
28
29if no_bug_found:
30    print(f'No bug found')
すべて表示
 コピー

ここで紹介したすべてのコードは、example_run.py(opens in a new tab)からアクセスできます。

最終編集者: @lukassim(opens in a new tab), 2024年4月26日