Echidnaを使用してスマートコントラクトをテストする方法

Solidity

スマートコントラクト

セキュリティ

テスト

ファジング

上級

Trailofbits

Building secure contracts

2020年4月10日

21 分の読書

インストール

Echidnaは、Dockerまたはコンパイル済みのバイナリを使用してインストールします。

DockerによるEchidna

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/training

バイナリ

https://github.com/crytic/echidna/releases/tag/v1.4.0.0 (opens in a new tab)

プロパティベースファジング入門

Echidnaはプロパティベースのファザーであり、以前のブログ投稿(1 (opens in a new tab)、2 (opens in a new tab)、3 (opens in a new tab))で説明しています。

ファジング

ファジング (opens in a new tab)は、セキュリティコミュニティでよく知られているテクニックです。プログラム内のバグを見つけるために、ある程度ランダムな入力を生成するものです。従来のソフトウェア用のファザー（AFL (opens in a new tab)やLibFuzzer (opens in a new tab)など）は、バグを見つけるための効率的なツールとして知られています。

純粋にランダムな入力生成以外に、適切な入力を生成するための多くのテクニックや戦略があります。以下に例を挙げます。

各実行からフィードバックを取得し、それを使用して生成をガイドします。例えば、新しく生成された入力が新しいパスの発見につながる場合、それに近い新しい入力を生成することは理にかなっています。
構造的制約を尊重して入力を生成する。例えば、入力にチェックサム付きのヘッダーが含まれている場合、ファザーにチェックサムを検証する入力を生成させるのは理にかなっています。
既知の入力を使用して新しい入力を生成する：有効な入力の大規模なデータセットにアクセスできる場合、ファザーはゼロから生成を開始するのではなく、それらから新しい入力を生成できます。これらは通常、_シード_と呼ばれます。

プロパティベースファジング

Echidnaは、QuickCheck (opens in a new tab)に強くインスパイアされたプロパティベースファジングという、ファザーの特定の種類に属します。クラッシュを見つけようとする従来のファザーとは対照的に、Echidnaはユーザー定義の不変条件を破ろうとします。

スマートコントラクトにおける不変条件とは、コントラクトが到達しうる不正または無効な状態を表すSolidity関数であり、次のようなものが含まれます。

不正なアクセス制御：攻撃者がコントラクトの所有者になる。
不正な状態マシン：コントラクトが一時停止している間にトークンを転送できる。
不正な算術演算：ユーザーが残高をアンダーフローさせ、無制限の無料トークンを取得できる。

Echidnaでプロパティをテストする

Echidnaを使ってスマートコントラクトをテストする方法を見ていきましょう。対象は、次のスマートコントラクトtoken.sol (opens in a new tab)です。

1contract Token{
2  mapping(address => uint) public balances;
3  function airdrop() public{
4      balances[msg.sender] = 1000;
5  }
6  function consume() public{
7      require(balances[msg.sender]>0);
8      balances[msg.sender] -= 1;
9  }
10  function backdoor() public{
11      balances[msg.sender] += 1;
12  }
13}
すべて表示

このトークンは、以下のプロパティを持つと想定します。

誰でも最大1000トークンを保有できます
このトークンは転送できません（ERC20トークンではありません）

プロパティを記述する

Echidnaのプロパティは、Solidityの関数です。プロパティは、以下の条件を満たす必要があります。

引数を持たない
成功した場合にtrueを返す
名前がechidnaで始まる

Echidnaは、以下を実行します。

プロパティをテストするために、任意のトランザクションを自動的に生成します。
プロパティがfalseを返すか、エラーをスローするトランザクションを報告します。
プロパティ呼び出し時の副作用を破棄する（つまり、プロパティが状態変数を変更した場合、テスト後にその変更は破棄されます）

以下のプロパティは、呼び出し元が1000トークンを超えて保有していないことをチェックします。

1function echidna_balance_under_1000() public view returns(bool){
2      return balances[msg.sender] <= 1000;
3}

継承を使って、コントラクトとプロパティを分離します。

