Solidity静的解析ツール比較：Slither・Aderyn・Mythrilを同じ脆弱contractで検証する

Solidityの静的解析toolは、同じsourceを渡しても同じfindingを返しません。構造とdata flowを広く調べるtool、AST ruleを高速に適用するtool、bytecodeの実行経路をsymbolic executionで探索するtoolでは、見える範囲とcostが違うからです。

この記事ではSlither 0.11.6、Aderyn 0.6.8、Mythril 0.24.8を、Solidity 0.8.36、optimizer 200 runs、Prague targetへ固定した同じ小規模projectで比較しました。13のground truth caseと安全対照1件を先に定義し、tool名やseverity表示を見てから正解を変えない方法を採っています。

結論を先に置くと、今回のcase-level検出はSlitherが9/13、Aderynが10/13、Mythrilが4/13でした。しかし、この数字だけでtoolを順位付けできません。Mythrilは15 contractを個別にsymbolic executionし、transaction数2、各20秒の上限を設けています。SlitherとAderynはproject全体を一度に走査しました。解析方式、timeout、rule setが違うため、coverageとruntimeを必ず設定と一緒に読みます。

比較の正解を先に固定する

検証用projectには次の13ケースを入れました。検出件数を増やすために同じbugを細かく分割せず、reviewで一つの原因として扱う単位を一つのcaseにしています。

1. classic reentrancy
2. cross-function reentrancy
3. ownerを書き換えられるmissing access control
4. tx.originによるauthorization
5. unchecked low-level call
6. user-controlled delegatecall
7. unprotected initializer
8. proxyとimplementationのstorage collision
9. timestampとprevrandaoを使うweak randomness
10. contract balanceのstrict equality
11. builtin/local shadowing、unused state、dead private code
12. library内に隠れたunchecked call
13. PUSH0を含み得るtarget EVM compatibility

安全対照には、stateを先に減らしてから外部callするchecks-effects-interactionsと、return valueを検査するlow-level callを置きました。toolが単に「外部callがある」と棚卸ししただけなら、すぐ誤警告とはしません。一方、安全対照を脆弱性として高・中・低severityで報告した場合はfalse positiveに分類します。

TPはsource spanとdetector familyがground truthの原因に一致したcaseです。一般的な外部call noticeだけでcross-function reentrancyを検出したことにはしません。FNは該当caseにTPが一つもない状態、duplicateは同じcaseを複数findingとして数えた状態です。severityはtool表示と編集側仮説を別々に保存しました。

13ケースの検出結果

Ground truth case	Slither	Aderyn	Mythril
classic reentrancy	検出	検出	検出
cross-function reentrancy	検出	検出	未検出
missing access control	未検出	未検出	未検出
tx.origin authorization	検出	検出	検出
unchecked low-level call	検出	検出	検出
user-controlled delegatecall	検出	検出	検出
unprotected initializer	未検出	検出	未検出
proxy storage collision	未検出	未検出	未検出
weak on-chain randomness	検出	検出	未検出
contract-balance equality	検出	検出	未検出
shadowing・unused・dead code	検出	検出	未検出
library内のunchecked call	検出	検出	未検出
PUSH0 compatibility	未検出	未検出	未検出

全toolが見逃したのは、unrestricted owner update、proxyとimplementationのslot 0 collision、target EVM compatibilityです。owner updateは「状態変更がある」「zero address検査がない」という周辺findingが出ても、authorization不在を指摘していないためTPにはしませんでした。

storage collisionではMythrilがproxyのassembly delegatecallをuser-supplied calleeと報告しました。しかし、今回の原因はcallerがtargetを直接選べることではなく、logicのslot 0 writeがproxyのimplementation slotを上書きするlayout mismatchです。原因が一致しないため、検出ではなくmisclassified findingとして残しています。

