テクニカル・サマリー：CNnotator: LLMによるメモリ安全性アノテーション合成

問題提起

メモリ安全性に関するエラーは、CおよびC++システムにおけるセキュリティ脆弱性の大部分を占めています。RustやJavaのような現代的なメモリ安全言語とは異異なり、Cは暗黙的なメモリ使用パターンに依存しており、これらを人間が抽出・検証することは困難です。形式手法とAIはそれぞれ補完的な強み（ニューラルネットワークはパターンの「推測」に優れ、形式手法ツールは「検証」に優れる）を持っていますが、レガシーなCコードを検証可能な仕様へと自動的に翻訳するプロセスには依然としてギャップが存在します。具体的には、Cプログラムがどのようにメモリを操作しているか（所有権、割り当て、解放）を判断することは、人間にとっては非常に手間がかかる作業ですが、大規模言語モデル（LLM）によって推論できる可能性があります。課題は、これらの暗黙的なパターンを正確に表現し、検証や安全なトランスパイルを可能にする形式的な仕様を生成することにあります。

手法

著者らは、LLMによる「推測と検証（guess-and-check）」のループを用いて、Cコードに対するメモリ安全性アノテーションを合成するツールであるCNnotatorを提案しています。このシステムは、分離論理（Separation Logic）に基づいた契約言語であるCN（Frama-Cに似ているが、Rustのボローチェッカーのように明示的なメモリ表現を持つ）を対象としています。

CNnotatorのワークフロー

このツールは、以下の反復ループとして動作します。

1. 前処理（Preprocessing）: ツールはCプロジェクトのファイルを単一のコンテキストに統合し、割り当てと解放を正しく扱うために必要なCNライブラリとマクロを注入します。その後、Tree-sitterを使用してコードを抽象構文木（AST）にパースします。
2. 関数選択（Function Selection）: ASTの位置を保持するため、ファイルの末尾から順に関数を反復処理します。
3. LLMによる「推測」（アノテーション生成）:
   • LLMには、CNの構文ガイド（CNチュートリアルからスクレイピングしたもの）、プロジェクト全体のコード、および特定の対象関数の情報がプロンプトとして与えられます。
   • アノテーションを生成する前に、LLMはその関数が本質的に安全でないか（例：use-after-free）を特定するよう求められます。安全でないと判断された場合、その関数に対するプロセスは停止し、バグに関する説明を含むコメントが挿入されます。
   • 関数が安全であると判断された場合、LLMは前提条件（所有権の要件）と事後条件を指定するCNアノテーションを生成します。
4. 形式的な「検証」（テスト）:
   • 生成されたアノテーションがCコードに注入されます。
   • バックエンドであるFulminateが、仕様をランタイムチェックへとコンパイルします。
   • Bennetフレームワークが、前提条件からランダムな入力ジェネレータを導出し、具体的なヒープ状態を作成します。
   • システムは100回のプロパティベーステストを実行し、生成された仕様の下でコードがメモリ安全性違反を起こさずに実行されるかを検証します。
5. 洗練（Refinement）:
   • 成功時: 100回のテストがすべて通過した場合、そのアノテーションは受理されます。
   • 失敗時: テストが失敗した場合、エラーメッセージがLLMにフィードバックされ、アノテーションの修正が行われます。このループは最大6回実行されます。
   • 構文エラー: 初回の生成が構文エラー（これらはしばしば役に立たないコンパイラメッセージを生成します）によって失敗した場合、エラーフィードバックを使用するのではなく、LLMの非決定性を利用して、元のプロンプトを最大2回まで再試行します。

主な貢献

• ツールの開発: LangChain/LangGraphによるエージェント制御、Tree-sitterによるパース、およびFulminate/Bennetフレームワークによる自動テストを統合したPythonベースのツール、CNnotatorの開発。
• ハイブリッド検証アプローチ: LLMが分離論理の仕様（CN）を生成し、形式的なテストバックエンドがそれらを検証するという、LLMの推論を盲信する必要のない実用的なパイプラインの実証。
• ベンチマーク・スイートの構築: 単純な所有権から、グローバル変数やマクロを含む複雑なループに至るまでの31個のアノテーション可能なC関数と、ツールのバグ検出能力をテストするために設計された3個の本質的に安全でない関数からなるテストスイートの構築。

実験結果

著者らは、31個のアノテーション可能な関数に対して、5つのOpenAI LLMバックエンド（o3, o4-mini, o3-mini, GPT-4.1, GPT-4o）を用いてCNnotatorを評価しました。

• パフォーマンス: 推論モデルであるo3が最高のパフォーマンスを示し、96.8%（31個中30個）の関数に対してアノテーションに成功しました。o3は初回の試行で**90.3%**の成功率を達成し、成功したアノテーションあたりの平均試行回数はわずか1.10回でした。
• チャットモデル: チャットモデルであるGPT-4oであっても、初回試行成功率は64.5%、総合成功率は**71.0%**に達し、初回の試行指標において新しいo3-miniを上回りました。
• 失敗モード:
  • ツールは、手動で挿入された3つの本質的に安全でない関数（use-after-free, double-free）をすべて特定し、アノテーションを拒否しました。
  • 手動検査において、誤検知（テストは通過するが内容は不正確なアノテーション）は観察されませんでした。
  • 過度に寛容なアノテーション（必要以上に多くの所有権を要求するもの）が、潜在的な問題として指摘されましたが、これらは依然として有効な仕様を提供するため、許容範囲内であるとみなされました。
• 効率性: システムは、小規模から中規模のプログラムにおいて、AI支援によるアノテーションが、高い成功率を伴う最小限の反復で実用的になりつつあることを示しています。

意義と主張

本論文は、CNnotatorが現実世界のCコードベースにおけるAI支援アノテーションの実現可能性を示していると主張しています。LLMのパターン認識能力と形式的テストツールの厳格なチェックを組み合わせることで、このアプローチは形式検証の「推測と検証」という性質に対処しています。

著者らは、本研究を以下のステップとして位置付けています。

1. コードの近代化: メモリ安全性の契約をまず確立することにより、レガシーなCコードをより安全な言語（Rustなど）へ移行することを容易にする。
2. 検証の自動化: 本来は手動かつエラーが発生しやすい作業である、メモリ安全性仕様の生成を自動化する。
3. 実用性: 現在のモデルがCにおけるメモリ所有権の複雑さを扱うことができ、最小限の人間の介入で高い成功率を達成できることを示す。

本論文は、ベンチマークが50行未満の関数であり、単純な制御フローに限定されていること、また型キャストや高度なポインタ演算といった複雑なプロダクションレベルのコードパターンをまだカバーしていないことを認め、その範囲について謙虚な姿勢を保っています。しかし、LLMの能力が向上するにつれ、この手法はより大規模で複雑なシステムへとスケールできる可能性を示唆しています。