Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware

以下は、論文「Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware」の詳細な技術的要約です。

1. 問題定義

ML-KEM（FIPS 203）や ML-DSA（FIPS 204）といったポスト量子暗号（PQC）規格は、数論的変換（NTT）パイプラインに大きく依存しています。これらのパイプラインは、線形な「バタフライ」ステージと、通常バーレット減算を用いて実装される非線形なモジュロ減算ステージから構成されます。

既存の形式検証フレームワーク（ISW、t-SNI、PINI、DOM）は、$GF(2)$上のブーリアンマスキングに対して強力な保証を提供しますが、特にバーレット減算における**素数体（$\mathbb{Z}_q$）上の算術マスキング**に対する機械検証済みの特性記述は欠けています。

• ギャップ: ハードウェア実装（例えば「Adams Bridge」設計）は、バーレット減算における非線形な条件付き減算が標準的な合成定理が仮定するアフィン構造を破るため、しばしばサイドチャネル脆弱性に悩まされています。
• 問い: 1 次算術マスキングの下において、バーレット減算回路の内部ワイヤの正確な漏洩 bound は何か？従来のツールは普遍的で機械検証済みの回答を提供できなかったため、FIPS 140-3 認証において不確実性が残っていました。

2. 手法

著者らは、Lean 4証明支援機とMathlibライブラリを用いた形式検証アプローチを採用しています。

• 形式化: 彼らは、バーレット内部ワイヤ写像を $\mathbb{Z}_q$（ここで $q$ は法）上で代数的に定義します。写像 $f_x(m)$ は、秘密 $x$ とランダムなマスク $m$ を受け取り、条件付き減算によって決定される 2 分岐構造に基づいて出力を生成します。
• 証明戦略: 特定のインスタンスをシミュレートする代わりに、すべての $q > 0$ およびシフトパラメータ $s$ に対して成立する普遍定理を証明します。
• 主要概念: 彼らは原像の基数を分析します。固定された秘密 $x$ と特定の出力値 $v$ に対して、いくつの異なるマスク $m$ が $v$ を生成し得るか？
• ツールチェーン: 成果物には 12 の証明された結果が含まれており、sorry はゼロ（不完全な証明なし）であり、すべてのステップが Lean によってカーネル検証されています。

3. 主要な貢献

A. 三値定理

この論文は、バーレット内部ワイヤ写像が3 値の原像構造を示すことを証明しています。任意の秘密 $x$ と任意の出力 $v$ に対して、$f_x(m) = v$ となるマスク $m$ の数は、正確に0、1、または 2です。

• メカニズム: 条件付き減算は、2 つのアフィン分岐（$\mathbb{Z}_q$ 内での移動）を作成します。任意の値の原像は、高々 2 つの候補 $\{x - v, x - v + r\}$（ここで $r = 2^s \mod q$）の部分集合です。
• 普遍性: これは、特定の PQC パラメータに依存せず、任意の法 $q$ とシフト $s$ に対して成立します。

B. 1 ビットの障壁

三値性に基づき、著者らは普遍的な漏洩 bound を確立します。

• 最大多重度: 単一の出力を生成するマスクの最大数が 2 であるため、特定の出力値を観測する最大確率は $2/q$ です。
• ミニエントロピー bound: 条件付きミニエントロピー $H_\infty(\text{output} \mid x)$ は、$\log_2(q) - 1$ 以上で抑えられます。
• 解釈: バーレット減算は、1 次プロービング下において、内部ワイヤあたり最大 1 ビットのミニエントロピーを漏らします。これは「保守的」な bound です。なぜなら、多くの出力値は到達不可能（原像数 = 0）であり、実際の漏洩はしばしば厳密に 1 ビット未満であるためです。

C. PF-PINI フレームワーク

著者らは、$\mathbb{Z}_q$ 上の算術ガジェットに対する新しいセキュリティ指標である**素数体 PINI（PF-PINI）**を導入します。

