技術要約：敵対的ネットワークに対する防御可能性分析としてのシールド合成

1. 問題提起

現在のネットワークセキュリティ評価ツールは、根本的なギャップに直面している。静的な検証ツールは、固定された構成における到達可能性や隔離を確認することはできるが、戦略的な敵対者をモデル化することはできない。一方で、サイバーセキュリティのための強化学習（RL）は、シミュレートされた攻撃者に対して適応型エージェントを訓練するが、ある攻撃者に生き残るポリシーが別の攻撃者に対しては失敗する可能性があり、また、あるネットワークトポロジが根本的に防御不可能であることを証明する非公式な手法も存在しない。

既存のシールド強化学習（ShRL）のアプローチは、通常、シールド合成を実行時の強制メカニズムとして扱う。このパラダイムでは、時相論理仕様がオートマトンにコンパイルされ、訓練中またはデプロイ中のエージェントの行動を制限する。しかし、この枠組みには深刻な限界がある：

• スケーラビリティ： 明示的な状態合成は状態変数とともに指数関数的に増大するため、計算可能な範囲が小さな環境に限定される。
• モデルの脆弱性： 保証はモデルに依存する。デプロイされた動態が想定された遷移モデルと異なる場合（モデル不一致）、その「安全な」シールドは、安全性が存在しない場所で安全であると主張してしまう可能性がある。
• 部分観測性： 標準的な定式化は、強い抽象化の仮定なしには、部分観可観測マルコフ決定過程（POMDP）への対応に苦慮する。

著者らは、シールド合成を実行時のフィルターとして扱うことは「誤った製品（wrong product）」であると主張している。代わりに、彼らは同じオートマタ理論のメカニズムを、設計時の分析用インストルメントとして再定義することを提案している。目標は、デプロイされたエージェントのための安全なポリシーを生成することではなく、システムが防御可能であるか、どこに脆弱性があるか、そしてアーキテクチャの変更が防御可能性にどのように影響するかについての構造的な洞察と形式的な証明書を生成することである。

2. 手法

本論文は、この視点をネットワーク防御のための**二重仕様制約付き安全性ゲーム（Dual-Specification Constrained Safety Game）**を通じて具体化している。

2.1 ネットワーク防御ゲーム

システムは、ホストがステータス（クリーン、侵害、検知、隔離、破壊）を持つ有向グラフとして、クリティカルなネットワークセグメントをモデル化する。このゲームには2人のプレイヤーが登場する：

• 防御者（Defender）： 行動には、モニタリング、隔離、復旧、およびホストの修復が含まれる。
• 攻撃者（Attacker）： 行動には、侵害の拡散およびホストの破壊が含まれる。

2.2 二重仕様と非対称な強制

核心となるアーキテクチャ上の革新は、2つの独立した時相論理仕様を決定性有限オートマトン（DFA）にコンパイルし、非対称に強制することである：

1. 防御者仕様 ($\phi_D$): 安全性の目的を定義する（例：クリティカルな資産が同時に侵害されてはならない）。このオートマトン（$A_D$）は、安全性ゲームの初期の非安全集合（$U$）をシード（種）となる。システムが拒絶状態にある状態で $A_D$ に入った場合、そのプレイは安全ではない。
2. 攻撃者仕様 ($\phi_A$): 攻撃者の運用上の制約を課す（例：エンゲージメント中に「破壊」アクションを最大2回までとする予算）。このオートマトン（$A_A$）は、アトラクタ計算中の攻撃者の合法的な行動をフィルタリングする。攻撃者は、$A_A$ を受理状態に留めるような遷移のみを選択できる。

この非対称性は極めて重要である：$\phi_D$ は「何が絶対に起きてはならないか」を定義し、$\phi_A$ は「攻撃者ができないこと」を定義する。

2.3 安全性ゲームの解とアトラクタ計算

フレームワークは、ネットワーク状態、ターンインジケーター、および両方のオートマトンの状態を組み合わせた積ゲームを構築する。そして、不動点アトラクタアルゴリズムを用いて**勝利領域（Winning Region, $W$）**を計算する：

• **アトラクタ（Attractor, $Attr^*$）**は、防御者の戦略に関わらず、攻撃者が $\phi_D$ の違反を強制できる状態の集合である。
• 計算は $\phi_A$ を尊重するように修正される：攻撃者の頂点は、自身が（$\phi_A$ を満たす）合法的な後続状態をアトラクタ内に持っている場合にのみ、アトラクタに入る。
• 防御可能性の判定（Defensibility Verdict）： 主要な出力はバイナリの証明書である：初期状態 $s_0 \in W$ か？ もしそうであれば、そのトポロジは防御可能である。そうでなければ、防御戦略は存在しない。
• シールドの抽出： シールド（安全な行動のルックアップテーブル）は、判定の証拠（witness）として導出されるのであり、実行時のコントローラーとしてではない。

2.4 防御可能性指標とフィンガープリント

バイナリの判定を超えて、著者らは6つの指標からなる**防御可能性フィンガープリント（Defensibility Fingerprint）**を導出している：

