reverify レビュー: LLMの主張を決定論的ツールで反証する検証ゲート

reverify が埋めようとしている穴

LLM はコードを読むのは得意だが、バイナリから構造体やアルゴリズムを復元するのは苦手だと README は述べている。オフセット、サイズ、関数の挙動を自信を持って捏造し、それを事実のように提示する。ソースコード以上にバイナリ解析でこの問題が深刻だと README は位置づけており、AI を実務の RE に使う上での最大の障壁は「モデルが今それをでっち上げたのではないか」という疑念だとする。reverify の答えは、モデルに事実を断言させないことだ。モデルは claim を提案し、決定論的ツールが実物のバイト列と照合して VERIFIED / REFUTED / INCONCLUSIVE を返す。この役割分担が設計の中心にある。対象読者は、マルウェア解析、CTF、相互運用性調査など、権限のある逆解析を行う実務者と、その作業をエージェントに手伝わせたい開発者だ。README は authorized な用途に限定する旨を明記し、SECURITY.md を参照させている。

claim と判定: 何を検証し、何を検証しないか

検証の単位は claim と呼ばれる仮説だ。CLI では reverify verify に対象ファイルと --claim で JSON を渡す。claim の種類は README に列挙があり、bytes_at、u16_at / u32_at / u64_at のような型付き読み出し、pattern_present、string_present、instructions、emulate_result、behavior_equiv、prove_equiv、protobuf_field、import_present、export_present、section_present、そして意味論的な function_at、calls、references、reachable_from_entry がある。instructions の例では offset 4096 の mnemonics が push, mov, sub であることを確認している。emulate_result の例では x86 のコード列 b805000000b90300000001c8c3 を実行し、eax が 8 になることを期待値として照合する。オフセットは既定でファイルオフセットで、claim に "space": "rva" または "va" を書けばセクションテーブル経由で変換され、3 種類のアドレスが返る。ここで注意すべきは、claim に書けるのは検証可能な形に落ちた主張だけだという点だ。「この関数は暗号化ルーチンだ」といった解釈は claim の種類に直接は対応しない。分解すれば pattern_present や calls の組み合わせになるが、分解の設計は使う側の仕事になる。

決定論的コアと任意エンジンの二層構造

reverify のコアは純 Python で、PE/ELF/Mach-O のパース、x86/x64/ARM/ARM64 の逆アセンブリ、AOB パターンスキャン、CPU エミュレーション、Protobuf/TLV の解析、Frida フック生成を担う。README は Ghidra なしでクリーンにインストールできると述べている。pip install "reverify[full]" を選ぶと capstone、unicorn、lief、Z3 が有効になり、pip install "reverify[angr]" で angr が加わり、関数境界、コールグラフ、クロスリファレンスが使える。エンジンが入っていなければ純 Python コアにフォールバックする。どのバックエンドが有効かは reverify backends で確認できる。この二層構造は導入判断で効いてくる。検証の厳密さはバックエンドに依存するため、同じ claim でも環境によって VERIFIED と INCONCLUSIVE の境界が動きうる。README は v0.9.1 で「soundness without the engines」に触れており、エンジンなしでも健全性を保つ方向の修正が入っている。ただし、どの claim 種別がどのバックエンドを必要とするかの対応表は README には示されていない。CI でゲートするなら、実行環境の reverify backends の出力を固定しておかないと、判定が環境差で揺れる可能性を否定できない。

検証ループを CI のゲートにする

reverify verify は REFUTED が 1 件でもあれば非ゼロで終了する。README はこれを、エージェントや CI ジョブが根拠のある再構成をゲートできる仕組みとして説明している。claim は --claims-file claims.json でまとめて渡せる。つまり、人手で確認する代わりに、主張の集合をファイルとして管理し、パイプラインの一部として実行する運用が想定されている。ここで現実的なコストになるのは claim を書く手間だ。モデルに claim を生成させ、それをそのまま検証に回すなら、claim の形式が崩れていないかを確認する工程が要る。JSON のスキーマに合わない claim は検証以前に失敗する。また、判定が INCONCLUSIVE のときにどう扱うかは README からは決まらない。REFUTED は非ゼロ終了という基準があるが、INCONCLUSIVE を失敗とみなすかは運用側の選択になる。ゲートとして使うなら、この 3 値のうちどれを許容するかを先に決めておく必要がある。

rollover が解こうとしている別の問題

reverify の 2 つ目の機能は文脈の劣化への対処だ。長いセッションでは自動要約が情報を落とし、タスクがずれる。reverify rollover は要約ではなく、セッションをファイルに引き継いで新しいセッションを開始する。README はこれを lossless な引き継ぎと表現し、Claude Code、Codex、Gemini CLI、OpenCode で動作するとしている。v0.11.0 のリリースノートもこの 4 つの CLI を挙げている。検証機能とは独立した機能であり、片方だけを使うこともできる。ただし README には rollover が書き出すファイルの形式や、セッションをまたいだときに何が保持され何が保持されないかの詳細は示されていない。lossless という語が指す範囲は、この資料からは確定できない。長いタスクで /clear を避けたいという動機は理解できるが、導入を決める前に、自分のワークフローで引き継ぎ後に何が残るかを実際に確認する必要がある。

