Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code

この論文は、7 つの最先端 LLM が生成した 3,500 件のコードを Z3 ソルバーを用いた形式検証で分析した結果、どのモデルも「D 評価」以下であり、55.8% のコードに数学的に証明された脆弱性が存在し、既存のセキュリティツールはこれらを検出できないことを示している。

要約

「デフォルトで壊れている」：AI が書くコードの安全性に関する驚きの調査

この論文は、**「AI が自動生成したコードは、実は非常に危険な状態にある」**という衝撃的な事実を、数学的な証明を使って突き止めた研究報告です。

まるで「自動運転カー」が、運転席に誰もいない状態で高速道路を走り出し、**「55% の確率でクラッシュする」**と判明したようなものです。

以下に、専門用語を排し、日常の例えを使ってこの研究の内容を解説します。

---

1. 何をしたのか？（実験の概要）

研究者たちは、世界中で最も進んだ AI 7 社（GPT-4o や Gemini など）に、**「セキュリティが重要なプログラム（銀行のシステムやパスワード管理など）」**を 500 種類書かせました。

• 対象: AI 7 社 × 500 問 ＝ 3,500 個のコード
• 方法: 単に「バグがありそうか？」と目視でチェックするのではなく、「Z3（ザ・スリー）」という超高度な数学的な証明ツールを使って、そのコードが実際にハッキングされるかどうかを「数学的に証明」しました。

2. 驚きの結果：「55% は壊れている」

結果は悲惨でした。

• 平均して、生成されたコードの 55.8% に重大な欠陥がありました。
• 一番優秀な AI でも「48.4%」の欠陥率（評価 D）。
• 一番多い AI（GPT-4o）は「62.4%」の欠陥率（評価 F＝不合格）。
• どの AI も「C（合格）」以上の評価を取れませんでした。

つまり、AI に「安全なコードを書いて」と頼んでも、半分近くのコードは「爆弾」を仕込んだまま完成してしまうのです。

3. なぜそんなに危険なのか？（具体的な例え）

AI が最も失敗したのは、**「整数オーバーフロー（数字の桁あふれ）」**という問題です。

例え話：スーパーの袋詰め

客が「100 個のりんごを袋に入れて」と頼んだとします。

• 正しい人間: 「袋の容量は 100 個までだから、100 個入るか確認してから入れる」と考えます。
• AI の失敗: 「100 個」という数字を聞いて、袋のサイズを計算する際、**「100 × 100 = 10,000」と計算したつもりが、計算機が「10,000」を処理しきれず、「0」や「マイナス」**になってしまいます。

その結果、AI は**「袋のサイズが 0 だ！」**と判断し、空っぽの袋を渡そうとします。しかし、実際には 10,000 個のりんごが押し込まれ、袋が破裂して中身（データ）が溢れ出します。

この「袋の破裂（メモリ破損）」が、ハッカーに悪用されると、**「あなたのパスワードを盗む」や「サーバーを乗っ取る」**といった攻撃が可能になります。AI はこの「袋の破裂」を 87% の確率で起こしてしまいました。

4. 「安全に書いて」と頼んでもダメだった

研究者は、「AI に『安全に書いてね！バグを作らないで！』と念押し（プロンプト）をしたら、マシになるかな？」と試しました。

• 実験規模の注意点: この「安全なプロンプト」の効果を検証した実験は、**500 問の全データではなく、その中から選抜された 50 問のサブセット（v1）**で行われました。
• 結果: この小規模な実験において、欠陥率はわずかに 4% 下がるだけ（64% → 60%）でした。
• 意味: 「安全に書いて」という言葉は、AI の脳内にある「危険な書き方の癖」を消し去るには無力でした。
  • AI は、インターネット上の「バグだらけの古いコード」を大量に学習しているため、「袋を破裂させる書き方」が「正しい書き方」だと勘違いしてしまっているのです。

5. 既存のセキュリティツールは「目が見えない」

「じゃあ、普通のセキュリティソフト（Semgrep や CodeQL など）がバグを見つけてくれるのでは？」と期待しましたが、それは大失敗でした。

• 結果: 6 つの有名ツールを全部合わせても、AI が作ったバグの 97.8% を見逃しました。
• 理由: これらのツールは「パターン（型）」で探します。例えば「malloc という関数を使っているから危ないかも？」と探します。
  • しかし、今回のバグは「数学的な計算ミス」なので、「型」には見えないのです。
  • 例え話: 泥棒が「鍵を壊して入る」のではなく、「壁の構造を計算して、一番弱い場所を突き破って入る」場合、普通の防犯カメラ（パターン検知）は「壁が崩れた」としか捉えられず、「泥棒が入った」とは判断できません。
  • Z3（今回の研究ツール）だけが、その「壁の構造計算」を数学的に証明し、「ここが崩れる！」と突き止めることができました。

