論文要約：AI のための暗号学的形式手法と理論的基盤の拡張

論文タイトル: Extending the Formalism and Theoretical Foundations of Cryptography to AI
著者: Federico Villa (ETH Zurich) 他
概要: 本論文は、自律的な大規模言語モデル（LM）ベースのエージェントシステムのセキュリティを評価・保証するために、現代暗号学の形式手法（定義、ゲームベースのモデル、還元証明）を適用する枠組みを提案しています。既存の権限管理やセキュリティ対策が直感的ではあるものの形式的な基盤に欠けている現状を踏まえ、攻撃の分類体系の構築、AIOracle（AI オラクル）のアルゴリズム的定義、そして機密性・完全性・可用性を統合したセキュリティゲームの導入を通じて、エージェントシステムの設計原理を数学的に厳密化しました。

---

1. 背景と問題定義

近年、大規模言語モデル（LM）の進歩により、人間の指示に基づいて自律的に複雑なタスクを実行する「AI エージェント」が実用化されつつあります。これらのエージェントは高い自律性と権限を持ってシステムに統合されるため、そのセキュリティは極めて重要です。

しかし、現在のセキュリティ対策（プロントインジェクションへの対策、権限管理など）は、以下のような課題を抱えています：

• 形式的基盤の欠如: 既存の提案（Progent, Conseca など）は直感的には正当化されるものの、共通の形式的基盤がないため、異なるアプローチ間の比較や、設計の安全性の厳密な証明が困難です。
• 安全性（Safety）とセキュリティ（Security）の分離: 従来の研究では、意図しない危害を防ぐ「安全性」と、悪意ある攻撃者からの防御を目的とする「セキュリティ」が別々に扱われてきました。
• 矛盾する目標: 「有用性（Helpfulness）」と「無害性（Harmlessness）」、あるいは「機密性（Confidentiality）」と「有用性」の間に本質的な緊張関係があり、これを形式的に定式化する必要性がありました。

2. 手法と枠組み

著者らは、現代暗号学の手法（アルゴリズム的定義、敵対モデル、ゲームベースのセキュリティ定義、還元証明）を AI システムに適用するアプローチを採用しました。

2.1 AIOracle（AI オラクル）の抽象化

LM ベースのシステム（チャットボット、分類器、エージェントなど）を統一的にモデル化するために「AIOracle」という概念を導入しました。

• 2 つのフェーズ:
  1. LEARN: コーパス（学習データ）からモデルを生成するフェーズ（学習、微調整、強化学習を含む）。
  2. INFER: ユーザーのクエリ（プロンプト）とコンテキストを用いてモデルから結果を出力するフェーズ。
• 目的関数（Predicate $\phi$）: 結果が「有用で、無害である」かどうかを判定する述語 $\phi$ を定義し、これがシステムの正しさを定義します。

2.2 攻撃分類体系（Attack Taxonomy）

LM に対する既知の攻撃を、以下の多次元フレームワークで体系化しました。

• 攻撃ベクトル: データベース攻撃（学習データの汚染）vs プロンプトベース攻撃（推論時の入力操作）。
• 攻撃フェーズ: 学習フェーズ（Pre-training/Fine-tuning）vs 推論フェーズ（Inference）。
• 敵対者の知識: ホワイトボックス（内部構造・重みの完全把握）vs ブラックボックス（API 経由でのみ相互作用）。
• 攻撃の持続性: 一時的（セッション限定）vs 永続的（モデルパラメータへの恒久的な変更）。
• 攻撃源: ユーザー、第三者、サプライチェーン。

2.3 セキュリティゲームの定義

暗号学における「ゲームベースのセキュリティ定義」を AI に適用し、以下の要素を統合したモデルを構築しました。

