💻 computer science

From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification

この論文は、有限領域での数値的検証に依存していた従来の手法を超越し、Lean 4 による機械検証で任意の法数 $q$ に対してマスクされたポスト量子暗号ハードウェアの安全性を普遍に証明する、環論的基盤を確立したものである。

原著者： Ray Iskander, Khaled Kirah

公開日 2026-04-22

📖 1 分で読めます☕ さくっと読める

原著者： Ray Iskander, Khaled Kirah

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

1. 背景：なぜこんなことをしたの？

未来の量子コンピュータは、今の暗号を簡単に解いてしまう可能性があります。そのため、世界中で「新しい暗号（PQC）」が作られました。
この新しい暗号は、ハードウェア（電子回路）の中で計算されますが、その計算過程で**「電力の消費パターン」**を盗み見られると、秘密の鍵がバレてしまう危険性があります。

これを防ぐために、**「マスク（覆い）」**という技術を使います。

秘密の鍵を「A」と「B」という 2 つのバラバラのかけら（マスク）に分けます。
外から見たら、A も B もただのランダムな数字に見えます。
2 つを足し合わせないと、元の秘密の鍵はわかりません。

【これまでの問題点】
これまでの検証方法は、**「実験室で小さなサンプル（数字 5 まで）だけを使って、全部試してみたら安全だった」**というものでした。

たとえ話： 「お菓子のレシピが安全かどうか確認したいので、砂糖を5 粒だけ使って試作してみたら、美味しくて安全だった！」と言っているようなものです。
問題： 実際の製品では、砂糖が3,329 粒や800 万粒も使われます。「5 粒なら安全でも、800 万粒なら危険かもしれない」という不安が残っていました。これを「有限な数字での検証（Finite Enumeration）」と呼びます。

2. この論文のすごいところ：「魔法の鏡」で全てを証明

この論文の著者たちは、「5 粒」や「800 万粒」を一つ一つ試すのをやめました。
代わりに、**「数学の法則そのもの（環論）」を使って、「どんな数の粒を使っても、絶対に安全である」**ことを証明しました。

新しいアプローチ：
彼らは、**「Lean 4」という、人間ではなく「コンピュータが厳密にチェックする魔法の鏡（証明支援システム）」**を使いました。
- 以前の証明（Z3/CVC5）： 225 種類のケースを、コンピュータに「全部計算させて」正解を出させた。（3300 万回以上の計算が必要だった！）
- 今回の証明（Lean 4）： **「5 行のコード」だけで、「どんな数字でも成り立つ」**という証明を完了させました。
たとえ話：
- 以前： 「1 階から 100 階まで、階段を一つ一つ登って、転ばないか確認した。」
- 今回： 「階段の作り方を設計図（数学の法則）から読み解き、『この設計なら、何階まで登っても転ばない』と証明した。」
これにより、「5 粒」でも「800 万粒」でも、未来に新しい数字が作られても、すべて安全であることが保証されました。

3. 具体的な成果（9 つの定理）

この論文では、メインの証明だけでなく、それを支える 9 つの小さな定理（T1〜T6 など）もすべて証明しました。

メイン定理（T1）： 「秘密の鍵が隠れていれば、外から見たデータは常に一定のランダムさを持つ」ということを、5 行のコードで証明。
オーバーフローの心配なし（T4）： 計算中に数字が溢れてバグる心配がないことを証明。
ランダム性の偏り（T5）： 乱数生成器が少し偏っていても、セキュリティにどう影響するかを計算。
「逆は成り立たない」ことの証明（T6）： 「データがランダムに見えるからといって、必ずしも安全とは限らない」という、逆に危険なケースも証明し、システムが「安全と判断したものは本当に安全だ」という信頼性を高めました。

4. なぜこれが重要なのか？

信頼性の向上：
これまで「Z3 という複雑なソフトウェア」を信じていましたが、今回は「Lean 4 という非常にシンプルで厳密な数学の核」だけを信じています。信頼できる部分（Trusted Base）が劇的に小さくなり、安全性が高まりました。
将来への備え：
将来、NIST（アメリカの規格機関）が新しい暗号規格を決めても、この証明は**「すべての数字に通用する」ため、「またゼロから検証し直す必要がなくなります。」**
効率化：
3300 万回の計算が必要だったものが、5 行のコードで済みました。これは「問題が簡単になった」のではなく、「正しい言語（数学の環論）で話せたから」です。

まとめ

この論文は、**「未来の暗号ハードウェアの安全性を、小さなサンプルで推測するのではなく、数学の法則そのもので『絶対安全』と証明した」**という画期的な成果です。

まるで、**「5 個のリンゴで試作したレシピが、100 万個のリンゴを使っても失敗しないことを、化学反応式（数学）を使って証明した」**ようなものです。これにより、世界中のエンジニアや規制当局は、この新しい暗号を安心して使い始めることができます。

キーワード：

有限な検証（5 粒の砂糖）： 過去の限界。
普遍的な証明（設計図の法則）： 今回の成果。
Lean 4（魔法の鏡）： 厳密にチェックするツール。
5 行のコード： 驚くほどシンプルで強力な証明。

論文要約：有限列挙から普遍証明へ：PQC ハードウェアマスキング検証のための環論的基盤

本論文は、ポスト量子暗号（PQC）のハードウェア実装における側面攻撃（サイドチャネル攻撃）対策としての「マスキング」技術の形式検証に関する研究です。特に、従来の有限領域での SMT ソルバによる検証の限界を克服し、任意の法（modulus） $q$ に対して有効な普遍証明を Lean 4 上で確立した点が核心です。