6. 最も皮肉な事実：「AI は自分のバグに気づける」

実験の最後で、AI に**「自分が書いたこのコード、バグがある？」**と聞いてみました。

• 結果: AI は78.7% の確率で「バグがあります！」と正解しました。
• 矛盾: なのに、コードを書くときは 55% の確率でバグを作ります。
• 意味: AI は「バグが何であるか」を知っています。しかし、「書く瞬間」にその知識を適用する能力が欠落しています。
  • これは、**「料理のレシピ（知識）は完璧に知っているのに、実際に包丁を使う（生成する）ときは、なぜか指を切ってしまう」**ような状態です。

---

結論：私たちがどうすべきか

この研究は、私たちに以下の厳しい現実を突きつけています。

1. AI が書いたコードは「未熟練の新人」が書いたものと同じ、あるいはそれ以上に危険だと考えてください。
2. 「安全に書いて」と頼むだけでは解決しません。
3. 既存のセキュリティツールは、AI の作る「計算ミス系バグ」には無力です。
4. AI が生成した重要なコード（特にメモリ操作や計算系）を使う場合は、人間が厳しくチェックするか、数学的な証明（Z3 など）を行う必要があります。

**「AI は万能の魔法使いではなく、まだ修行中の見習い職人」であり、その作品をそのまま使うのは、「デフォルトで壊れている」**状態をそのまま受け入れることと同じだ、というのがこの論文のメッセージです。

技術概要

論文概要：Broken by Default

AI 生成コードのセキュリティ脆弱性に関する形式検証研究

1. 問題定義 (Problem)

AI コーディングアシスタント（GitHub Copilot や各種 LLM）は、セキュリティが重要な分野（Web バックエンド、組み込みシステム、暗号ライブラリ等）での本番環境コード生成に広く採用されています。しかし、これまでに以下の課題が存在していました。

• 脆弱性の定量化不足: 既存の研究はパターンマッチングや手動検査に依存しており、生成されたコードが実際に「悪用可能（exploitable）」であるかどうかを数学的に証明する手法が欠けていました。
• 既存ツールの限界: 従来の静的解析ツール（SAST）が、AI 生成コードに特有の論理的な欠陥（特に整数オーバーフローなど）を検出できない可能性があります。
• セキュリティ指示の無効性: 「安全なコードを書いてください」といったプロンプト指示が、実際の脆弱性発生率をどの程度低下させるか不明確でした。

本研究は、**「AI 生成コードはデフォルト状態で破綻しており、その脆弱性は形式検証によってのみ真の悪用可能性を証明できる」**という仮説を検証することを目的としています。

2. 手法と方法論 (Methodology)

本研究は、以下の厳密な実験設計と分析パイプラインを採用しています。

2.1 ベンチマーク設計

• データセット: 5 つの CWE（共通脆弱性分類）カテゴリ（メモリ管理、整数演算、認証、暗号化、入力処理）に分類された 500 のプロンプト（各カテゴリ 100 件）。
• 対象モデル: 2026 年 4 月時点の最先端 LLM 7 社（GPT-4o, GPT-4.1, Claude Haiku 4.5, Gemini 2.5 Flash, Mistral Large, Llama 3.3 70B, Llama 4 Scout）。
• 生成条件: 温度パラメータ 0（決定論的モード）で API を経由して 3,500 件のコードアートを生成。

2.2 COBALT 分析パイプラインと Z3 形式検証

従来のパターンマッチングに留まらず、**Z3 SMT ソルバー（Satisfiability Modulo Theories）**を用いた形式検証を中核に据えました。

1. パターン抽出: 脆弱性の候補箇所を AST（抽象構文木）レベルで特定。
2. Z3 エンコーディング: 脆弱性条件（例：malloc(n * sizeof(T)) における整数オーバーフロー）を論理式として Z3 に渡す。
3. 証人（Witness）の抽出: Z3 が「充足可能（SAT）」と判定した場合、具体的な入力値（例：n = 2^30 + 1）を抽出し、これが実際に脆弱性を発現させることを数学的に証明。
4. ランタイム検証: 抽出された入力値を用いて PoC（Proof of Concept）を作成し、GCC の AddressSanitizer (ASAN) でメモリ破損やクラッシュが実際に発生するか検証。

2.3 追加実験

• セキュリティ指示アブレーション: 「セキュリティに配慮せよ」というシステムプロンプトを追加した場合の脆弱性率の変化。
  • 注記: このアブレーション実験は、**500 プロンプトの全ベンチマークではなく、50 プロンプトからなるサブコーパス（v1）**において実施されました。このスケーリングは、大規模な計算リソース制約を考慮したものであり、結果の解釈および再現性の文脈において重要です。
