Solidity stateful fuzzing比較：Foundry・Echidna・Medusaを同じpropertyで検証

Stateful fuzzingは、入力値だけでなく操作の順序と途中stateを探索します。1回のdepositでは保たれる会計が、donationの後の小額depositで崩れる。権限付与と実行は正常でも、次の操作へ権限cacheが残る。こうしたbugは、単一callのunit testやstateless fuzzだけでは届きにくい領域です。

この記事ではFoundry 1.8.0、Echidna 2.3.3、Medusa 1.5.1へ、同じ8 contract、同じproperty_関数、同じaction範囲を渡しました。7種類の意図的bugと安全対照1件を先に定義し、各caseを3回ずつ、合計72 campaign実行しています。

結果は3toolとも7 bugを3/3回再現し、安全対照は3/3回passでした。tool errorとtimeoutも0です。しかし、これは「3toolが同点で安全性も同じ」という意味ではありません。今回のbugは最短2〜5 callで到達できる小さなfixtureです。検出件数では差がつかなかったため、propertyの書き方、探索設定、seed、shrinking、corpus、coverage、出力検証の違いを比較します。

testの価値は本数ではなく、どの失敗を検出でき、無効な実行を失敗として止め、再現に必要な証拠を残せるかで判断します。

同じpropertyへ三つの探索方法を接続する

各target contractは、壊れたときだけfalseになるproperty_関数を持ちます。EchidnaとMedusaはその関数をproperty modeで直接探索します。Foundryでは同じ関数をinvariant test contractから呼び、falseならtestを失敗させます。

Tool	propertyの入口	今回のtarget指定	failure時の主な証拠
Foundry 1.8.0	`invariant_` testから共通`property_`を確認	invariant test contractごとにtargetを分離	call sequence、trace、runs / calls / reverts、fuzz seed
Echidna 2.3.3	`property_`をproperty modeで実行	caseごとのcontractと設定	縮約sequence、coverage corpus、unique instructions、宣言seed
Medusa 1.5.1	`property_`をproperty testingで実行	caseごとのtargetとJSON設定	縮約sequence、call-sequence corpus、branch coverage、trace

Foundry invariant testのhandler・actor・ghost variable設計を先に読むと、propertyの観測値と探索actionを分ける理由が分かります。本比較ではtoolごとのsyntaxを無理に同一化せず、同じ原因と同じpropertyを見ていることを揃えました。

7 bugと安全対照を実行前に固定する

検出結果を見てから正解を作ると、toolが出したsequenceへ都合よくground truthを寄せられます。そこで、原因、期待するfailure、意味のある最短sequenceを先に固定しました。

Case	Category	ground truthの最短sequence	原因
queue cancel	accounting	`queue → cancel`	cancel時にqueued liabilityだけ減らない
epoch double claim	state machine	`advance → claim → claim`	奇数epochでclaim checkpointを更新しない
authorization reuse	access control	`stage → authorize → execute → stage → execute`	実行後もauthorizationが残る
vault zero share	rounding	`donate → deposit`	share price上昇後の小額depositを0 shareで受理する
revoked role cache	access control	`grant → revoke → privilegedAction`	revoke時にauthorization cacheを消さない
callback reentrancy	reentrancy	`armCallback → withdraw`	外部callbackより後にcreditを消費する
delayed double execute	time-dependent state	`schedule → tick → tick → execute → execute`	実行後もscheduleをclearしない
safe queue control	negative control	failureなし	cancel時にcredit、queued amount、liabilityを同期する

安全対照は「何も見つけなかった」だけではありません。3toolがpropertyを正しくpassさせ、exit statusも成功し、compiler errorや未知の出力へ落ちていないことまで確認します。安全対照がcompileされずに終了しても、bug未検出と数えてはいけません。

callback caseの意味はreentrancyを6分類してstate差を追う記事で詳しく整理しています。ここでは外部callの有無ではなく、callback中に同じcreditを再利用でき、最終withdrawalがcreditを超えることをpropertyにしました。

上限を対応づけても仕事量は完全には同じにならない

共通条件はSolidity 0.8.36、Prague target、optimizer 200 runs、sequence長32、worker 1、per-campaign timeout 45秒、shrink上限5,000です。EchidnaとMedusaのcompile前解析にはSlither 0.11.6を有効にしました。

設定	Foundry	Echidna	Medusa
探索上限	625 runs × depth 32	`testLimit: 20000`	`testLimit: 20000`
sequence上限	depth 32	`seqLen: 32`	`callSequenceLength: 32`
並列数	1 thread	1 worker	1 worker
revert policy	`fail_on_revert: false`	property modeの通常探索	property testingの通常探索
shrink上限	5,000	5,000	5,000
source解析	Forge compile	Slither 0.11.6	Slither 0.11.6
campaign間cache	毎回clear	毎回clear	毎回clear

