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

Solidity

スマートコントラクト

セキュリティ

テスト

形式的検証

上級

Trailofbits

Building secure contracts

2020年1月13日

18 分の読書

このチュートリアルでは、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)は、高度な意味認識に基づき状態空間を探索するプログラム解析手法です。この手法は、パス述語と呼ばれる数式で表される「プログラムパス」の発見に基づいています。概念的には、この手法は2つのステップでパス述語を操作します:

パス述語は、プログラムの入力に対する制約を使用して構築されます。
パス述語は、関連するパスを実行させるプログラム入力を生成するために使用されます。

このアプローチでは、特定されたすべてのプログラム状態が具体的な実行中にトリガーされうるという意味で、誤検出(偽陽性)は発生しません。例えば、解析で整数オーバーフローが発見された場合、その再現性が保証されます。

パス述語の例

DSEがどのように機能するかを理解するために、次の例を考えてみましょう。

1function f(uint a){
2
3  if (a == 65) {
4      // バグが存在します
5  }
6
7}

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

パス1: a == 65
パス2: Not (a == 65)

各パス述語は、いわゆるSMTソルバー (opens in a new tab)に与えることができる数式であり、ソルバーはその方程式を解こうとします。 パス1では、ソルバーは a = 65 でパスを探索できると応答します。 パス2では、ソルバーは a に65以外の任意の値、例えば a = 0 を与えることができます。

プロパティの検証

Manticoreでは、各パスのすべての実行を完全に制御できます。その結果、ほとんどすべてのものに任意の制約を追加できます。この制御により、コントラクトに関するプロパティを作成できます。

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

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // オーバーフロー保護なし
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は、失敗したトランザクションの後(例: revertの後)には、新しいトランザクションを実行しません。

Manticoreは、mcore_*ディレクトリに情報を出力します。このディレクトリには、とりわけ次のものが含まれます。

global.summary: カバレッジとコンパイラの警告
test_XXXXX.summary: カバレッジ、最後の命令、テストケースごとのアカウント残高
test_XXXXX.tx: テストケースごとのトランザクションの詳細リスト

ここでは、Manticoreは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は成功したトランザクションやrevertされたトランザクションごとに、一意のテストケースを生成します。

高速なコード探索を行いたい場合は --quick-mode フラグを使用してください(バグ検出器、ガス計算などを無効にします)。

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# コントラクトを初期化する
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種類のトランザクションをサポートしています。

Rawトランザクション: すべての関数が探索されます
名前付きトランザクション: 1つの関数のみが探索されます

Rawトランザクション

Rawトランザクションは 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になります。

まとめ

トランザクションの引数は具象値またはシンボリック値にできます
Rawトランザクションはすべての関数を探索します
関数は名前で呼び出すことができます

ワークスペース

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() # 探索を停止
すべて表示

上記のすべてのコードは 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): 準備完了状態のリスト(REVERT/INVALIDを実行していない状態)
m.killed_states (opens in a new tab): 強制終了された状態のリスト
m.all_states (opens in a new tab): すべての状態

1for state in m.all_states:
2    # 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## 実行がREVERTまたはINVALIDで終了するかどうかを確認します
15
16for state in m.terminated_states:
17    last_tx = state.platform.transactions[-1]
18    if last_tx.result in ['REVERT', 'INVALID']:
19        print('Throw found {}'.format(m.workspace))
20        m.generate_testcase(state, 'ThrowFound')
すべて表示

上記のすべてのコードは 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) です。

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}

演算子

Operators (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.constrain(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    # 状態は実行可能です

まとめ: 制約の追加

前のコードに制約を追加すると、次のようになります。

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## 実行がREVERTまたはINVALIDで終了するかどうかを確認します
20
21for state in m.terminated_states:
22    last_tx = state.platform.transactions[-1]
23    if last_tx.result in ['REVERT', 'INVALID']:
24        # a == 65のパスは考慮しません
25        condition = symbolic_var != 65
26        if m.generate_testcase(state, name="BugFound", only_if=condition):
27            print(f'Bug found, results are in {m.workspace}')
28            no_bug_found = False
29
30if no_bug_found:
31    print(f'No bug found')
すべて表示

上記のすべてのコードは example_run.py (opens in a new tab) にあります。

最終更新： 2024年4月26日

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

インストール

Docker経由のManticore

pip経由のManticore

スクリプトの実行

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

動的シンボリック実行の簡単な説明

パス述語の例

プロパティの検証

Manticoreでの実行

スタンドアロン探索の実行

APIによるスマートコントラクトの操作

アカウントの作成

まとめ

トランザクションの実行

Rawトランザクション

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

まとめ

ワークスペース

探索の終了

まとめ: Manticoreでの実行

例外をスローするパスの取得

状態情報の使用

テストケースの生成方法

まとめ

まとめ: 例外をスローするパスの取得

制約の追加

演算子

制約

グローバル制約

状態制約

制約のチェック

まとめ: 制約の追加

このチュートリアルは役に立ちましたか?