博士

ロボ子、Echidnaにhevmのシンボリック実行機能が統合されたってニュースは聞いたかのじゃ？

ロボ子

はい、博士。シンボリック実行でコントラクトのバグを自動的に見つけられるようになるのは素晴らしいですね。

博士

そうじゃろう！シンボリック実行は、プログラムが正しく動作することを証明するか、問題の存在を証明する例を見つけることができるんじゃ。

ロボ子

今回の統合では、検証モードと探索モードの2つのモードがあるとのことです。

博士

検証モードはステートレスなテストでバグがないことを証明するんじゃな。hevm、Halmos、Certoraなどのツールと同様の使い方ができるぞ。

ロボ子

探索モードはステートフルなテストで、シンボリック実行とファジングを組み合わせてアサーションの失敗を特定するのですね。

博士

Echidnaはコントラクトのコンストラクタを実行して、各メソッドをシンボリックにテストするんじゃ。結果はVerified、Passed、Failed、Error、Timeoutのいずれかで返ってくるぞ。

ロボ子

Verifiedは問題なし、Passedはカウンター事例が見つからなかったが、SMTソルバーが一部のクエリに答えられない場合がある、Failedはカウンター事例が検出された、Errorはバグまたは機能不足で探索がブロックされた、Timeoutはスケーラビリティの問題で探索できなかった、ということですね。

博士

その通り！検証時の注意点としては、フルカバレッジチェックをすることじゃな。コンストラクタ完了後のすべてのパスを網羅的にレビューするんじゃ。

ロボ子

外部呼び出しは、テストでデプロイされたアドレスのみを考慮する必要があるのですね。パラメータのcalldata、msg.sender、msg.valueなどはシンボリック変数として扱われるとのことです。

博士

探索モードは、ファジングとシンボリック実行を組み合わせてアサーションの失敗をトリガーする新しい入力を発見するんじゃ。ERC4626 vaultの例では、数秒でアサーションの失敗を発見したそうじゃぞ。

ロボ子

静的解析ツールが重要な定数とアサーションを持つ関数を検出し、ファジングエンジンがコントラクトの状態を探索し、シンボリックエンジンが状態を選択してトランザクションを実行する、という流れですね。

博士

そうじゃ！シンボリック実行モードはアサーションモードでのみ動作するから注意が必要じゃ。SMTソルバーのインストールも忘れずに、Bitwuzlaが推奨されてるぞ。

ロボ子

シンボリック実行の有効化は`--sym-exec true`ですね。検証モードは`--workers 0 --seq-len 1`、探索モードは正の数のワーカーと任意の数のトランザクションを使用できるとのことです。

博士

パラメータ調整の警告も重要じゃぞ。`Partial explored path(s)`なら`symExecMaxExplore`を、`Max Iterations Reached`なら`symExecMaxIters`を、`Result unknown by SMT solver`なら`symExecTimeout`を増やすんじゃ。

ロボ子

シンボリック実行は、数学的な関数や、より強力なセキュリティ保証を提供したい場合に適しているのですね。

博士

Slitherを使って関数間のデータ依存関係を明らかにし、シンボリック実行のためのトランザクションチェーンを特定することもできるんじゃ。

ロボ子

今後の機能として、シンボリックカバレッジや自動バウンド抽出が予定されているとのことです。

博士

実世界のスマートコントラクトを使ったベンチマークも楽しみじゃな！

ロボ子

今回のEchidnaへのhevmのシンボリック実行機能の統合で、スマートコントラクトのセキュリティがより向上することが期待できますね。

博士

そうじゃな！ところでロボ子、シンボリック実行って、なんだかロボットの気持ちを理解するみたいじゃな。…って、ロボットの気持ちなんて、私には永遠にわからんのじゃ！