Foundryの625 × 32は20,000 callの上限です。EchidnaとMedusaのtestLimitと内部の生成・coverage処理を同じ仕事量に変換する式ではありません。設定名が似ていても、property failureまでに実行するcall、初期化、compile、coverage feedbackはtoolごとに異なります。

campaignごとにcompile cache、生成config、coverage出力を消し、前のtoolが作ったSolidity reproducerやcorpusを次のtoolへ読ませないよう分離しました。wall-clockにはcompileとSlither解析も含めます。warm cacheを含む最速値だけを選んでいません。

seedは三つで完全一致していない

run labelは19501、19502、19503の3つです。FoundryではFOUNDRY_FUZZ_SEED、Echidnaではconfigのseedへ設定しました。

Medusa 1.5.1について今回確認した公開configとCLI helpでは、外部からRNG seedを固定する項目を確認できませんでした。そのため、Medusaの3回は独立campaignであり、この番号は記録上のrun labelにすぎません。「同じseedを3toolへ渡した」とは扱いません。

seed固定には、failureを完全に再現できる保証もありません。tool version、compiler、target、initial state、action集合、worker数、sequence長、corpusを一緒に保存します。最終的な回帰testには、seedよりshrinking後の具体的なcall sequenceを戻します。

3toolとも7 bugを再現した

次の表は「3回中の再現回数 / 3回で得た最短counterexample call数」です。最短値は、全runが同じ長さまで縮約されたことを意味しません。

Case	Foundry	Echidna	Medusa
queue cancel	3/3・2 calls	3/3・2 calls	3/3・2 calls
epoch double claim	3/3・3 calls	3/3・3 calls	3/3・3 calls
authorization reuse	3/3・5 calls	3/3・5 calls	3/3・5 calls
vault zero share	3/3・2 calls	3/3・2 calls	3/3・2 calls
revoked role cache	3/3・3 calls	3/3・3 calls	3/3・3 calls
callback reentrancy	3/3・2 calls	3/3・2 calls	3/3・2 calls
delayed double execute	3/3・5 calls	3/3・5 calls	3/3・5 calls
safe queue control	3/3 pass	3/3 pass	3/3 pass

全72 campaignについて、tool固有のexact failure / pass markerとexit statusの組み合わせを確認しました。compiler error、spawn error、timeout、認識できない出力は検出にもpassにもせず、tool_errorとして比較全体を止めます。実測はvalid 72/72、tool error 0、timeout 0、安全対照のfalse positive 0でした。

このfixtureでは結果が揃いました。差が出なかったことも重要です。2〜5 callで到達でき、propertyが直接原因を表す小さなcaseでは、三つとも十分に到達できました。一方、actor制約、低確率入力、長い前提sequence、revertの多いhandler、複数contractの複雑なcallbackを加えれば結果は変わり得ます。7/7を製品全体の検出率へ外挿しません。

runtimeは順位ではなく実行設計に使う

Ubuntu 24系、AMD EPYC 9V74、2 logical CPU、約8.3 GB RAMの同じ環境で、各campaignのcompileとsource解析を含むwall-clockを測りました。

Tool	valid campaign	全24 campaignの中央値	安全対照3回の中央値
Foundry	24/24	0.454秒	0.736秒
Echidna	24/24	1.573秒	2.072秒
Medusa	24/24	1.129秒	3.433秒

bug caseはfailureを見つけると早く止まり、安全対照は上限まで探索します。そのため全24 campaignの中央値は、bugの見つけやすさとcase構成に依存します。Foundryの0.454秒を、任意projectでEchidnaより3倍速いという能力値にはしません。

今回の時間から判断できるのは、固定fixtureをこの設定で自動実行できたことまでです。大規模projectではcompile graph、Slither解析、worker数、corpus再利用、timeout、runner CPUが支配します。PRごと、nightly、release前のどこへ置くかは、自分のprojectで安全対照と既知bugを含む時間分布を測って決めます。

coverageの単位を共通percentageへ変換しない

3toolは同じcoverage値を出しません。

Foundryのreportではruns、calls、revertsを確認した
Echidnaではcorpusとunique instructionsを保存した
Medusaではcall-sequence corpusとbranch coverageを保存した

callsが多いこと、unique instructionsが多いこと、branch数が多いことは相互変換できません。分母、instrumentation、initialization、revert処理が違うからです。coverageは同じtool・version・fixture内で「新しいstateへ進めているか」「handler変更で急に落ちていないか」を見る指標にします。

corpusにも役割差があります。Echidnaはcoverageを増やしたsequenceとreproducerを残し、Medusaはcall sequence、test result、coverageを残しました。今回のFoundry設定ではpersistent exploration corpusを比較対象にしていません。三つを同じ「corpus件数」へ丸めず、回帰testへ戻す最小sequenceと、再探索に使うtool固有corpusを分けます。

