技術要約：Assuming You Knew: Agentic AIを用いたフローポリシーのための認識論的意味論の修正

1. 問題提起

情報のフローに関する高レベルなセキュリティ要件、特に選択的な格下げ（declassification）を伴うものは、厳密に形式化することが極めて困難である。認識論的論理（epistemic logic）は、コンフィデンシャリティ（特定の特権レベルを持つオブザーバーが何を知ることを許可されているか）を定義するための有望なフレームワークとして浮上しているが、表現力豊かなフローポリシーのための堅牢で一般的なフレームワークは依然として未確立である。

CN（Naumannら、CSF 2018）と称される先行研究は、リアクティブ・プログラムモデルを統一するフレームワークを提供しようと試みた。CNでは、ポリシーはコード内のassume文を通じて記述され、派生したリリース・ポリシーは入力ストリームのみを用いて表現されていた。しかし、CNにおける定式化には、カンファレンスのプレゼンテーション中に発表された重大な欠陥が含まれていた。元のリリース・ポリシーの定義、および「安全性（safety）がセキュリティ（security）を意味する」というその後の証明は、不完全かつ誤っていた。さらに、既存の機械検証可能な適応例（例：Murrayらによる並行Cプログラム）は、多くの場合、定数時間実行のような強い特性に依存しており、認識論的な推論に必要な複数の実行の整合性を取るための複雑さを回避（簡略化）してしまっている。

核心となる課題は、以下の事項を満たす、修正された機械検証可能な形式化を提供することである：

1. 状態依存の格下げを正しく扱うために、認識論的意味論を修正する。
2. コードのアノテーションから派生するリリース・ポリシーのセマンティクスを明示的に定義する。
3. プログラム指向の特性である**安全性（safety）が、認識論的なセキュリティ（security）**特性を包含することを証明する。

2. メソドロジー

著者は、Rocq証明助手（旧Coq）を用いた形式検証アプローチを採用している。本手法の構成は以下の通りである：

• プログラムモデル: 特定のセキュリティレベルを持つ入力ハンドラを備えた、小規模な命令型リアクティブ言語。プログラムは入力ストリームを消費し、出力を生成する。
• アノテーション: 関係的アサーション（assert）および仮定（assume）を利用して、情報フローの要件を指定する。これらのアノテーションにより、ベースラインの非干渉（non-interference）ポリシーから逸脱する条件付きフローが可能となる。
• 認識論的意味論: セキュリティは、オブザーバーの知識に基づいて定義される。レベル $\ell$ のオブザーバーは、自身の可視な観測（レベル $\ell' \sqsubseteq \ell$ における入力および出力）と矛盾しない、可能な入力履歴の集合を知る。
• リリース・ポリシー ($RP_\ell$): コード内のassume文から導出される、オブザーバーが学習を許可されている入力リストの集合として定義される。このポリシーは、「メジャー（主要な）」プリラン（実際の実行）と「マイナー（補助的な）」プリラン（異なる入力を持つ可能性のある実行）の間の**アライメント（整列）**を通じて解釈される。
• 安全性条件: プログラム指向の特性であり、メジャーな実行をあらゆる可能なマイナーな実行と比較した際の、「失敗（failure）」（アサーション失敗、アライメント失敗）の不在、または特定の「フィアット（fiat）」（仮定のフィアット、発散のフィアット）の存在によって定義される。
• Agentic AIによる支援: 本形式化は、エージェンティックAIコーディングアシスタントであるClaude Codeの支援を受けて開発された。AIは、LaTeXの定義をRocqの仕様へと翻訳し、証明の構築を支援するように誘導されたが、論理的誤りの修正、定義の洗練、あるいは証明戦略の管理において、多大な人間によるキュレーションを必要とした。

3. 主な貢献

A. 修正された認識論的意味論

本論文は、フローポリシーのための認識論的意味論の修正された形式化を提示している。主な技術的修正点は以下の通りである：