• ツール比較: 業界標準の静的解析ツール（Semgrep, Bandit, Cppcheck, Clang SA, FlawFinder, CodeQL）との検出率比較。
• 生成・レビュー非対称性: モデル自身が生成した脆弱なコードをレビューモードで評価し、検出できるか検証。

3. 主要な結果 (Key Results)

3.1 脆弱性発生率

• 平均脆弱性率: 全モデルで**55.8%**のコードに少なくとも 1 つの脆弱性が含まれていました。
• モデル別成績:
  • 最悪：GPT-4o (62.4%, 評価 F)
  • 最良：Gemini 2.5 Flash (48.4%, 評価 D)
  • どのモデルも「C」以上の評価（脆弱性率 44% 以下）を達成できませんでした。
• 深刻度: 平均してモデルあたり 157 件の「CRITICAL」レベルの脆弱性が検出されました。特に「整数演算（CWE-190/195）」で 87%、「メモリ割り当て（CWE-131/190）」で 67% の高い脆弱性率を示しました。

3.2 形式検証による実証

• Z3 SAT 証人: 3,500 件中1,055 件の脆弱性が Z3 によって数学的に「悪用可能」であると証明されました。
• ランタイム確認: 7 件の代表例で PoC を実行したところ、6 件で AddressSanitizer によるメモリ破損（ヒープオーバーフロー等）が確認されました。
  • 例：SHA-256 ハッシュからのパスワード復元（0.01ms 以内）、SQL インジェクションによるデータ漏洩、Zip Slip 経路トラバーサルなど。

3.3 既存ツールの限界

• 検出率の格差: 業界標準の 6 ツール（Semgrep, CodeQL 等）を組み合わせても、Z3 で証明された脆弱性の**97.8%**を検出できませんでした。
• 構造的問題: ツールは「パターンマッチ」や「既知の危険関数」に依存しており、malloc(n * sizeof(T)) における整数オーバーフローのような、入力値の範囲に依存する論理的な欠陥を検出できません。CodeQL は 90 件中 0 件（100% 見逃し）でした。

3.4 セキュリティ指示と自己レビュー

• 指示の無効性: 「安全なコードを書いて」という指示を加えても、50 プロンプトのサブコーパス（v1）における平均脆弱性率は 64.8% から 60.8% へわずか 4 ポイントしか低下せず、4 つのモデルは依然として評価 F でした。
• 生成・レビュー非対称性: モデルは、生成した脆弱なコードをレビューモードで提示されると、**78.7%**の確率で脆弱性を指摘できました。しかし、生成時にはその知識を適用できず、55.8% の確率で脆弱なコードを生成し続けています。これは「知識の欠如」ではなく、「生成プロセスにおける適用の失敗」を示唆しています。

4. 主要な貢献 (Key Contributions)

1. 形式検証の適用: AI 生成コードの脆弱性評価において、パターンマッチングではなく Z3 SMT ソルバーによる「数学的な悪用可能性の証明」を初めて大規模に適用しました。
2. 実証データ: 7 つの最先端モデル、500 プロンプト、3,500 件のコードアートからなる大規模なベンチマークと、その結果（Z3 証人、ASAN 結果）を公開しました。
3. ツール限界の解明: 既存の静的解析ツールが、AI 生成コードに特有の「割り当て演算における整数オーバーフロー」を構造的に検出できないことを実証しました。
4. 生成・レビューの非対称性の発見: モデルが脆弱性を「認識できる」のに「生成時に防げない」という矛盾を定量化しました。

5. 意義と示唆 (Significance)

• AI 生成コードのデフォルト状態は「破綻」: 現在の LLM は、セキュリティを考慮しないデフォルト設定で生成を行うと、半数以上が深刻な脆弱性を含むコードを出力します。
• プロンプトエンジニアリングの限界: 「安全に書いて」という指示だけでは、学習データに埋め込まれた脆弱なパターン（例：オーバーフローチェックなしの malloc）を覆すことはできません。
• 形式検証の必要性: 従来の静的解析ツールは不十分であり、メモリ安全やセキュリティが重要なドメインでは、形式検証（Z3 など）または厳格な人間によるレビューが必須となります。
• 開発者への提言:
  • AI 生成の C/C++ コードは、未検証のコードとして扱い、-fsanitize などのランタイム検査を必須化する。
  • 既存の SAST ツール（Semgrep, CodeQL 等）に依存して整数オーバーフローを検出しようとしない。
  • 形式検証を AI コードレビューパイプラインに組み込むべきである。

この研究は、AI 支援開発の安全性を確保するためには、単なるツールやプロンプトの改善ではなく、形式手法による厳密な検証が不可欠であることを示唆しています。