counterexampleは原因の説明まで縮める

shrinkerの最短call数だけでは、良いcounterexampleとは限りません。確認するのは次の四点です。

ground truthの原因を実際に踏んでいる
不要なcallとactorが除かれている
初期state、引数、sender、時間進行を再現できる
修正後のdeterministic regression testへ移せる

たとえばauthorization reuseの5 callは、最初のexecute後にauthorizationが残り、次のstageを再認証なしで実行できる因果を保ちます。単に最後のproperty failureだけを保存すると、「なぜ二度目だけ成功したか」が消えます。

reentrancyもwithdraw一行だけでは不十分です。callbackをarmed stateへ移し、外部制御移譲中にcreditが未消費であることをtraceへ残します。静的解析3toolの比較でexternal-call noticeとground truthを分けたのと同じく、fuzzerでも「失敗した」と「原因を説明できる」を分けます。

Foundry・Echidna・Medusaの選び方

Foundryは既存Forge testと回帰へ接続しやすい

Foundry invariant testingは、Solidity test、cheatcode、handler、target selector、traceを同じForge projectへ置けます。既存unit testとの共有や、縮約sequenceをSolidity regressionへ戻す流れが短い構成です。

一方、targetを絞らないとtest contractやhelperまで探索対象になり、revertの多いhandlerは有効stateへ進みません。runsを増やす前に、actor、selector、bound、ghost state、revert policyを確認します。

Echidnaはproperty・corpus・coverageを一組で残しやすい

Echidnaの設定はtestLimit、seqLen、seed、worker、shrink、corpusを明示できます。coverageを増やしたcorpusを調べ、届いていないfunctionやrevertへ偏ったsequenceを見直せます。

今回のようなproperty_ contractは簡潔ですが、production contractへtest-only propertyを混ぜるか、専用harnessを置くかを決める必要があります。Slitherによるcontract理解も含むため、compilerとimport解決を固定します。

Medusaはparallel fuzzingとcall-sequence証拠を設計できる

Medusaのtesting設定はproperty testing、call sequence、worker、test limit、shrinkをJSONで管理します。今回も推奨されているSlither解析を有効にしました。

Medusaはworkerを増やせますが、公平な1-worker比較では無効にしています。また、1.5.1では外部seedを固定できないため、厳密なseed replayが要件なら、保存した縮約sequenceとtool versionを再現の中心にします。

CIではexit codeだけで判定しない

property failureはtestとしては非zero exitでも、benchmarkでは「意図したbugを検出した正常な観測」です。反対に、compiler errorの非zero exitは検出ではありません。safe controlのexit 0も、property pass markerがなければ成功扱いにしません。

自動判定は次の順にします。

tool、version、target property、case IDを固定する
timeout、spawn failure、compiler errorを先に除外する
tool固有のexact pass / failure markerを読む
markerとexit statusが一致することを確認する
意図的bugは期待するfailure、安全対照はpassを要求する
raw output、縮約sequence、corpus、設定、hashを保存する

今回の最初の試行では、あるtoolが生成したSolidity reproducerを後続toolのsourceとして拾い、compile errorになったcampaignがありました。旧判定は「残り2toolがbugを見つけた」ことで全体を通してしまいました。campaign directoryの分離と厳密なoutput contractを入れ、1toolでも無効な実行があれば比較全体を失敗させてから再測定しています。

これはtest数を増やす問題ではありません。必要だったのは、無効な結果を成功へ混ぜない一つの再利用可能な判定境界です。公開済み記事の文章や固定件数をsnapshotするtestではなく、compiler errorを検出へ分類しないこと、安全対照を必ず実行すること、tool出力変更を未知として止めることを小さな合成入力で検証します。

導入checklist

まとめ

今回の固定fixtureでは、Foundry、Echidna、Medusaの3toolすべてが7種類のbugを各3回再現し、最短2〜5 callのcounterexampleへ到達しました。安全対照も全runでpassしました。この結果だけなら、検出件数によるtool選択はできません。

差が出るのは運用です。Forge testへ統合するFoundry、seed・coverage corpusを設定しやすいEchidna、JSON設定とcall-sequence corpusを持つMedusaでは、propertyの置き場所、再現方法、coverageの読み方が違います。

一つを「最強」と決める前に、project固有のground truthと安全対照を同じpropertyへ通します。そして、有効な実行だけを比較し、縮約sequenceを回帰testへ戻します。多く回したことではなく、何を探索し、何を見逃し、失敗をどう再現できるか説明できることがstateful fuzzingの完成条件です。

この記事にスポンサー、affiliate、paid tool提供はありません。FoundryはMIT / Apache-2.0のdual license、EchidnaとMedusa、今回併用したSlitherはAGPL-3.0です。導入時は利用versionのlicenseと配布形態を自分のprojectで確認してください。