2akouwu/reverify

Reverify – AI生成バイナリ解析のための決定論的検証

概要 – 純粋なPython（オプションでネイティブ拡張機能を使用）で構築されたツールキットです。言語モデルがバイナリ（またはソースコード）に関する事実を提案し、それを実際のファイルに対してチェックします。検証器は、具体的な証拠（バイト列、逆アセンブル、エミュレーション結果など）とともに、VERIFIED（検証済み）、REFUTED（反論済み）、または INCONCLUSIVE（結論不能）を返します。

重要性 – 大規模言語モデルはコードの読み取りには優れていますが、バイナリの逆エンジニアリングを求められると、構造体のオフセット、関数のプロローグ、API名などを捏造するハルシネーションを頻繁に起こします。Reverifyは、決定論的な解析（PE/ELF/Mach‑O解析、逆アセンブル、パターンマッチング、CPUエミュレーション、Protobuf解析、Fridaフック生成、およびオプションのZ3/angr証明）を実行することで、モデルの主張に根拠を与えます。ツールが実際のバイト列でその主張を実証できた場合にのみ主張が受け入れられるため、AI支援による逆エンジニアリングにおける最大のエラー源が排除されます。

主な機能

• 決定論的コア – PE、ELF、Mach‑O用の純粋なPythonパーサーおよび逆アセンブラ。x86/x64/ARM/ARM64逆アセンブル。AOBスキャン。軽量CPUエミュレータ。protobuf/TLV解析。Fridaフック生成。外部バイナリは不要です。
• オプションのフルスタックバックエンド – pip install "reverify[full]" でCapstone（高性能逆アセンブル）、Unicorn（リアルCPUエミュレーション）、LIEF（バイナリ解析）、Z3（形式証明）が追加されます。pip install "reverify[angr]" でangrによるコールグラフおよび相互参照解析が追加されます。これらがインストールされていない場合、ツールは純粋なPythonコアにフォールバックします。
• 検証ループ – ユーザーは主張（期待されるバイト列、命令、エミュレートされたレジスタ状態、エクスポートされたシンボルなどを記述したJSON）を提供します。Reverifyはバイナリに対してその主張をチェックし、判定結果と、バイナリのSHA‑256、ツールバージョン、証拠を含むレシートを返します。
• 重み付けと情報スコア – 各検証済み主張には、その情報量（エントロピー、一意性）に基づいて重みが割り当てられます。再構築は、反論された主張がなく、かつ合計の重みが設定可能な閾値（--min-information）を超えた場合にのみ根拠があるとみなされます。
• 台帳とロールオーバー – 検証済みの事実と誤りであることが判明した主張は .reverify/ledger/<sha256>.json に永続化されます。AIエージェントのコンテキストウィンドウが溢れそうになった場合、reverify rollover は検証済みの事実のみを含むハンドオフファイルを書き出し、次のセッションで信頼できる状態を失うことなく開始できるようにします。
• エージェントネイティブな MCP サーバー – ReverifyはMCP (Model‑Control‑Protocol) サーバーとして実行できるため、Claude Code、Cursor、Gemini CLI、OpenCode、またはOpenAI互換のエージェントが検証機能を直接呼び出すことができます。通常のCLIも提供されています。
• 等価性テスト – reverify equiv <reference> <candidate> は、両方の実装を同じ入力で実行し、出力が一致するかどうかをチェックします。これは、AIが生成したソースコードのリファクタリングを検証するのに役立ちます。

典型的なワークフロー

# コアのインストール（またはフルバックエンド付き）
pip install reverify          # 純粋なPythonのみ
pip install "reverify[full]"   # capstone, unicorn, lief, z3を追加

# バイナリの迅速な自動解析
reverify auto sample.bin --json

# 特定の主張の検証
reverify verify sample.bin --claim '{
  "kind": "instructions",
  "offset": 4096,
  "mnemonics": ["push","mov","sub"],
  "note": "function prologue"
}'

# LLMドライバーを使用したマルチステップセッションの実行
reverify orchestrate target.exe \
  --goal "map the loader: entry, imports it really uses, exports" \
  --driver claude

ベンチマーク – 71個の実際のWindowsシステムファイルにおいて、言語モデルの教科書的なプロローグの主張は97%の確率で誤っていました。Reverifyはすべての誤った主張を反論し、誤った主張を誤って検証することはありませんでした (0/71)。ベンチマークはLinux、macOS、WindowsのCIで自動的に実行され、結果は BENCHMARK.md で公開されています。

インストールと使用方法 – パッケージはPyPIにあります (pip install reverify)。コアはPython標準ライブラリのみで動作します。オプションのネイティブバックエンドはextras経由でインストールされます。CLIはチェックアウトディレクトリから直接呼び出すことができます (python reverify/cli.py …)。

安全性とライセンス – 許可された逆エンジニアリング（マルウェア解析、CTF、相互運用性研究、または所有するソフトウェア）を目的としています。MITライセンスの下で提供され、CIにはファジングと広範なクロスプラットフォームテストが含まれています。再現可能な監査のために、レシートとSLSA来歴証明が提供されます。

---

Reverify は、AIエージェントがモデルのハルシネーションを信頼することなく、バイナリの逆エンジニアリングやソースコードの等価性チェックを安全に支援できるようにする、具体的で決定論的なガードを提供します。