• 完全性（Completeness）: 敵対者が存在しない条件下で、システムが仕様通り（$\phi$ が真）に動作すること。
• セキュリティ（Security）: 敵対者が特定の能力（モデルの閲覧、学習データの注入、プロンプトの改ざんなど）を持つ条件下で、システムが $\phi$ を満たし続けること。
• CIA 三要素の統合: 機密性、完全性、可用性を単一のゲームモデル内で統一的に扱います。

2.4 二重構成（Dual Construction）とモジュール分解

「有用性」と「無害性」を独立したサブ問題として扱い、それらを組み合わせるアプローチを提案しました。

• クリエイティブ AIOracle (CAIO): 計算問題（結果の生成）を解決するモデル。
• 退屈な AIOracle (BAIO): 決定問題（結果のフィルタリング・承認）を解決するモデル。
• これらを組み合わせることで、モジュールごとの安全性を保証し、全体の設計の安全性を証明する「還元」が可能になります。

3. 主要な結果と発見

3.1 機密性と有用性の本質的矛盾

トレーニングデータの機密性（学習データがモデルから推論できないこと）と、システムの有用性（すべてのデータから学習して正確な結果を出すこと）の間には、形式的に矛盾が生じることを証明しました。

• 差分プライバシー（DP）の観点から、特定のデータ要素を完全に秘匿しようとすると、モデルはそのデータから学習できず、有用性が損なわれます。
• したがって、機密性の問題は「学習前のデータ選別」や「出力フィルタリング」など、別のモジュールで解決する必要があることを示唆しています。

3.2 既存アプローチの形式的評価

提案した枠組みを用いて、既存の権限管理システム（FIDES, Progent, Conseca, Controlvalve）を分析しました。

• Progent: 動的なポリシー更新を LM に委ねる設計は、プロンプトインジェクション攻撃に対して脆弱であることを指摘。別のモデル（BAIO）がポリシー更新を評価する「二重構成」の必要性を強調しました。
• Conseca: プランナー（LM）がセキュリティポリシーを生成する設計は、プランナー自身が攻撃された場合、ポリシー生成ロジックを回避されるリスク（LM-to-secure-LM のパラドックス）を指摘しました。
• FIDES: データフロー制御は有効ですが、手動ポリシーの完全性に依存する限界があります。

3.3 安全性証明のモジュール化

セキュリティを「完全性（正常動作）」と「耐攻撃性（敵対者への頑健性）」に分解し、さらに「有用性」と「無害性」を独立したモジュールとして扱うことで、複雑なエージェントシステムのセキュリティを構成論理的に証明できることを示しました。

4. 意義と貢献

1. 形式的基盤の確立: AI エージェントのセキュリティ研究に対し、暗号学のような厳密な数学的基盤（定義、ゲーム、証明）を提供しました。これにより、異なる防御手法の定量的比較と、設計の安全性の厳密な証明が可能になります。
2. 統一的なモデルの提案: 機密性、完全性、可用性、有用性、無害性という多岐にわたる要件を、単一の「AIOracle」モデルと「セキュリティゲーム」の中で統合的に扱えるようにしました。
3. 設計指針の提示: 単一の巨大なモデルで全てのセキュリティ要件を満たそうとするのではなく、モジュール（CAIO と BAIO など）に分割し、それぞれを独立して保証する「モジュラーアプローチ」が、実用的かつ理論的に堅牢なシステム設計に必要であることを示しました。
4. 将来の研究への道筋: 攻撃分類体系の提供と、既存システムに対する形式的な批判的評価を通じて、今後の AI セキュリティ研究の方向性を示唆しています。

結論

本論文は、AI エージェントのセキュリティを「経験則」や「実証的ベンチマーク」の域から脱却させ、「証明可能なセキュリティ（Provable Security）」の領域へと引き上げるための重要な一歩です。暗号学の形式手法を AI に適用することで、AI システムの設計者が、有用性と安全性のトレードオフを明確に理解し、構造的な脆弱性を特定・解決するための強力な理論的ツールを提供しています。特に、モジュール化された設計アプローチの提案は、将来の安全な AI システム構築の指針となるでしょう。