Alignment Contracts for Agentic Security Systems

Isaac David、Marco Guarnieri、Arthur Gervais による論文「Alignment Contracts for Agentic Security Systems」の詳細な技術的サマリーを以下に示す。

1. 問題定義

大規模言語モデル（LLM）を搭載し、計画、実行、セキュリティテスト（例：ペネトレーションテスト）の検証を自律的に行う「Agentic Security Systems（自律型セキュリティシステム）」の台頭は、重大な「非対称な制御問題」を生み出している。

• ジレンマ: これらのエージェントは、承認された範囲内では脆弱性の悪用やシステムへのプロービングなどの強力な攻撃的機能を維持しつつ、その範囲外（承認されていないターゲットへの攻撃、敵対者へのデータ持ち出しなど）ではそれらと同じ機能を厳格に拒否しなければならない。
• 既存のガードレールの失敗: 現在の安全性メカニズム（プロンプトフィルタリング、意図分類、包括的な拒否など）は不十分である。その理由は以下の通りである。
  1. これらは多くの場合、エージェントの「意図」を推測することに依存しており、敵対的なプロンプトインジェクションやモデルのバックドアに対しては信頼性が低い。
  2. 「承認された行動」と「承認されていない行動」の境界を、観測可能な効果に基づいて形式的に、第一級のものとして定義する仕組みが欠けている。
  3. 緩いポリシーによって技術的に「許可」されている行動であれば、エージェントが侵害または操作された場合でも、有害な行動を実行しないことを保証できない。

核心的な課題は、LLM の内部状態や敵対的な操作に関係なく、すべての実現された効果（ネットワークリクエスト、ファイルアクセス、プロセス実行）がオペレーターによって定義された制約内に留まることを保証する責任の境界を強制することである。

2. 手法：アライメントコントラクト

著者らは、観測可能な効果のトレースに対する行動制約を指定し、強制するための形式的フレームワークであるアライメントコントラクトを提案する。

A. 中核概念

• 効果アルファベット（$\Sigma$）: 観測可能な効果のクラス（例：ネットワーク用 NET、ファイルシステム用 FS、プロセス実行用 EXEC）の有限集合。
• イベント: 効果クラス、パラメータ（例：宛先 IP、メソッド）、タイムスタンプ、エージェント ID を表すタプル $e = \langle \sigma, p, t, i \rangle$。
• トレース: イベントの有限列。
• コントラクト（$C$）: 以下を定義するタプル。
  • スコープ（$S$）: どのターゲットが承認されているか。
  • 許可/禁止効果（$E_{allow}, E_{forbid}$）: 許可または禁止される特定の行動クラス。
  • 予算（$B$）: リソース制限（例：最大 10,000 リクエスト）。
  • 開示ポリシー（$D$）: 機密データ（脆弱性、認証情報など）が流れることができる場所。
  • コストとフロー: リソースとデータ抽出の会計関数。

B. 強制メカニズム

このシステムは、効果観測可能性仮説（EOA）の下で動作する参照モニターに依存している。

1. 仲介: すべての外部効果は、実行前に仲介層（例：型付きツールラッパー、HTTP プロキシ、カーネルフック）を通過しなければならない。
2. 受容性チェック: 提案された各イベント $e$ と現在のトレース接頭辞 $\tau$ に対して、モニターは $Adm(e, \tau, C)$ が成り立つかどうかをチェックする。これには以下の検証が含まれる。
   • ターゲットがスコープ内にあること。
   • 効果が許可されており、禁止されていないこと。
   • 予算を超えていないこと。
   • 開示フローが承認されていること。
3. アクション: 受容可能であればイベントを許可し、そうでなければ拒否する。モニターは LLM の内部推論を無視し、観測可能なデータのみに基づいて動作する。

C. 形式的基盤

• 安全性特性: コントラクトの充足は、有限トレース上の安全性特性として定義される。コントラクトが違反された場合、その違反を証する有限の「悪い接頭辞」が存在する。
• 機械化: 中核となる定理は、形式的証明支援系であるLean 4を用いて検証されており、フレームワークの論理的妥当性が保証されている。

3. 主要な貢献

