The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware

技術的サマリー：1 ビットバリアの普遍性

問題定義
数論的変換（NTT）は、NIST 量子耐性暗号（PQC）規格である ML-DSA（FIPS 204）および ML-KEM（FIPS 203）の計算基盤として機能する。これらの規格のハードウェア実装は、差分電力分析（DPA）などのサイドチャネル攻撃への耐性のために、算術的マスキングに依存している。$GF(2^n)$ 上のブールマスキングには、PINI などの構成可能性の枠組みが確立されているが、素数 $q$ に対する $\mathbb{Z}_q$ 上の算術的マスキングは固有の課題を呈する。

QANARY プログラムにおける先行研究（論文 1–6）は、構造的依存関係分析を確立し、特定のコンポーネントに対するセキュリティマージンを定量化した。特に、バレット還元が「1 ビットバリア」（PF-PINI(2)）を満たすことを証明した。しかし、2 つの重要なギャップが残されていた：

1. 任意のパイプライン深度： 以前の構成定理は 2 段階に限定されていた。フレッシュなステージ間マスキングを伴う任意の $k$ 段階パイプラインに対する形式的保証は存在しなかった。
2. モンゴメリー還元： バレット還元が特徴づけられた一方、NTT ハードウェアで用いられる 2 番目の標準的なモジュラ還元であるモンゴメリー還元（ML-DSA および一部の ML-KEM 実装で支配的）には、形式的な PF-PINI 特徴づけが欠けていた。
3. 統合されたエンドツーエンドの境界： バタフライ、バレット、モンゴメリー還元から構成される任意のパイプラインの結果を統合する、単一の機械検証済みの原像基数（cardinality）境界は存在しなかった。

手法
本論文は、Lean 4 証明支援系を用いた形式的検証を採用する。アプローチは厳密に構成的であり、sorry（未証明の仮定）も非標準的な公理もゼロである。手法は以下の要素に依存する：

• PF-PINI の定義： 単一の算術的マスク下での単一ワイヤガジェットからの漏洩を定量化する、素数体プローブ分離非干渉（PF-PINI）パラメータの使用。任意の出力値の原像の基数が $M$ 以下である場合、ガジェットは PF-PINI($M$) である。
• パイプラインのモデル化： 各ステージ $G_i$ が PF-PINI ガジェットであり、フレッシュなランダムマスクによって分離される $k$ 段階パイプラインを定義する。パイプライン出力は再帰的に計算される。
• 組合せ論的分析： フレッシュなステージ間マスキングが中間ステージの漏洩パラメータを「消去」し、最終的な境界を最後のステージのパラメータのみに依存させることを証明する。
• ハードウェア忠実なモデル化： ハードウェアレジスタの幅とラップアラウンド動作を考慮したモンゴメリー還元のモデル化。特に、衝突オフセット $2^{w-s}$ を分析する。

主要な貢献
本論文は、すべて Lean 4 で形式化された 4 つの主要な貢献を行う：

1. $k$ 段階構成定理（定理 3.1）：
   この定理は、以前の 2 段階構成結果を任意の深度 $k \ge 1$ に一般化する。フレッシュなステージ間マスキングを伴うガジェット $G_0, \dots, G_{k-1}$ のパイプラインにおいて、出力の原像の基数は以下によって有界であることを証明する：
   $$| \{ (m, f) : \text{パイプライン出力} = v \} | \le G_{k-1}.\text{maxMult} \cdot q^{2k-2}$$
   決定的に、この境界は最終ステージで決定される；すべての中間ステージのパラメータはフレッシュなマスクによって消去される。

2. モンゴメリー還元は PF-PINI(2) である（定理 4.3）：
   本論文は、モンゴメリー還元がバレット還元と構造を同じくする PF-PINI(2) 性質を満たすことを形式的に証明する。ラップアラウンドが発生するかどうかによって依存する「2 分岐」構造を持つハードウェア忠実なモンゴメリーマップは、最大 2 の原像基数をもたらすことを示す。定理 4.7 はさらに、この境界の緊密性を確立し、標準パラメータ（ML-KEM および ML-DSA）に対して多重度が正確に 2 であることを示す。

3. エンドツーエンドの多重度境界（定理 5.1）：
   $k$ 段階構成定理と、バレット（論文 5）、モンゴメリー（本論文）、バタフライ（論文 4）に対する特定の PF-PINI(2) 結果を組み合わせることで、本論文は統合された境界を確立する。すべてのステージが $\text{maxMult} \le 2$ を満たす任意の $k$ 段階パイプラインにおいて、出力原像の基数は以下によって有界である：
   $$2 \cdot q^{2k-2}$$
   一様マスクを用いた第一順序プローブモデル下では、これはパイプライン深度 $k$ に依存しない、観測ごとの条件付き確率境界 $2/q$ に対応する。

4. 経験的知見の形式的定着（定理 5.4）：
   本論文は、パイプライン内の任意のステージが $\text{maxMult} \ge 3$（例えば、未マスキングされたステージ）を持つ場合、エンドツーエンド境界の仮定が失敗するという、Lean 検証済みの条件を提供する。これは、「Adams Bridge」PQC アクセラレータ（論文 1、2 および外部の作業）の以前の経験的および構造的分析を形式的に定着させ、その設計における特定の未マスキング構成が深度非依存境界の十分条件の外にあることを確認する。

結果

• 1 ビットバリアの普遍性： 本論文は、「1 ビットバリア」（基数 2 の原像）が、NIST PQC ハードウェアで使用される標準的なモジュラ還元（バレットおよびモンゴメリー）の両方に適用されることを確認する。
• 深度非依存性： 形式的証明は、フレッシュなステージ間マスキングが使用され、かつすべてのステージが PF-PINI($\le 2$) を満たす限り、パイプラインにステージを追加しても観測ごとの漏洩境界は劣化しないことを示す。
• 検証ステータス： 完全なアーティファクトは、3 つの定理モジュールにわたる 20 の宣言で構成され、1,753 のジョブでビルドされ、エラーゼロ、sorry ゼロ、ネイティブの決定手続きなしで完了した。

意義と主張
本論文は、マスキングされた NTT ハードウェアの形式的検証プログラムの完成として位置づけられる。その意義は、ハードウェア設計者に対して定量的かつ機械検証済みの構成基盤を提供することにある。

• 認証のために： 導出された基数境界（$2 \cdot q^{2k-2}$）は、SILVER や maskVerif などのゲートレベルツールを補完し、アーキテクチャレベルでの DPA 耐性論証に必要な具体的な証拠を提供する。
• 設計者のために： 深度非依存境界を達成するための処方的な修復経路を提供する；設計者はすべてのステージが PF-PINI($\le 2$) であることを保証し、ステージ間にフレッシュなマスクを挿入しなければならない。
• 主張の謙虚さ： 著者は明示的に、確率および最小エントロピーの解釈（例：$2/q$）は基数境界の形式的な意味論的帰結であり、Lean 内で機械的に形式化されていないと述べている。さらに、Adams Bridge 分析に関しては、本論文は特定の構成が定理 5.1 の十分条件に失敗すると主張するのみであり、ハードウェアが「破損」しているまたは「不安全」であると主張するものではない。代替の枠組みやより強力なモデルが異なる結論をもたらす可能性があることを認めている。この作業は、特定の実装に対する決定的なセキュリティ判決というよりも、構成分析のためのツールとして位置づけられている。