以下に、問題定義、手法、主要な貢献、結果、および意義について詳細をまとめます。

1. 背景と問題定義

背景: NIST による ML-KEM (FIPS 203) と ML-DSA (FIPS 204) の標準化に伴い、PQC ハードウェアの移行が進んでいます。これらの実装では、数論的変換（NTT）などの演算において、秘密情報を保護するための「算術マスキング」が不可欠です。
既存手法の限界: 著者らの先行研究（QANARY フレームワーク）では、SMT ソルバ（Z3, CVC5）を用いて構造依存性分析を行い、117 万セルの検証を達成しました。しかし、その正統性（Soundness）を保証する定理（Theorem 3.9.1）の機械的検証は、法 $q=5$ の有限領域でのみ行われていました（225 個のブール関数の列挙による検証）。
課題:
1. 普遍性の欠如: $q=5$ での検証結果は、ML-KEM ( $q=3,329$ ) や ML-DSA ( $q=8,380,417$ ) などの実際の生産環境の法に対して構造的に保証されていません。
2. スケーラビリティ: 法が大きくなると、状態空間が指数的に増大し（例： $q=3,329$ で $2^{11,082,241}$ 状態）、列挙による検証は不可能です。
3. 信頼基盤: 従来の手法は SMT ソルバや Python エンコーディングの正しさに依存しており、信頼基盤（Trusted Base）が広範でした。

2. 手法とアプローチ

本論文は、SMT ソルバによる「列挙」から、インタラクティブ定理証明器（ITP）である Lean 4 とその数学ライブラリ Mathlib を用いた「代数的証明」へとパラダイムを転換しました。

環論的抽象化: 算術マスキングの検証を、ビットベクトル論理ではなく、剰余環 $\mathbb{Z}/q\mathbb{Z}$ の可換環（Commutative Ring）の公理に基づいて定式化しました。
再パラメータ化の代数的性質: 秘密 $x$ とマスク $s_1$ による再パラメータ化 $s_0 = x - s_1$ は、計算手順ではなく環の恒等式（ $sub\_add\_cancel$ ）として扱います。
Lean 4 による形式化: Mathlib の ZMod q 型（ $\mathbb{Z}/q\mathbb{Z}$ ）を使用し、任意の $q > 0$ に対して定理を証明しました。証明はすべて「sorry-free」（未検証のスタブなし）であり、Lean カーネルによって検証されます。

3. 主要な貢献

本論文は以下の 3 つの主要な貢献を提示しています。

普遍的正統性証明（Theorem 4.1）:
- 「値の独立性（Value-Independence）が成り立てば、周辺分布は一定である」という定理の普遍証明を確立しました。
- 任意の法 $q > 0$ 、任意の出力型 $\beta$ 、任意の秘密 $x, x'$ に対して有効です。
- 証明はわずか5 行の Lean 4 スクリプトで完結し、 $q=5$ での 225 回の評価を不要にしました。
9 つの支援定理の証明 suite:
- T1, T1': 値の独立性から一定のヒストグラム（周辺分布）への普遍証明。
- T2, T3, T3': ブールおよび算術マスキングにおける再パラメータ化の往復（Round-trip）と全単射性の証明。
- T4: オーバーフローなしの境界条件の証明（ハードウェア実装への橋渡し）。
- T5: 乱数発生器（RNG）のバイアス特性の分析（ML-KEM 固有のケースと普遍的上界）。
- T6: 定理の逆が成り立たないこと（非緊密性）を示す普遍的反例（ $q \ge 2$ すべてに対して）。
方法論的洞察:
- 算術マスキングの検証において、環論（Ring Theory）がビットベクトル SAT よりも自然な抽象化レイヤーであることを示しました。
- 証明の簡潔さ（5 行）は問題が単純だからではなく、適切な代数的形式（可換環の公理）を用いた結果であることを実証しました。

4. 結果

証明の完全性: 1,739 のビルドタスクがすべて成功し、エラーや未検証部分（sorry）は 0 でした。
検証範囲の拡大: $q=5$ のみだった検証範囲が、ML-KEM ( $q=3,329$ )、ML-DSA ( $q=8,380,417$ ) および将来の任意の PQC 標準に対して自動的に拡張されました。
信頼基盤の縮小: 従来の Z3/CVC5/Python に依存していた信頼基盤から、Lean 4 カーネル（および T5 の一部でネイティブコンパイラ）のみへと縮小されました。
保守的な判定の正当性: 先行研究で「INSECURE_CONSERVATIVE」と判定されたワイヤが、実際には値の独立性を満たさないことを T6 で普遍証明し、ツールの保守的な挙動が実装上のバグではなく本質的な限界であることを示しました。

5. 意義と影響

FIPS 140-3 認証への貢献: 個別のパラメータセットごとの再検証が不要になり、認証プロセスの負担を大幅に軽減します。一つの普遍証明がすべての NIST PQC 標準をカバーします。
設計の移植性: 法 $q$ の変更や新しい格子ベースの方式への移行においても、証明が自動的に有効であり続けます。
ツールの信頼性向上: 複雑な SMT ソルバのブラックボックスに依存せず、数学的に厳密に検証された証明を提供することで、高信頼性システムにおける PQC ハードウェアの安全性保証を強化します。
将来の研究への指針: 環論的アプローチが、高次マスキングや混合ブール - 算術変換などの他の性質の証明にも適用可能であることを示唆し、NTT パイプライン全体の構成定理（Composition Theorem）への道を開きました。

結論として、本論文は PQC ハードウェアの側面攻撃耐性検証において、有限列挙から代数的普遍証明への転換を実現し、形式検証の信頼性とスケーラビリティを飛躍的に向上させました。