• 定義: 原像の基数が $k$ 以下に抑えられている場合、そのガジェットは PF-PINI($k$) であるといいます。
• 具体例:
  • バタフライステージ: PF-PINI(1) を満たします（完全な全単射、マスクを超えた漏洩なし）。
  • バーレット減算: PF-PINI(2) を満たします（1 ビットの障壁）。
• 合成の観察: 彼らは（まだ形式的に証明されていませんが）、パイプラインステージが新鮮なステージ間マスキングによって分離されている場合、合成されたパイプラインの最大多重度は $\max(k_1, k_2)$ になると観察しています。これは、1 ビットの障壁が NTT パイプライン全体に伝播することを意味します。

4. 結果と分析

• 機械検証済み証明: 成果物には、三値定理、tightness 証明（count=2 が達成可能であることを示す）、および PF-PINI 具体例を含む 12 の検証済み定理が含まれています。
• サポートギャップの発見: 分析により、「到達不可能な」出力値（原像数 = 0）が明らかになりました。これはバグではなくセキュリティ機能であり、攻撃者の有効な情報を削減します。
• Adams Bridge ケーススタディ: この論文は「Adams Bridge」ハードウェア実装を分析します。
  • ステージ内失敗: 先行研究（論文 1 & 2）は、中間マスキングなしのシェア相互作用による脆弱性を示しました。
  • ステージ間失敗: この論文は、Adams Bridge がステージ間の新鮮なマスキングを適用していないことを特定しています。その結果、PF-PINI 合成 bound が適用されず、漏洩が最大値（$\max(k_1, k_2)$）で抑えられるのではなく、乗算（$k_1 \times k_2$）されてしまいます。これが、個々のバーレットゲートに 1 ビットの障壁が存在するにもかかわらず、設計が脆弱である理由を説明します。
• 定量的影響:
  • ML-KEM ($q=3329$) の場合: 漏洩 $\le 1$ ビット（ミニエントロピー $\ge 10.70$ ビット）。
  • ML-DSA ($q=8,380,417$) の場合: 漏洩 $\le 1$ ビット（ミニエントロピー $\ge 21.99$ ビット）。

5. 意義

• 認証への準備: 1 ビットの障壁は、ハードウェア設計者に対する普遍的で機械検証済みの証明書を提供します。これにより、評価者は特定のパラメータセットを再検証することなく、FIPS 140-3 に対するバーレットベースの実装を認証できます。
• 設計ガイダンス: セキュリティのための主要なアーキテクチャ要件が新鮮なステージ間マスキングであることを明確にします。これが実装されていれば、バーレット減算の非線形性は、無視できる 1 ビットの損失を超えて NTT パイプラインのセキュリティを損なうことはありません。
• 方法論的転換: この論文は、サイドチャネル分析を経験的なシミュレーションや SAT ベースのチェックから、カーネル検証された代数的証明へと移行させ、PQC ハードウェア検証の新たな基準を確立します。
• 5 論文プログラムの完結: この研究は、シリーズの先行論文が残したギャップを埋め、ツール構築（論文 1）と攻撃の定量化（論文 2）から、代数的基礎（論文 3）、線形合成（論文 4）、そして最後に非線形特性記述（論文 5）へと移行させます。

6. 限界と今後の課題

• 合成証明: 新鮮なマスキングを伴う合成パイプラインに対して $\max(k_1, k_2)$ が成立するという主張は、現時点では観察事項であり、形式的定理ではありません。
• 高次マスキング: 結果は 1 次マスキング（$t=1$）に限定されています。高次セキュリティには、複数のワイヤにわたる結合原像の分析が必要です。
• エントロピーの形式化: 代数的 bound は証明されていますが、情報理論的なミニエントロピー bound は、まだ Mathlib に完全にアップストリームされていない標準的な定義に依存しています。
• 他の減算法: 結果はバーレット減算に固有です。モンゴメリー減算やスクールブック減算は、個別の分析が必要です。

要約すると、この論文は、バーレット減算は、パイプラインステージ間に新鮮なマスキングが適用される限り、1 次算術マスキング下で本質的に安全であり、ワイヤあたり 1 ビット以下の情報を漏らすことを確立しています。これは、次世代 PQC ハードウェアを保護するための厳密な数学的基盤を提供します。