1contract TestToken is Token{
2      function echidna_balance_under_1000() public view returns(bool){
3            return balances[msg.sender] <= 1000;
4      }
5  }

token.sol (opens in a new tab)はプロパティを実装し、トークンを継承します。

コントラクトの初期化

Echidnaには、引数のないコンストラクタが必要です。コントラクトに特定の初期化が必要な場合、コンストラクタで行う必要があります。

Echidnaには、いくつかの特定のアドレスが含まれます。

0x00a329c0648769A73afAc7F9381E08FB43dBEA72はコンストラクタを呼び出します。
0x10000、0x20000、および0x00a329C0648769a73afAC7F9381e08fb43DBEA70は、他の関数をランダムに呼び出します。

この例では特定の初期化は必要ないため、コンストラクタは空になります。

Echidnaの実行

Echidnaは次のように起動します。

echidna-test contract.sol

contract.solに複数のコントラクトが含まれる場合、対象を指定できます。

echidna-test contract.sol --contract MyContract

まとめ：プロパティのテスト

以下は、この例におけるEchidnaの実行をまとめたものです。

1contract TestToken is Token{
2    constructor() public {}
3        function echidna_balance_under_1000() public view returns(bool){
4          return balances[msg.sender] <= 1000;
5        }
6  }

echidna-test testtoken.sol --contract TestToken
...
echidna_balance_under_1000: failed!💥
  Call sequence, shrinking (1205/5000):
    airdrop()
    backdoor()
...
すべて表示

Echidnaは、backdoorが呼び出された場合にプロパティが違反することを発見しました。

ファジングキャンペーン中に呼び出す関数をフィルタリングする

ファジング対象となる関数をフィルタリングする方法を見ていきましょう。対象は、次のスマートコントラクトです。

1contract C {
2  bool state1 = false;
3  bool state2 = false;
4  bool state3 = false;
5  bool state4 = false;
6
7  function f(uint x) public {
8    require(x == 12);
9    state1 = true;
10  }
11
12  function g(uint x) public {
13    require(state1);
14    require(x == 8);
15    state2 = true;
16  }
17
18  function h(uint x) public {
19    require(state2);
20    require(x == 42);
21    state3 = true;
22  }
23
24 function i() public {
25    require(state3);
26    state4 = true;
27  }
28
29  function reset1() public {
30    state1 = false;
31    state2 = false;
32    state3 = false;
33    return;
34  }
35
36  function reset2() public {
37    state1 = false;
38    state2 = false;
39    state3 = false;
40    return;
41  }
42
43  function echidna_state4() public returns (bool) {
44    return (!state4);
45  }
46}
すべて表示

この簡単な例は、状態変数を変更する特定のトランザクションのシーケンスをEchidnaに見つけさせるものです。これはファザーにとって困難です（Manticore (opens in a new tab)のようなシンボリック実行ツールの使用が推奨されます）。 Echidnaを実行して、これを確認できます。

echidna-test multi.sol
...
echidna_state4: passed! 🎉
Seed: -3684648582249875403

関数のフィルタリング

2つのリセット関数（reset1とreset2）がすべての状態変数をfalseに設定するため、Echidnaがこのコントラクトをテストするための正しいシーケンスを見つけるのは困難です。しかし、Echidnaの特別な機能を使用して、リセット関数をブラックリストに登録するか、f、g、 h、i関数のみをホワイトリストに登録することができます。

関数をブラックリストに登録するには、この設定ファイルを使用します。

1filterBlacklist: true
2filterFunctions: ["reset1", "reset2"]

関数をフィルタリングするもう1つのアプローチは、ホワイトリストに登録された関数をリストアップすることです。そのためには、この設定ファイルを使用します。

1filterBlacklist: false
2filterFunctions: ["f", "g", "h", "i"]

filterBlacklistのデフォルト値はtrueです。
フィルタリングは、名前のみ（パラメータなし）で実行されます。 f()とf(uint256)の両方がある場合、フィルタ"f"は両方の関数にマッチします。

