メインコンテンツへスキップ

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

Solidityスマートコントラクトセキュリティテストファジング
上級
Trailofbits
セキュアなコントラクトの構築(opens in a new tab)
2020年4月10日
22 分の読書 minute read

インストール

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 トークンを所持できる
  • このトークン（ERC-20 トークンではない）は、送信不可である

プロパティを記述する

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"]

関数を絞り込むもう一つの方法は、ホワイトリストに含まれる関数を列挙することです。 これには、設定ファイルを以下のように指定します：

1filterBlacklist: false
2filterFunctions: ["f", "g", "h", "i"]
  • filterBlacklistの初期値はtrueです。
  • 絞り込みは、名前のみ（パラメータなし）で実行されます。 f()とf(uint256)の両方が含まれる場合、"f"で絞り込むと両方の関数がヒットします。

Echidna を実行する

設定ファイル blacklist.yaml に従って Echidna を実行するには、以下のようにします：

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

Echidna は、プロパティを false にするトランザクションのシーケンスを瞬時に特定します。

対象の関数を絞り込む作業のまとめ

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 つの関数に対し複数のアサーションを含めることは可能ですが、どのアサーションが失敗したのか区別できなくなります。

アサーションをいつ、どのように使用すべきか

アサーションは、特にチェックしたい条件が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 では require を検出できません。（ただしこの場合でも、コントラクトは元に戻されます）。

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

以下は、この例における 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 はまだ適切な magic 値を特定できませんが、収集したコーパスを確認することはできます。 例えば、以下のようなファイルが収集されました：

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]
すべて表示
 コピー

言うまでもなく、この入力はプロパティ違反をトリガーしません。 しかし、次のステップでこれを修正することができます。

コーパスをシードする

Echidna をmagic関数に対応するように設定する必要があります。 この入力が適切なパラメータを使用できるように、コピーし、変更します。

$ cp corpus/2712688662897926208.txt corpus/new.txt

magic(42,129,333,0)を呼び出せるようにnew.txtを変更します。 その上で、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 を実行して、これを確認します：

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

ガス消費量を測定する

Ethidna でガスの消費量を確認できるようにするには、 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
すべて表示

ガス量を削減する呼び出しを対象外にする

ファジング実行時に呼び出す関数を絞り込む方法のチュートリアルでは、特定の関数をテストの対象外にする方法を示しました。
この作業は、ガス量を正確に見積もる上で非常に重要です。 以下の例を検討してみましょう：

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 がすべての関数を呼び出せる場合、ガス代が高いトランザクションを見つけることは困難になるでしょう。

1$ echidna-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"]
1$ echidna-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 は、ファジングを実行した後、各関数ごとにガス消費量が最大となるシーケンスを報告します。

最終編集者: @tsukky(opens in a new tab), 2023年8月15日

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