エキドナを使用してスマート・コントラクトをテストする方法

インストール

エキドナは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/training

バイナリ

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

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

エキドナはプロパティベースのファザーであり、以前のブログ記事（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)など）は、バグを見つけるための効率的なツールとして知られています。

純粋にランダムな入力の生成を超えて、優れた入力を生成するための多くの手法や戦略があります。これには以下が含まれます:

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

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

エキドナは、QuickCheck (opens in a new tab)に強く影響を受けたプロパティベースのファジングという特定のファザーのファミリーに属しています。クラッシュを見つけようとする従来のファザーとは対照的に、エキドナはユーザー定義の不変条件を破ろうとします。

スマート・コントラクトにおいて、不変条件はSolidityの関数であり、コントラクトが到達する可能性のある不正確または無効な状態を表すことができます。これには以下が含まれます:

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

エキドナを使用したプロパティのテスト

エキドナを使用してスマート・コントラクトをテストする方法を見ていきます。ターゲットは以下のスマート・コントラクトtoken.sol (opens in a new tab)です:

contract Token{
  mapping(address => uint) public balances;
  function airdrop() public{
      balances[msg.sender] = 1000;
  }
  function consume() public{
      require(balances[msg.sender]>0);
      balances[msg.sender] -= 1;
  }
  function backdoor() public{
      balances[msg.sender] += 1;
  }
}

このトークンには以下のプロパティが必要であると仮定します:

• 誰でも最大1000トークンを持つことができる
• トークンは転送できない（ERC-20トークンではない）

プロパティの記述

エキドナのプロパティはSolidityの関数です。プロパティは以下の条件を満たす必要があります:

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

エキドナは以下を行います:

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

以下のプロパティは、呼び出し元が1000トークンを超えて持っていないことを確認します:

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

継承を使用して、コントラクトをプロパティから分離します:

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

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

コントラクトの初期化

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

エキドナにはいくつかのアドレスが指定されています:

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

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

エキドナの実行

エキドナは以下で起動します:

echidna-test contract.sol

contract.solに複数のコントラクトが含まれている場合は、ターゲットを指定できます:

echidna-test contract.sol --contract MyContract

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

以下は、この例でのエキドナの実行のまとめです:

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

echidna-test testtoken.sol --contract TestToken
...

echidna_balance_under_1000: failed!💥
  Call sequence, shrinking (1205/5000):
    airdrop()
    backdoor()

...

エキドナは、backdoorが呼び出されるとプロパティが違反されることを発見しました。

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

ファジング対象の関数をフィルタリングする方法を見ていきます。 ターゲットは以下のスマート・コントラクトです:

contract C {
  bool state1 = false;
  bool state2 = false;
  bool state3 = false;
  bool state4 = false;

  function f(uint x) public {
    require(x == 12);
    state1 = true;
  }

  function g(uint x) public {
    require(state1);
    require(x == 8);
    state2 = true;
  }

  function h(uint x) public {
    require(state2);
    require(x == 42);
    state3 = true;
  }

 function i() public {
    require(state3);
    state4 = true;
  }

  function reset1() public {
    state1 = false;
    state2 = false;
    state3 = false;
    return;
  }

  function reset2() public {
    state1 = false;
    state2 = false;
    state3 = false;
    return;
  }

  function echidna_state4() public returns (bool) {
    return (!state4);
  }
}

この小さな例では、状態変数を変更するために特定のトランザクションのシーケンスを見つけることをエキドナに強制します。 これはファザーにとっては困難です（マンティコア (opens in a new tab)のようなシンボリック実行ツールの使用が推奨されます）。 エキドナを実行してこれを確認できます:

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

関数のフィルタリング

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

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

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

関数をフィルタリングする別のアプローチは、ホワイトリストに登録された関数をリストすることです。これを行うには、この設定ファイルを使用できます:

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

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

エキドナの実行

設定ファイルblacklist.yamlを使用してエキドナを実行するには:

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

エキドナは、プロパティを反証するトランザクションのシーケンスをほぼ即座に見つけます。

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

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

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

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

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

エキドナでSolidityのアサートをテストする方法

この短いチュートリアルでは、エキドナを使用してコントラクト内のアサーションチェックをテストする方法を示します。次のようなコントラクトがあると仮定しましょう:

contract Incrementor {
  uint private counter = 2**200;

  function inc(uint val) public returns (uint){
    uint tmp = counter;
    counter += val;
    // tmp <= counter
    return (counter - tmp);
  }
}

アサーションの記述

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

contract Incrementor {
  uint private counter = 2**200;

  function inc(uint val) public returns (uint){
    uint tmp = counter;
    counter += val;
    assert (tmp <= counter);
    return (counter - tmp);
  }
}

エキドナの実行

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

checkAsserts: true

このコントラクトをエキドナで実行すると、期待される結果が得られます:

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

ご覧のとおり、エキドナはinc関数でいくつかのアサーションの失敗を報告します。関数ごとに複数のアサーションを追加することは可能ですが、エキドナはどのアサーションが失敗したかを判別できません。

アサーションを使用するタイミングと方法

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

function f(..) public {
    // 複雑なコード
    ...
    assert (condition);
    ...
}

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

function echidna_assert_after_f() public returns (bool) {
    f(..);
    return(condition);
}

ただし、いくつかの問題があります:

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

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

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

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

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

以下は、この例でのエキドナの実行のまとめです:

contract Incrementor {
  uint private counter = 2**200;

  function inc(uint val) public returns (uint){
    uint tmp = counter;
    counter += val;
    assert (tmp <= counter);
    return (counter - tmp);
  }
}

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

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

エキドナのコーパスの収集と変更

エキドナを使用してトランザクションのコーパスを収集し、使用する方法を見ていきます。ターゲットは以下のスマート・コントラクトmagic.sol (opens in a new tab)です:

contract C {
  bool value_found = false;
  function magic(uint magic_1, uint magic_2, uint magic_3, uint magic_4) public {
    require(magic_1 == 42);
    require(magic_2 == 129);
    require(magic_3 == magic_4+333);
    value_found = true;
    return;
  }

  function echidna_magic_values() public returns (bool) {
    return !value_found;
  }

}

この小さな例では、状態変数を変更するために特定の値を見つけることをエキドナに強制します。これはファザーにとっては困難です （マンティコア (opens in a new tab)のようなシンボリック実行ツールの使用が推奨されます）。 エキドナを実行してこれを確認できます:

echidna-test magic.sol
...

echidna_magic_values: passed! 🎉

Seed: 2221503356319272685

ただし、このファジングキャンペーンを実行する際に、エキドナを使用してコーパスを収集することは依然として可能です。

コーパスの収集

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

mkdir corpus-magic

そして、エキドナの設定ファイル (opens in a new tab) config.yamlを作成します:

coverage: true
corpusDir: "corpus-magic"

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

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

エキドナは依然として正しいマジックバリューを見つけることができませんが、収集されたコーパスを確認することはできます。 たとえば、これらのファイルの1つは次のとおりでした:

[
  {
    "_gas'": "0xffffffff",
    "_delay": ["0x13647", "0xccf6"],
    "_src": "00a329c0648769a73afac7f9381e08fb43dbea70",
    "_dst": "00a329c0648769a73afac7f9381e08fb43dbea72",
    "_value": "0x0",
    "_call": {
      "tag": "SolCall",
      "contents": [
        "magic",
        [
          {
            "contents": [
              256,
              "93723985220345906694500679277863898678726808528711107336895287282192244575836"
            ],
            "tag": "AbiUInt"
          },
          {
            "contents": [256, "334"],
            "tag": "AbiUInt"
          },
          {
            "contents": [
              256,
              "68093943901352437066264791224433559271778087297543421781073458233697135179558"
            ],
            "tag": "AbiUInt"
          },
          {
            "tag": "AbiUInt",
            "contents": [256, "332"]
          }
        ]
      ]
    },
    "_gasprice'": "0xa904461f1"
  }
]

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

コーパスのシード

エキドナがmagic関数を処理するには、いくつかの助けが必要です。入力をコピーし、それに適したパラメータを使用するように変更します:

cp corpus/2712688662897926208.txt corpus/new.txt

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

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

今回は、プロパティが即座に違反されることを発見しました。

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

エキドナを使用してガス消費量の多いトランザクションを見つける方法を見ていきます。ターゲットは以下のスマート・コントラクトです:

contract C {
  uint state;

  function expensive(uint8 times) internal {
    for(uint8 i=0; i < times; i++)
      state = state + i;
  }

  function f(uint x, uint y, uint8 times) public {
    if (x == 42 && y == 123)
      expensive(times);
    else
      state = 0;
  }

  function echidna_test() public returns (bool) {
    return true;
  }

}

ここで、expensiveは大量のガスを消費する可能性があります。

現在、エキドナには常にテストするプロパティが必要です。ここではechidna_testは常にtrueを返します。 エキドナを実行してこれを確認できます:

echidna-test gas.sol
...
echidna_test: passed! 🎉

Seed: 2320549945714142710

ガス消費量の測定

エキドナでガス消費量の測定を有効にするには、設定ファイルconfig.yamlを作成します:

estimateGas: true

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

seqLen: 2
estimateGas: true

エキドナの実行

設定ファイルを作成したら、次のようにエキドナを実行できます:

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)によって提供される推定値です。

ガスを削減する呼び出しのフィルタリング

上記のファジングキャンペーン中に呼び出す関数のフィルタリングに関するチュートリアルでは、テストから一部の関数を削除する方法を示しています。
これは、正確なガスの推定値を取得するために重要になる場合があります。 以下の例を考えてみましょう:

contract C {
  address [] addrs;
  function push(address a) public {
    addrs.push(a);
  }
  function pop() public {
    addrs.pop();
  }
  function clear() public{
    addrs.length = 0;
  }
  function check() public{
    for(uint256 i = 0; i < addrs.length; i++)
      for(uint256 j = i+1; j < addrs.length; j++)
        if (addrs[i] == addrs[j])
          addrs[j] = address(0x0);
  }
  function echidna_test() public returns (bool) {
      return true;
  }
}

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

echidna-test pushpop.sol --config config.yaml
...
pop used a maximum of 10746 gas
...
check used a maximum of 23730 gas
...
clear used a maximum of 35916 gas
...
push used a maximum of 40839 gas

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

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

echidna-test pushpop.sol --config config.yaml
...
push used a maximum of 40839 gas
...
check used a maximum of 1484472 gas

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

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

estimateGas: true

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

ファジングキャンペーンが終了すると、エキドナはすべての関数について最大ガス消費量のシーケンスを報告します。