Echidnaの実行

Echidnaを構成ファイルblacklist.yamlで実行するには、次のようにします。

echidna-test multi.sol --config blacklist.yaml
...
echidna_state4: failed!💥
  Call sequence:
    f(12)
    g(8)
    h(42)
    i()

Echidnaは、プロパティを偽にするトランザクションのシーケンスをほぼ瞬時に見つけます。

まとめ：関数のフィルタリング

Echidnaは、ファジングキャンペーン中に呼び出す関数を、以下を使用してブラックリストまたはホワイトリストに登録できます。

1filterBlacklist: true
2filterFunctions: ["f1", "f2", "f3"]

echidna-test contract.sol --config config.yaml
...

Echidnaは、filterBlacklistブール値の値に応じて、f1、f2、f3をブラックリストに登録するか、これらのみを呼び出すファジングキャンペーンを開始します。

EchidnaでSolidityのアサーションをテストする方法

この短いチュートリアルでは、Echidnaを使用してコントラクトのアサーションチェックをテストする方法を説明します。以下のようなコントラクトを想定します。

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    // tmp <= counter
8    return (counter - tmp);
9  }
10}
すべて表示

アサーションを記述する

その差を返した後に、tmpがcounter以下であることを確認したいと思います。 Echidnaのプロパティを記述することもできますが、tmpの値をどこかに保存する必要があります。代わりに、このようなアサーションを使用できます。

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
すべて表示

Echidnaの実行

アサーション失敗テストを有効にするには、Echidna設定ファイル (opens in a new tab) config.yamlを作成します。

1checkAsserts: true

このコントラクトをEchidnaで実行すると、期待通りの結果が得られます。

echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: failed!💥
  Call sequence, shrinking (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)
Seed: 1806480648350826486
すべて表示

ご覧のとおり、Echidnaはinc関数でのアサーションの失敗を報告します。 1つの関数に複数のアサーションを追加することは可能ですが、Echidnaはどのアサーションが失敗したかを特定できません。

アサーションを使用する状況とその方法

アサーションは、特にチェック対象の条件が何らかの操作fの正しい使用に直接関連する場合、明示的なプロパティの代替として使用できます。コードの後にアサーションを追加すると、そのコードが実行された直後にチェックが強制的に行われます。

1function f(..) public {
2    // some complex code
3    ...
4    assert (condition);
5    ...
6}
7

対照的に、明示的なEchidnaプロパティを使用すると、トランザクションがランダムに実行され、いつチェックされるかを正確に強制する簡単な方法はありません。この回避策を行うことは依然として可能です。

1function echidna_assert_after_f() public returns (bool) {
2    f(..);
3    return(condition);
4}

しかし、いくつかの問題があります。

fがinternalまたはexternalとして宣言されている場合は失敗します。
fを呼び出すのにどの引数を使用すべきかが不明確です。
fがリバートされると、プロパティは失敗します。

一般に、アサーションの使用方法については、John Regehr氏の推奨事項 (opens in a new tab)に従うことをお勧めします。

アサーションチェック中に副作用を強制しないでください。例：assert(ChangeStateAndReturn() == 1)
明らかなステートメントをアサートしないでください。例えば、varがuintとして宣言されている場合のassert(var >= 0)などです。

最後に、assertの代わりにrequireを使用しないでください。Echidnaはそれを検出できません（ただし、コントラクトはいずれにしてもリバートします）。

まとめ：アサーションチェック

以下は、この例におけるEchidnaの実行をまとめたものです。

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
すべて表示

echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: failed!💥
  Call sequence, shrinking (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)
Seed: 1806480648350826486
すべて表示

Echidnaは、incのアサーションが、この関数が大きな引数で複数回呼び出された場合に失敗する可能性があることを見つけました。

Echidnaコーパスの収集と変更

Echidnaを使ってトランザクションのコーパスを収集し、利用する方法について見ていきましょう。対象は、次のスマートコントラクトmagic.sol (opens in a new tab)です。

