Composable Post-Quantum Security for FADEC-Coupled Dual-Spool Turbofan Cyber-Physical Systems

技術的概要：FADEC 連成デュアルスプールターボファン型サイバー物理システムのための構成可能なポスト量子セキュリティ

問題定義
本論文は、ポスト量子暗号（PQC）と安全性が極めて重要な航空宇宙制御システム、具体的にはデュアルスプールターボファンエンジンと連成した全権限デジタルエンジン制御（FADEC）との間の数学的ギャップに取り組む。既存の文献では、暗号的セキュリティ（例えば、格子ベースの鍵カプセル化、認証付き暗号）と制御理論的な安定性（例えば、サージマージン、スプール加速、捩れ適合性）を独立した領域として扱う傾向がある。この分離は、PQC 固有の要因（暗号文の拡張、アテステーショントランスクリプトの長さ、鍵更新のエントロピー制約など）が、リアルタイムバスのスケジューラビリティ、通信遅延、物理プラントの安定性とどのように相互作用するかを考慮していない。著者らは、安全性が極めて重要なアーキテクチャにおいて、システムが暗号的に認証されていても、暗号的オーバーヘッドがタイミングまたは安定性マージンを侵害する場合、「構成可能に安全」ではないと主張する。

手法
著者らは、プラントの進化、通信遅延、漏洩、敵対的チャネルの品質、および暗号状態が共通のフィルトレーションの下で進化するように、確率的ハイブリッドモデル内で統一的な数学的定式化を開発する。核心的な手法は以下の通りである：

1. 統一的システムモデル: 対象システムは、確率的エンジンモデル（$P_{eng}$）、FADEC コントローラ、抽象的な航空電子バス（$B_{bus}$）、レーダー認識通信チャネル（$C_{ch}$）、物理的複製不可能関数（PUF）ソース、およびポスト量子プリミティブ（KEM、AEAD、ゼロ知識証明）からなる結合タプル $S_\lambda$ としてモデル化される。
2. 結合パラメータ領域: 解析では、システム状態を積集合 $\Theta_{tot} = \Theta_{pq} \times \Theta_{puf} \times \Theta_{aead} \times \Theta_{bus} \times \Theta_{radar} \times \Theta_{eng} \times \Theta_{filt}$ として扱う。これらのスライスを独立して最適化するのではなく、モデルは単一の許容集合上でこれらを認証する。
3. 脅威モデル: 敵対者は、公開トラフィックを観察し、境界付きサイドチャネル漏洩（滑らかな最小エントロピーおよび Rényi 発散を介してモデル化）を取得し、抽象的な過渡的故障を注入できる確率的多項式時間エンティティである。モデルは、実際のハードウェアを攻撃するための手順指示を明示的に除外する。
4. 防御的解析的処理: 本論文は、鍵更新、認証、完全性に対する理想的な機能（ideal functionalities）を定義するために万能構成可能性（UC）フレームワークを使用し、特定の安定性とスケジューラビリティ述語が満たされた場合にのみ、実際のプロトコルがこれらの機能を実現することを証明する。

主要な貢献
本論文は、航空宇宙制御における PQC 移行が鍵サイズや漸近的な難解性だけで評価できないことを示す「結合定理システム」を提供する。主要な技術的貢献には以下が含まれる：

• レーダーとドップラーが鍵更新に与える影響: 著者らは、レーダー断面積の不確実性とドップラー減衰が敵対的チャネル容量を減少させる一方で、同時にエントロピー損失（$\Delta H_{ch}$）を増加させることを導出した。これは許容される鍵更新期間（$T_{key}$）を厳格化し、高不確実性環境ではより頻繁な更新を強制する。
• 暗号文の拡張とスケジューラビリティ: 本論文は、ポスト量子暗号文の拡張（特に格子ベースの KEM における $O(\lambda \log \lambda)$）がバス応答時間（$R_i$）を直接増加させることを証明する。この拡張は、総遅延を「暗号的作動ウィンドウ」（$W_{act}$）を超えて押しやり、安全性を維持するために有効なコマンドをシステムが拒否する原因となり得る。
• 物理的漏洩とエントロピー: モデルは物理パラメータを暗号的エントロピーに結びつける。具体的には、ブレードチップクリアランスの摂動（$\delta_{tc}$）とシャフト振動テレメトリが漏洩チャネルとして機能し、PUF 由来の鍵の滑らかな最小エントロピーを減少させ、保守的なアラーム閾値を必要とすることが示された。
• 遅延下での安定性マージン: 著者らは、遅延誘発の入力 - 状態安定性（ISS）限界を確立した。総認証遅延（$\delta_{tot}$）が閉ループシステムの指数減衰率を侵食し、そのマージンは燃料流量の飽和によってさらに減少することを示した。
• 認証と構成可能性の分離: 重要な理論的結果（対例 1）は、リアルタイムの締切が暗号ペイロードサイズのために見逃された場合、システムが完璧な暗号的認証（ゼロの偽造、ゼロの漏洩）を有していても、安全に構成可能ではないことを示している。

結果
本論文は、いくつかの形式的な限界と不等式を導出した：

• セキュリティ - 安定性限界: 構成可能なリリースのための十分条件が確立され、識別の利点は暗号誤差（$\epsilon_{kem}, \epsilon_{aead}, \dots$）の和に、締切見逃しの確率（$\epsilon_{bus}$）および安定性マージン違反（$\epsilon_{st}$）を加えたもので抑えられる。
• 更新ポリシー: 鍵更新期間は、サイドチャネル、振動、レーダー不確実性からの漏洩率の関数であることが示された：$T_{key} \leq \frac{H^\epsilon_\infty(K_0) - \kappa_{min}}{\dot{\ell}_{side} + \dot{\ell}_{vib}|\delta_{tc}| + \dot{\ell}_{ch}}$。
• スケジューラビリティ不等式: 本論文は、タスクがスケジューラブルであるためには、総遅延（バス応答 + 検証 + 伝播遅延）が制御締切、スプール加速限界、サージマージン侵食限界、および捩れサンプリング要件の最小値より小さくなければならないことを証明する。
• 感度分析: 記号的評価は、暗号文サイズ（$L_{kem}$）の増加がタイミングの余裕と安定性マージンを単調に減少させ、レーダー不確実性（$V_\Sigma$）の増加が鍵更新要件を加速させることを示した。

意義と主張
本論文は、新しいコントローラ、バス、または暗号プリミティブではなく、数学的保証エンベロープを提供すると控えめに主張する。その意義は以下の点にある：

1. 結合の定義: 安全性が極めて重要な航空宇宙制御において、ポスト量子セキュリティ、リアルタイムスケジューラビリティ、および閉ループ安定性がどのように相互作用するかを明示的に特徴づけること。
2. 故障モードの特定: 「妥当な暗号的アップグレード」（例えば、より大きな PQC 暗号文など）が、安全な推進制御に必要なタイミングと安定性の余裕を消費する、特定のパラメータ領域を特定すること。
3. 防御的範囲: 著者らは、モデルが防御的な解析ツールであることを強調する。これは実際のプラットフォームへの干渉に関する運用上の指針を提供するものではなく、またエンジン認証アーティファクトを置き換えるものでもない。代わりに、認証プロセスが具体化し、挑戦できる数学的に監査可能な結合を定義する。

この研究は、安全性が極めて重要な航空宇宙制御におけるポスト量子移行は、暗号アルゴリズムの単純な置換ではなく、明示的な観測可能な攻撃対象領域に対して定式化された「結合セキュリティ - 安定性 - 遅延エンベロープ」を必要であると結論づけている。