PUSH0は対応済みEVMでは正常なopcodeです。古いtargetへdeployするときだけcompatibility riskになります。このcaseを全toolが報告しなかった結果は、compiler・target EVMの照合を別工程に残す必要性を示します。optimizer・via-IR・EVM versionの比較と同じく、source scannerへビルド設定の全責任を移せません。

TP・FP・FN・重複を分けた集計

Tool	TP case	FN case	FP finding	Duplicate finding	Case coverage
Slither 0.11.6	9	4	0	4	69.2%
Aderyn 0.6.8	10	3	2	4	76.9%
Mythril 0.24.8	4	9	1	1	30.8%

Aderynの2 false positivesは、安全対照のchecks-effects-interactionsとreturn value検査済みcallをETH transferred without address checksとしてhigh severityで報告したものです。Mythrilの1件は、安全対照vaultの外部callをlow severityのreentrancyとして報告しました。Slitherも安全対照のlow-level callをinformationalに棚卸ししましたが、脆弱性主張ではないためFPへ数えていません。

raw finding数はSlither 30、Aderyn 37、Mythril 10でした。ここからTP caseへ圧縮すると9、10、4になります。「findingが多いtoolほど多くのbugを見つけた」とは言えません。一般的なlow-level call、event不足、zero address検査、optimization noticeはreviewには役立ちますが、今回の13原因とは別に扱いました。

Slitherはproject全体の構造とdata flowを広く拾った

Slitherは今回、二つのreentrancy、weak randomness、controlled delegatecall、unchecked call、strict equality、shadowing、dead code、library内callを検出しました。project全体のcontractと関係を短時間で見渡す最初のreview queueとして使いやすい結果です。

一方、unprotected initializer、storage collision、missing access control、target EVM compatibilityはTPになりませんでした。detectorを増やすだけでなく、proxy layout checker、compiler manifest、権限testを別に組み合わせます。

抑制にはdetector単位のinline指定、path filter、severity filter、triage databaseがあります。今回の比較設定はfindingがあってもexit 0とし、別のbaseline設定ではlowとinformationalを除外してhighをgateにできます。抑制行には「なぜ安全か」と期限を残し、source変更後に無期限で隠れないようreviewします。

Aderynは高速なrule走査でinitializerまで届いた

Aderynは3tool中で唯一、unprotected initializerをground truthと一致させました。13ケース中10件を検出し、warm runは約0.21秒でした。Foundry projectを認識し、JSON、SARIF、Markdownを直接出せるため、editor feedbackと自動集約を同じ設定へ寄せやすい構成です。

ただし、安全対照2箇所へのhigh severity warningがありました。外部callの宛先検査だけを見て、effects-firstとreturn value検査を十分に反映しないruleでは、人手triageが必要です。detector include/excludeとsource path filterは使えますが、noise ruleを一括除外すると別の真のfindingも消える可能性があります。

Mythrilはsymbolic pathを深掘りする代わりに境界を強く受けた

Mythrilはclassic reentrancy、tx.origin、unchecked return、user-controlled delegatecallの4ケースを検出しました。classic reentrancyでは具体的なtransaction sequenceとstate write after callを返し、source ruleとは違う証拠を付けられます。

今回のcross-function caseでは「user-supplied addressへのcall」というsupporting findingは出ましたが、外部call後のstate writeまたは別entry pointへの再入経路を示さなかったためFNにしました。weak randomnessも値をreturnするだけでcontrol flowを変えない設計では、指定moduleのfindingになりませんでした。

symbolic executionはpath、transaction count、solver、timeoutの影響を強く受けます。今回は15 entry contractを個別に、transaction数2、各20秒上限で実行しました。別のdepthやmoduleなら結果は変わり得ます。4/13はMythril全体の能力値ではなく、この固定条件の観測です。

runtimeは同じ仕事量として読まない

Apple M4 Max、16 logical CPU、128 GiB RAM、Docker 28.5.1の同じrunnerでwall clockを計測しました。container内peak RSSをportableに取得できなかったため、memory rankingは行っていません。

