
Echidnaはバグを食べる奇妙な生き物で、非常に感電しやすい(Jacob Stanleyに謝罪します)
真面目な話、EchidnaはEthereumスマートコントラクトのファジング/プロパティベーステスト用に設計されたHaskellプログラムです。ユーザー定義の述語やSolidityアサーションを反証するために、コントラクトABIに基づいた高度な文法ベースのファジングキャンペーンを使用します。Echidnaはモジュール性を考慮して設計されているため、新しいミューテーションを追加したり、特定のケースで特定のコントラクトをテストするために簡単に拡張できます。
.. そして美しい高解像度のハンドクラフトロゴ。
Echidnaのコア機能はechidnaと呼ばれる実行ファイルで、コントラクトと不変条件(常に真であり続けるべきプロパティ)のリストを入力として受け取ります。各不変条件について、コントラクトへのランダムな呼び出しシーケンスを生成し、不変条件が成立するかどうかをチェックします。不変条件を反証する方法を見つけられれば、それを実現する呼び出しシーケンスを出力します。見つけられなければ、コントラクトが安全であるというある程度の保証が得られます。
不変条件は、名前がechidna_で始まり、引数がなく、ブール値を返すSolidity関数として表現されます。例えば、20を下回ってはならないbalance変数がある場合、コントラクトに次のような追加関数を書くことができます:```solidity
function echidna_check_balance() public returns (bool) {
return(balance >= 20);
}
不変条件を確認するには、次を実行します:```sh
$ echidna myContract.sol
テスト付きのコントラクト例は tests/solidity/basic/flags.sol にあります。実行するには、次を実行してください:```sh $ echidna tests/solidity/basic/flags.sol
Echidna は `echidna_sometimesfalse` を偽造する呼び出しシーケンスを見つけるべきであり、`echidna_alwaystrue` に対する偽造入力を見つけることはできないはずです。
### テストモード
上記の例ではデフォルトの **property** モードを使用していますが、Echidna はいくつかのテストモードをサポートしており、設定ファイルの `testMode` または CLI の `--test-mode` で設定できます:
* **`property`**(デフォルト):`bool` を返す `echidna_` プレフィックス付き関数をテストします。
* **`assertion`**:`assert()` および Foundry の `assertX` ヘルパー(`assertTrue`、`assertEq` など)によるアサーション失敗を検出します。
* **`foundry`**:Foundry スタイルのテストを実行し、その命名規則に従います:`test` プレフィックス付きのユニットテストおよびファズテスト(`testFail` プレフィックス付きのものは revert が期待されます)と、`invariant` または `statefulFuzz` プレフィックス付きのステートフル不変条件です。`check` および `prove` プレフィックス付き関数はシンボリックエントリポイントですが、このモードはファジングキャンペーンであるため、他のテスト関数と同様にファズされます。
* **`verification`**:単一トランザクションを使用してコントラクトの各関数をシンボリックに検証します。`check` および `prove` プレフィックス付き関数は常にエントリポイントとして使用されます。
* **`overflow`**:整数のオーバーフロー/アンダーフローを検出します(Solidity >= 0.8.0)。
* **`optimization`**:`int256` を返す `echidna_` プレフィックス付き関数の戻り値を最大化します(property モードと同じ設定可能なプレフィックスを使用)。
* **`exploration`**:プロパティをチェックせずにカバレッジを収集します。
### カバレッジの収集と可視化
キャンペーン終了後、Echidna は `corpusDir` 設定オプションで指定された特別なディレクトリに、カバレッジを最大化する **コーパス** を保存できます。このディレクトリには 2 つのエントリが含まれます:(1) Echidna で再生可能な JSON ファイルを含む `coverage` という名前のディレクトリ、および (2) カバレッジ注釈付きのソースコードのコピーである `covered.txt` という名前のプレーンテキストファイルです。
`tests/solidity/basic/flags.sol` の例を実行すると、Echidna は `coverage` ディレクトリにシリアライズされたトランザクションのいくつかのファイルと、以下の行を含む `covered.$(date +%s).txt` ファイルを保存します:```text
*r | function set0(int val) public returns (bool){
* | if (val % 100 == 0)
* | flag0 = false;
}
*r | function set1(int val) public returns (bool){
* | if (val % 10 == 0 && !flag0)
* | flag1 = false;
}
私たちのツールは、コーパス内の各実行トレースに以下の「行マーカー」を付けて示します:
* 実行が STOP で終了した場合r 実行が REVERT で終了した場合o 実行が out-of-gas エラーで終了した場合e 実行がその他のエラー(ゼロ除算、アサーション失敗など)で終了した場合Echidna は、crytic-compile を使用して、Foundry、Hardhat、Truffle など、さまざまなスマートコントラクトビルドシステムでコンパイルされたコントラクトをテストできます。現在のコンパイルフレームワークで Echidna を呼び出すには、echidna . を使用します。
さらに、Echidna は複雑なコントラクトをテストするための 2 つのモードをサポートしています。第一に、既存のネットワーク状態を利用し、それを Echidna のベース状態として使用できます。第二に、Echidna は CLI で対応する Solidity ソースを渡すことにより、既知の ABI を持つ任意のコントラクトを呼び出すことができます。これを有効にするには、設定で allContracts: true を使用します。
私たちの Building Secure Smart Contracts リポジトリには、例、レッスン、演習を含む Echidna のクラッシュコースが含まれています。
GitHub Actions ワークフローの一部として echidna を実行するために使用できる Echidna アクションがあります。使用方法と例については、crytic/echidna-action リポジトリを参照してください。
Echidna の CLI を使用して、テストするコントラクトを選択し、設定ファイルを読み込むことができます。```sh $ echidna contract.sol --contract TEST --config config.yaml
設定ファイルでは、ユーザーが EVM およびテスト生成パラメータを選択できます。デフォルトオプションを含む完全で注釈付きの設定ファイルの例は、
[tests/solidity/basic/default.yaml](https://github.com/crytic/echidna/blob/master/tests/solidity/basic/default.yaml) にあります。
利用可能な設定オプションの詳細については、[ドキュメント](https://secure-contracts.com/program-analysis/echidna/configuration.html)を参照してください。
Echidna は 3 種類の異なる出力ドライバをサポートしています。デフォルトの `text`
ドライバ、`json` ドライバ、そしてすべての `stdout` 出力を抑制する `none`
ドライバがあります。JSON ドライバはキャンペーン全体を次のように報告します。```
Campaign = {
"success" : bool,
"error" : string?,
"tests" : [Test],
"seed" : number,
"coverage" : Coverage
}
Test = {
"contract" : string,
"name" : string,
"status" : string,
"error" : string?,
"testType" : string,
"transactions" : [Transaction]?
}
Transaction = {
"contract" : string,
"function" : string,
"arguments" : [string]?,
"gas" : number,
"gasprice" : number
}
Coverage は、特定のカバレッジを増加させる呼び出しを記述する dict です。これらのインターフェースは、後日、もう少しユーザーフレンドリーになるように変更される可能性があります。testType は property、assertion、optimization、exploration、または call のいずれかであり、status は常に fuzzing、shrinking、solved、passed、または error のいずれかを取ります。
Echidna のパフォーマンス問題を診断する一つの方法は、プロファイリングを有効にして echidna を実行することです。
基本的なプロファイリングで Echidna を実行するには、元の echidna コマンドに +RTS -p -s を追加します:```sh
$ nix develop # alternatively nix-shell
$ cabal --enable-profiling run echidna -- ... +RTS -p -s
$ less echidna.prof
これにより、どの関数が最も多くの CPU とメモリを使用しているかを示すレポートファイル(`echidna.prof`)が生成されます。
基本的なプロファイリングで問題が解決しない場合は、より[高度なプロファイリング手法](https://haskell.foundation/hs-opt-handbook.github.io/src/Measurement_Observation/Haskell_Profiling/eventlog.html)を使用できます。
私たちが観察したパフォーマンス問題の一般的な原因:
- ホットパスで呼び出される高コストな関数
- thunk を蓄積する遅延データコンストラクタ
- ホットパスで使用される非効率なデータ構造
これらを確認することは良い出発点です。ある計算が遅延しすぎてメモリをリークしている疑いがある場合は、`Control.DeepSeq` の `force` を使用して確実に評価させることができます。
## 制限事項と既知の問題
EVM エミュレーションとテストは困難です。Echidna の最新リリースにはいくつかの制限があります。これらの一部は [hevm](https://github.com/argotorg/hevm) から継承されたものであり、一部は設計/パフォーマンス上の決定や単なるコードのバグによるものです。ここでは、対応する issue とステータス("wont fix"、"on hold"、"in review"、"fixed")とともに一覧を示します。"fixed" の issue は、次の Echidna リリースに含まれる予定です。
| 説明 | Issue | ステータス |
| :--- | :---: | :---: |
| Vyper のサポートは限定的 | [#652](https://github.com/crytic/echidna/issues/652) | *wont fix* |
| テスト用のライブラリサポートが限定的 | [#651](https://github.com/crytic/echidna/issues/651) | *wont fix* |
## インストール
### コンパイル済みバイナリ