• リリース・ポリシーの定義: リリース・ポリシー $RP_\ell(gs)$ の定義を、単なる観測イベントのトレースではなく、プリラン（有限の実行接頭辞）に対する述語へと修正した。これは、メジャーなプリランとマイナーなプリランを特定のアノテーションポイントで整列させる**半適合（semi-conformance）**を通じて定義される。
• 進捗に依存しないセキュリティ: フレームワークは、進捗に依存しない（progress-insensitive）セキュリティ定義を採用している。発散（divergence）を扱うために進捗知識（$k_\ell^\to$）の概念を利用しており、プログラム自体が発散する場合でも、その発散自体が隠蔽された入力に関する情報を漏洩させない限り、セキュリティ保証が保持されるようにしている。
• 適切に指定されたプログラム: 形式化を簡素化し、ベースラインのポリシーを挙動を変えることなくエンコードするために、「ボイラープレート・アノテーション」（ハンドラの開始時の仮定および出力前のアサーション）を導入している。

B. 安全性がセキュリティを包含する

中心的な理論的結果は、定理2である：すべてのレベル $\ell$ において、$\ell$ に対して安全なすべてのプリランは、$\ell$ に対して安全である。

• 安全性は、あらゆる代替入力リストに対するアサーション/アライメントの失敗の不在、および有効なフィアット（仮定または発散）の存在によって定義される。
• 証明は、プログラムが安全であれば、オブザーバーが学習する入力の集合（$k_\ell$）が、リリース・ポリシー（$RP_\ell$）によって許可された入力の集合と、進捗知識との積集合に含まれることを示している。
• この結果は、複雑な全実行のランタイムモニタリングを行うのではなく、プログラムのアノテーションの関係的検証を通じてセキュリティを強制するというアプローチの妥当性を立証している。

C. 機械検証

修正された定義およびメインの定理を含む開発全体が、Rocqで機械検証済みである。これにより、CN論文への修正が根本的に健全であることが確認されるとともに、元の人間によるスケッチでは見落とされていた証明の微妙な細部が明らかになった。

D. Agentic AIの使用経験

本論文は、形式化プロセスにおけるエージェンティックAI（Claude Code）の使用について記録している。著者は、AIが非自明なインフラストラクチャや定型的な証明を生成できる能力を持っていた一方で、以下の事項において人間の監視が必要であったと述べている：

• レマ（例：Lemma 3）の不備のある形式化の修正。
• 「発散のフィアット（divergence fiat）」の定義における論理的ギャップの特定と修正。
• 知識（$k_\ell$）の定義を、等価性ではなく**接頭辞（prefixes）**を使用するように洗練すること（これはAIが見つけた反例によって必要となった変更である）。
• AIが仮定を過剰に強化したり、不要な決定可能性の仮定を導入したりすることを防ぐこと。

4. 結果

• 形式的正当性: 機械検証された証明は、修正された安全性条件が、リアクティブ・プログラムモデルにおける認識論的セキュリティ特性を正しく包含することを裏付けている。
• CNの欠陥の解決: 実行の整列およびリリース・ポリシーの定義に関する、2018年のCNにおける具体的な欠陥は解決された。
• AI支援による形式化の実現可能性: 本研究は、人間がツールを能動的に導き、論理的な誤りを修正し、全体的な証明アーキテクチャを管理するという条件下において、エージェンティックAIが複雑な数学的仕様を機械検証可能な証明へと翻訳する上で効果的に支援できることを示している。

5. 意義と主張

本論文は、控えめながらも重要な貢献を主張している：

• 統一フレームット: 認識論的論理と関係的アノテーションを用いて、表現力豊かなフローポリシーを表現し検証するための、修正された一般的なフレームワークを提供する。
• 実用的な検証: 安全性（ランタイムモニタリングや帰納的証明が可能な特性）がセキュリティを包含することを示すことで、本研究は高レベルのポリシー仕様と、実装可能なプログラム特性との間の溝を埋めている。
• 機械検証の信頼性: 理論的な理想環境における開発であっても、機械検証の必要性を強調している。なぜなら、人間によるレビューが見落とす可能性のある微妙なエラーを露呈させるからである。
• 形式手法におけるAI: 本研究は、エージェンティックAIを用いた実質的な形式的開発の具体的なケーススタディを提供しており、効率性の向上というポテンシャルと、論理的厳密さを確保するための人間による専門知識の決定的な必要性の両方を浮き彫りにしている。

著者は、安全性条件の合成的な証明規則の開発は依然として未解決の問題であり、現在の研究は基礎的な意味論と主要な含意定理に焦点を当てていることを明記している。本論文は、機械検証による形式化の先駆的な役割を認めて、David Basinに捧げられている。