Tool	Cold	Warm	実行単位
Slither	2.277秒	2.295秒	project全体1回
Aderyn	0.501秒	0.209秒	project全体1回
Mythril	165.492秒	165.380秒	15 entry contractの合計

Slitherのwarmがcoldより約18ms長い差はnoise範囲で、優劣には使いません。Aderynは最初のcompiler準備後に短縮しました。Mythrilは各contractのsolver探索が支配的で、cacheだけでは大きく短縮しませんでした。

project全体を一回走査するtoolと、entry contractごとにbounded symbolic executionするtoolの秒数を直接割り算してはいけません。自動gateでは短いstatic passを常時実行し、重いsymbolic passを変更範囲、nightly、release前などへ分ける設計が現実的です。

JSON・SARIF・textとexit codeを選ぶ

Tool	JSON	SARIF	Human-readable	今回のfinding有りexit
Slither	対応	対応	text / Markdown	0（policyで変更可能）
Aderyn	対応	対応	Markdown	0
Mythril	JSON / JSONv2	非対応	text / Markdown	1

SARIFは複数toolのlocationとruleを共通viewerへ集約する形式ですが、severity名、fingerprint、suppression semanticsまで同じにはしません。upload前にtool、version、config hashをresultへ添え、同じfindingの再出現と新規findingを区別します。

Aderynはfindingがあってもexit 0だったため、report countを読むwrapperが必要です。Mythrilはfindingのあるcontractで1、ないcontractで0でした。Slitherは設定したfail_onで変わります。終了codeの違いを無視して三つを同じshell条件へ並べると、見つけたのに成功、見つけて正常終了したのに失敗、といった逆転が起きます。

suppressionとbaselineを安全に運用する

抑制は「toolが間違っているから消す」操作ではなく、ground truthとreview責任を記録する操作です。最低限、次を一組にします。

• tool versionとdetector ID
• source spanまたは安定したfingerprint
• TP、FP、duplicate、accepted risk、out-of-scopeの分類
• 判断理由とreviewer
• 追加testまたは別toolで補う境界
• source・compiler・tool更新後の再確認日

baselineは既存findingを凍結し、新規差分だけをgateできます。ただし、source移動でfingerprintが変わる、detector改良でIDやlocationが変わる、compiler更新でASTが変わる場合があります。件数だけ比較せず、消えたfindingと新しいfindingをground truthへ再対応させます。

Foundry invariant testの設計はsequenceでしか破れない性質を補い、reentrancy 6分類のtrace比較は外部call noticeから実際のstate差へ進む方法を示します。Foundry・Echidna・Medusaのstateful fuzzing比較では、同じproperty、安全対照、2〜5 callの意図的bugを3toolへ接続しています。

導入時の選択checklist

• sourceだけでなくcompiler、target EVM、framework設定を固定した
• tool version、binaryまたはimage digest、config hashを保存した
• project固有のground truthと安全対照を先に作った
• raw finding数とTP case数を分けた
• FP、FN、duplicate、supporting、out-of-scopeを区別した
• tool severityと製品側risk評価を別項目にした
• JSON / SARIF / textのlocationとfingerprintを確認した
• finding有り・無しのexit codeを実測した
• suppressionへ理由、owner、再確認日を付けた
• baseline更新で新規findingをまとめて隠していない
• fast passとbounded symbolic passの実行頻度を分けた
• access control、proxy layout、compiler compatibilityを別testで補った
• scanner passをaudit完了や安全保証として表示していない

今回の公開検証JSONには、13ケース、tool別TP / FP / FN / duplicate、全findingの分類、cold / warm runtime、exit code、runner spec、source hash、raw report hash、suppression方針を保存しました。各toolはfree/open-source版だけを使い、paid plan、sponsor提供、affiliate、cloud scanはありません。

静的解析toolは、review queueを速く作り、見落としやすいpatternを継続的に示すための道具です。完成条件は「三つともgreen」ではなく、どのground truthをどのtoolが検出し、どこを別testと人手reviewが引き受けるか説明できる状態です。