• レイヤー1（形式的ゲーム指標）： アトラクタ・シェルの分解（状態から違反までの距離）から導出される。
  • 攻撃可能性 (Attackability, ATK): 勝利領域に対するアトラクタの加重露出度。
  • 沈降比 (Sinking Ratio, SNK): 非違反状態が非安全領域に吸収される割合。
  • シールド摩擦 (Shield Friction, FRC): 安全性を維持するためにシールドによってブロックされる防御者アクションの割合。
  • アトラクタの急峻さ (Attractor Steepness, STP): シェル分布のエントロピー（崖のような形状か、緩やかな傾斜か）。
  • 違反近接性 (Violation Proximity, VPX): 平均ステップ数への逆数。
• レイヤー2（運用指標）：
  • 攻撃者支配比 (Attacker Dominance Ratio, ADR): **シールド型敵対的多エージェント強化学習（Shielded Adversarial MARL）**から導出される。2つのミニマックスQ学習者が勝利領域 $W$ 内でプレイする。この指標は、平衡状態における攻撃者が制御するホストの平均割合を測定する。

3. 主な貢献

1. 二重仕様制約付き安全性ゲーム： 防御者の安全性目的と攻撃者の運用制約が、それぞれ別々のDFAにコンパイルされ、非対称な強制役割（非安全集合のシード化 vs 後続状態のフィルタリング）を持つ形式。
2. 主要出力としての防御可能性判定： 勝利領域を中間ステップから、主要な成果物である「形式的な防御可能性の証明書」へと昇格させたこと。
3. 防御可能性フィンガープリント： 6つの指標（5つの形式的指標と1つの運用指標）を組み合わせ、ネットワーク構成を特徴付ける統一された診断アーティファクト。
4. 診断としてのシールド型敵対的MARL： ポスト収束後のMARL挙動（防御者支配比）を、エージェントの性能指標としてではなく、連続的なトポロジ診断として使用すること。
5. 「What-If」分析： 形式的な安全性と運用上の有効性が異なる側面を捉えることを示し、小さなアーキテクチャの変更が、形式的な安全マージンをほとんど変えずに、運用上の結果を劇的に変化させ得ることを明らかにしたこと。

4. 実験結果

フレームワークは、5ホストのリファレンストポロジと「忘れられた」VPNバイパスエッジを用いて評価された。5つの「What-If」ケースが分析された：

• ベースライン： リファレンストポロジ。
• ケース2（フルコネクト）： 接続性の増加（6エッジから13エッジへ）。
• ケース3（無制限の破壊）： 攻撃者のリソース制約の除去。
• ケース4（緩和された $\phi_D$）： 最小アクティブホスト要件の削減。
• ケース5（VPNの削除）： 特定のVPNバイパスエッジの削除。

主な知見：

• レイヤーの分離： ケース2（フルコネクト）において、形式的な安全性指標（勝利領域のサイズ、攻撃可能性）はベースラインとほぼ同一であった。しかし、運用上の結果（防御者支配比）は、約54%から約23%へと崩壊した。形式的なゲームは「生存は可能」と言っていたが、運用レイヤーは、防御者が圧倒されていることを明らかにした。
• 単一エッジへの感度： ケース5（VPNバイパスの削除）において、形式的な勝利領域のサイズはほとんど変化しなかったが（23,730から23,858状態へ）、防御者支配比は53.9%から80.7%へと跳ね上がった。これは、単一のアーキテクチャ上の欠陥が、形式的に防御可能なシステムを運用上は防御不可能に陥れる可能性があることを示している。
• 仕様の摂動： 制約を緩和すること（ケース3および4）は、両方のレイヤーを整合的に動かした。これにより、仕様がゲームの幾何学を支配し、それが運用行動を決定することが確認された。

5. 重要性と主張

本論文は、シールド合成は安全なエージェントのためのデプロイメカニズムとしてではなく、アーキテクチャに関する問いに答えるためのフレームワークとして最も価値があると主張している。

• 製品の転換： 出力は安全なポリシーではなく、防御可能性の判定と構造的な洞察である。シールドは派生した証拠（witness）であり、デリバラブル（納品物）ではない。
• 設計時のインストルメント： このフレームワークにより、設計者は「この構成は防御可能か？」「どの程度防御可能か？」「どの変更がマージンを改善するか？」という問いに対し、形式的な保証を持って答えることができる。
• 二層構造の必要性： 形式的な安全性ゲームと運用MARLレイヤーは、互いに必要であり、非冗長である。システムは、形式的に防御可能（生存は可能）であっても、運用上は圧倒されている（適応的な攻撃者に対して生存は実質的に不可能）可能性がある。
• 実行可能な診断： 「防御可能性フィンガープリント」は、視覚的かつ定量的な方法で構成を比較することを可能にし、単一のファイアウォールルールのような小さなトポロジの変化が、静的な分析や非公式なシミュレーションが見逃す可能性のある大規模な運用上の影響を与えることを明らかにしている。

著者らは、スケーラビリティ（明示的な状態分析の制限、$|V| \le 7$）や決定論的な遷移の仮定を含む制限事項を認めている。しかし、彼らは、設計決定が行われる小規模でクリティカルなネットワークセグメントの領域において、このフレームワークは既存のツールが提供できない、防御可能性を定量化するための扱いやすく厳密な方法を提供すると主張している。