バイナリ以外への適用と equiv の位置づけ

reverify はバイナリ専用ではない。reverify equiv <reference> <candidate> --lang python あるいは C を使うと、候補実装と参照実装を共通の入力で実行し、両者が一致するかを確認する。反証の場合は入力と両方の出力が返る。README はこれを、AI によるリファクタや書き換えを信頼ではなくテストする仕組みだと説明している。これは claim の種類にある behavior_equiv や prove_equiv と近い位置づけだが、CLI のサブコマンドとして参照実装を直接渡せる点が違う。ソースコードの書き換えを検証したい場合、バイナリ解析の道具立てを経由せずに済む。ただし、一致する入力の集合がどの程度の範囲をカバーするかは README からは分からない。共有入力での一致は、すべての入力での等価を意味しない。prove_equiv が Z3 を必要とするのに対し、equiv は実行による比較であり、保証の強さが異なる。この違いは README の記述から読み取れる範囲でも明確だ。

ベンチマークの読み方と、そこから言えないこと

README は 71 個の実在する Windows システムファイルを使った結果を報告している。AI の教科書的な答えは 97% の割合で誤っており、reverify はそのすべてを捕捉し、誤った主張を 1 件も受け入れなかった（0 of 71）とされる。同じゲートは Linux と macOS で毎プッシュ CI 実行され、独立した aarch64 の実行でも同じ結果だったと README は述べ、EXAMPLE.md、BENCHMARK.md、python benchmarks/prologue_prior.py を参照先として挙げている。v0.10.0 のリリースノートは、3 プラットフォームでの CI ゲート付きベンチマーク、混同行列、再現可能なコーパス、レシートに言及している。ここで注意したいのは、この数値が測っているのは「誤った主張を受け入れなかったか」であって「解析が正しいか」ではないという点だ。検証ゲートが REFUTED を返す能力と、正しい再構成を生成する能力は別物である。また、この数値は prologue に関する特定のベンチマークに由来し、他の claim 種別や他のバイナリ種別に一般化できるかは資料からは判断できない。

向かない場面と、代わりに何を使うか

reverify が向かないのは、検証ではなく解析そのものを自動化したい場合だ。難読化されたバイナリや VM ベースの保護がかかったコードでは、純 Python コアが既知の命令セットを前提とするため、意味論的な claim は INCONCLUSIVE に落ちやすい。この場合、angr を入れて関数境界やコールグラフを取る方向はあるが、それでも復元の網羅性は保証されない。代替として挙げられるのは Ghidra だ。違いは検証の有無にある。Ghidra はデコンパイラと解析エンジンを提供し、解析結果を人間が読む。reverify は解析結果を主張として受け取り、それを実物と照合する。つまり Ghidra が答えを出すのに対し、reverify は答えの正しさを判定する。両者は排他ではない。README が Ghidra なしでインストールできることを利点として挙げているのは、reverify が Ghidra の代替ではなく、Ghidra を含む解析結果を検証する層として設計されているためだ。もう一つの代替は、単純に人間がレビューすることだ。コストはかかるが、claim の形式に落とせない解釈的な判断を扱える。reverify はその判断を代替しない。

ライセンスと保守の見通し

ライセンスは MIT で、リポジトリの LICENSE ファイルに基づく。MIT は商用利用を含めて寛容な条件だが、具体的な義務や帰属表示の要否は自組織の法務判断であり、ここで法的助言はできない。保守の面では、v0.9.1 から v0.11.0 までが 2026 年 9 月 4 日から 9 月 7 日にかけての短期間に集中している。活発な開発の時期があったことは分かるが、この間隔だけから長期の安定性を判断することはできない。依存関係の重さは選ぶ extras で変わる。純 Python コアは標準ライブラリのみで動くと README は述べており、checkout から python reverify/cli.py auto sample.bin --json のように直接実行できる。reverify[full] や reverify[angr] を選ぶと capstone、unicorn、lief、Z3、angr というネイティブ依存が加わり、アップグレード時の追従コストが増える。CI で使うなら、どの extras を固定するかを決めておくことが、判定の再現性に直結する。

編集部の結論

採用すべきなのは、LLM にバイナリやコードの書き換えを提案させつつ、その主張を人手で確認するコストを下げたいチームだ。特に CI で検証をゲートしたい場合、reverify verify が REFUTED を 1 件でも含めば非ゼロ終了する挙動はそのまま使える。逆に、逆アセンブリの網羅性や難読化されたコードの復元を期待するなら向かない。純 Python コアは既知の命令セットを前提とするため、VM ベースの難読化や独自 ISA では INCONCLUSIVE が積み上がる。導入前に確認すべきは 3 点ある。reverify backends を実行して capstone / unicorn / lief / Z3 / angr のどれが実際に有効か、対象ファイルで reverify auto を走らせて parse-pe や disasm が期待した出力を返すか、そして CI に組み込むなら --claims-file で渡す claim の集合が REFUTED を出さないことだ。ここが通らなければ、検証ゲートとしての価値は主張の正しさではなく主張の形式の正しさに留まる。

公式情報源

1. 2akouwu/reverify on GitHub
2. Issues
3. License: MIT
4. README
5. Releases