1contract C {
2  bool value_found = false;
3  function magic(uint magic_1, uint magic_2, uint magic_3, uint magic_4) public {
4    require(magic_1 == 42);
5    require(magic_2 == 129);
6    require(magic_3 == magic_4+333);
7    value_found = true;
8    return;
9  }
10
11  function echidna_magic_values() public returns (bool) {
12    return !value_found;
13  }
14
15}
すべて表示

この簡単な例では、状態変数を変更するために、Echidnaに特定の値を探索させます。これはファザーにとって困難です（Manticore (opens in a new tab)のようなシンボリック実行ツールの使用が推奨されます）。 Echidnaを実行して、これを確認できます。

echidna-test magic.sol
...
echidna_magic_values: passed! 🎉
Seed: 2221503356319272685

しかし、このファジングキャンペーンの実行中にEchidnaを使用してコーパスを収集することは依然として可能です。

コーパスの収集

コーパス収集を有効にするには、コーパスディレクトリを作成します。

mkdir corpus-magic

そして、Echidna設定ファイル (opens in a new tab)であるconfig.yamlを作成します。

1coverage: true
2corpusDir: "corpus-magic"

これでツールを実行し、収集したコーパスを確認できます。

echidna-test magic.sol --config config.yaml

Echidnaはまだ正しいマジック値を見つけることができませんが、収集したコーパスを見ることができます。例えば、これらのファイルの1つは次のとおりでした。

1[
2  {
3    "_gas'": "0xffffffff",
4    "_delay": ["0x13647", "0xccf6"],
5    "_src": "00a329c0648769a73afac7f9381e08fb43dbea70",
6    "_dst": "00a329c0648769a73afac7f9381e08fb43dbea72",
7    "_value": "0x0",
8    "_call": {
9      "tag": "SolCall",
10      "contents": [
11        "magic",
12        [
13          {
14            "contents": [
15              256,
16              "93723985220345906694500679277863898678726808528711107336895287282192244575836"
17            ],
18            "tag": "AbiUInt"
19          },
20          {
21            "contents": [256, "334"],
22            "tag": "AbiUInt"
23          },
24          {
25            "contents": [
26              256,
27              "68093943901352437066264791224433559271778087297543421781073458233697135179558"
28            ],
29            "tag": "AbiUInt"
30          },
31          {
32            "tag": "AbiUInt",
33            "contents": [256, "332"]
34          }
35        ]
36      ]
37    },
38    "_gasprice'": "0xa904461f1"
39  }
40]
すべて表示

明らかに、この入力はプロパティの失敗をトリガーしません。しかし、次のステップでは、そのためにこれを変更する方法を見ていきます。

コーパスのシーディング

magic関数を扱うために、Echidnaには少し助けが必要です。入力をコピーして変更し、適切なパラメータを使用するようにします。

cp corpus/2712688662897926208.txt corpus/new.txt

new.txtをmagic(42,129,333,0)を呼び出すように変更します。これでEchidnaを再実行できます。

echidna-test magic.sol --config config.yaml
...
echidna_magic_values: failed!💥
  Call sequence:
    magic(42,129,333,0)
Unique instructions: 142
Unique codehashes: 1
Seed: -7293830866560616537
すべて表示

今回は、プロパティが即座に違反していることがわかりました。

ガス消費量の多いトランザクションの発見

Echidnaを使用してガス消費量が多いトランザクションを見つける方法を見ていきましょう。対象は、次のスマートコントラクトです。

1contract C {
2  uint state;
3
4  function expensive(uint8 times) internal {
5    for(uint8 i=0; i < times; i++)
6      state = state + i;
7  }
8
9  function f(uint x, uint y, uint8 times) public {
10    if (x == 42 && y == 123)
11      expensive(times);
12    else
13      state = 0;
14  }
15
16  function echidna_test() public returns (bool) {
17    return true;
18  }
19
20}
すべて表示

ここでexpensiveは大きなガス消費量を持つ可能性があります。

現在、Echidnaは常にテスト対象のプロパティを必要とします。ここではechidna_testが常にtrueを返します。 Echidnaを実行して、これを確認できます。