1. 形式的モデル: トレースベースのセマンティクスを持つ有限効果アルファベット上のタプルとしてのアライメントコントラクトの定義。論文は、違反が有限時間で検出可能であることを保証する有限の悪い接頭辞の証人特性を証明している。
2. 強制の妥当性: EOA の下で、著者らは、いかなるエージェント（敵対的、プロンプトインジェクションされた、バックドアされたものを含む）も、その効果が完全に仲介される場合、コントラクトを満たすトレースのみを生成することを証明している。これにより、信頼の拠点は信頼できない LLM から、小さく監査可能な強制バリアへと移行する。
3. コントラクト代数:
   • 洗練（$C' \sqsubseteq C$）: 妥当性を維持しつつ、より厳格なコントラクト（より狭いスコープ、より厳しい予算）を作成するメカニズム。
   • 一方向合成: 契約を組み合わせるための規則（例：組織ポリシーとエンゲージメントスコープの統合）であり、証明された妥当性の保証を伴う。
   • 決定可能性: 論文は、受容性チェックが決定可能であり、計算効率的（キャッシュ付きでオンライン $O(|Res|)$）であることを確立している。
4. 適応スキーマ: 「コントラクトを保持する」適応ルールを定義することにより、サブエージェントの生成やツールの交換などの動的なシステム変化に対応するフレームワーク。
5. 不可能性の結果: 論文はこのアプローチの限界を形式的に区画している。
   • 決定不可能性: ツールがいつか禁止された効果を試みるかどうかの静的な事前承認分析は、チューリング完全な言語に対して決定不可能である。
   • 回避の限界: ツールが仲介層を回避する場合（例：カーネルモジュールやサイドチャネル経由）、妥当性の保証は崩壊する。
   • 観測可能性の境界: 隠蔽チャネル（ペイロードのステガノグラフィ、タイミングチャネル）やモデル化されていない効果は、定理の対象外である。

4. 結果と評価

• 理論的保証: Lean 4 によるアーティファクトは、参照モニターが正しく実装され、EOA が成り立つ場合、システムが妥当であることを検証している。LLM の行動は保証には無関係であり、重要なのは実現された効果のみである。
• ケーススタディ（Web ペネトレーションテスト）: このフレームワークは、Web ペネトレーションテストのシナリオで具体化された。以下のような制約が正常にモデル化された。
  • 「*.example.com に対して HTTP GET/HEAD のみ。」
  • 「ファイルシステム操作は禁止。」
  • 「最大 10,000 リクエスト。」
  • 「レポートはダッシュボードへのみ送信。」
  • モニターは、エージェントがそうするように「プロンプトインジェクション」された場合でも、evil.com へのデータ持ち出しや承認されていないドメインへのアクセスを試みる行為を正しくブロックした。
• 複雑性: 中核となる受容性チェックは、実用的な展開（小さく固定されたリソースセットを仮定）において、イベントあたり定数時間であることが示されており、ランタイム強制に実用可能である。

5. 意義

この論文は、AI エージェントのセキュリティ確保におけるパラダイムシフトを表している。

• 意図から効果へ: 困難で脆弱な LLM の内部意図を「アライメント」しようとする試みから、検証可能な観測可能な効果に対する制約の強制へと移行する。
• 形式的信頼: 機械化された証明を用いることで、仲介層が安全であれば、エージェントがコントラクトを違反できないという数学的に厳密な保証を提供する。これにより、信頼計算基盤（TCB）は LLM を除外し、モニターと仲介境界に縮小される。
• 実用性: このフレームワークは、現実世界の攻撃的セキュリティワークフロー向けに設計されており、副次的な被害やデータ漏洩の恐れなく、強力な自律型エージェントを安全に展開する方法を提供する。
• 明確な境界: システムが保証できないこと（例：ペイロード内容の検査、タイミングチャネル）を明示的に述べることで、技術への過剰な依存を防ぎ、将来のエンジニアリング努力をこれらの特定のギャップを埋める方向へ導く。

要約すると、アライメントコントラクトは、自律型セキュリティシステムが厳密に承認された境界内で動作することを保証する、最初の形式的で決定可能かつ機械的に検証されたフレームワークを提供する。これにより、LLM 推論の「ブラックボックス」を、強制可能な効果制約の「ホワイトボックス」へと変換する。