1echidna-test gas.sol
2...
3echidna_test: passed! 🎉
4
5Seed: 2320549945714142710

ガス消費量の測定

Echidnaでガス消費を有効にするには、設定ファイルconfig.yamlを作成します。

1estimateGas: true

この例では、結果を理解しやすくするために、トランザクションシーケンスのサイズも小さくします。

1seqLen: 2
2estimateGas: true

Echidnaの実行

設定ファイルが作成されたら、次のようにEchidnaを実行できます。

echidna-test gas.sol --config config.yaml
...
echidna_test: passed! 🎉
f used a maximum of 1333608 gas
  Call sequence:
    f(42,123,249) Gas price: 0x10d5733f0a Time delay: 0x495e5 Block delay: 0x88b2
Unique instructions: 157
Unique codehashes: 1
Seed: -325611019680165325
すべて表示

表示されるガスは、HEVM (opens in a new tab)によって提供される推定値です。

ガスを削減する呼び出しの除外

上記の「ファジングキャンペーン中に呼び出す関数のフィルタリング」のチュートリアルでは、テストからいくつかの関数を削除する方法を示しています。
これは、正確なガス見積もりを得るために重要となる場合があります。次の例を考えてみましょう。

1contract C {
2  address [] addrs;
3  function push(address a) public {
4    addrs.push(a);
5  }
6  function pop() public {
7    addrs.pop();
8  }
9  function clear() public{
10    addrs.length = 0;
11  }
12  function check() public{
13    for(uint256 i = 0; i < addrs.length; i++)
14      for(uint256 j = i+1; j < addrs.length; j++)
15        if (addrs[i] == addrs[j])
16          addrs[j] = address(0x0);
17  }
18  function echidna_test() public returns (bool) {
19      return true;
20  }
21}
すべて表示

Echidnaがすべての関数を呼び出せる場合、ガス代が高いトランザクションを簡単に見つけることはできません。

1echidna-test pushpop.sol --config config.yaml
2...
3pop used a maximum of 10746 gas
4...
5check used a maximum of 23730 gas
6...
7clear used a maximum of 35916 gas
8...
9push used a maximum of 40839 gas
すべて表示

これは、コストがaddrsのサイズに依存し、ランダムな呼び出しでは配列がほとんど空のままになる傾向があるためです。しかし、popとclearをブラックリストに登録すると、はるかに良い結果が得られます。

1filterBlacklist: true
2filterFunctions: ["pop", "clear"]

1echidna-test pushpop.sol --config config.yaml
2...
3push used a maximum of 40839 gas
4...
5check used a maximum of 1484472 gas

まとめ：ガス消費量の多いトランザクションの発見

Echidnaは、estimateGas設定オプションを使用して、ガス消費量の多いトランザクションを見つけることができます。

1estimateGas: true

echidna-test contract.sol --config config.yaml
...

ファジングキャンペーンが終了すると、Echidnaは各関数の最大ガス消費量を持つシーケンスを報告します。

最終更新： 2025年10月21日

Echidnaを使用してスマートコントラクトをテストする方法

インストール

DockerによるEchidna

バイナリ

プロパティベースファジング入門

ファジング

プロパティベースファジング

Echidnaでプロパティをテストする

プロパティを記述する

コントラクトの初期化

Echidnaの実行

まとめ：プロパティのテスト

ファジングキャンペーン中に呼び出す関数をフィルタリングする

関数のフィルタリング

Echidnaの実行

まとめ：関数のフィルタリング

EchidnaでSolidityのアサーションをテストする方法

アサーションを記述する

Echidnaの実行

アサーションを使用する状況とその方法

まとめ：アサーションチェック

Echidnaコーパスの収集と変更

コーパスの収集

コーパスのシーディング

ガス消費量の多いトランザクションの発見

ガス消費量の測定

Echidnaの実行

ガスを削減する呼び出しの除外

まとめ：ガス消費量の多いトランザクションの発見

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