💻 computer science

Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators

この論文は、大規模なポスト量子暗号ハードウェア（117 万ゲート）の側面攻撃耐性を検証するために、構造的依存性分析と SADC を組み合わせた階層的検証手法を提案し、従来のツールでは扱えなかった生産規模の回路においても、数学的証明を伴う効率的な第一階マスク検証を実現したことを示しています。

原著者： Ray Iskander, Khaled Kirah

公開日 2026-04-17

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

CC BY 4.0

原著者： Ray Iskander, Khaled Kirah

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

1. 背景：なぜこんな研究が必要なの？

「量子コンピュータ」という新しい怪物
現在、銀行や国家の秘密を守る暗号技術は、従来のコンピュータでは解読できません。しかし、近い将来登場する「量子コンピュータ」という超強力な機械が現れると、今の暗号は簡単に壊されてしまいます。

そこで、新しい「ポスト量子暗号」という技術が開発されました。これは、量子コンピュータでも解読できないように設計された新しい鍵です。

「側面攻撃」という隠れた罠
しかし、この新しい鍵をハードウェア（チップ）に実装する際、新しい問題が生まれました。それは**「側面攻撃（サイドチャネル攻撃）」です。
ハッカーは、回路が計算している内容そのものを見ようとするのではなく、「回路が消費する電力の揺らぎ」や「発熱」**を盗み見て、秘密の鍵を推測しようとするのです。

「マスク」という対策
これを防ぐために、設計者は**「マスク（覆い）」**という技術を使います。
秘密の鍵を「A」と「B」という 2 つのバラバラの破片（シェア）に分け、それぞれにランダムなノイズを混ぜて処理します。

理想の状態: 回路のどこを見ても、A と B が一緒に現れることはなく、ハッカーは「A も B も分からない」状態になります。
問題: 回路が複雑になるほど、設計ミスで「A と B がうっかり出会う場所」ができてしまい、そこから秘密が漏れてしまうリスクがあります。

2. 従来の問題点：「全部チェック」は不可能

これまで、この「A と B が出会う場所」を見つけるには、2 つの方法しかありませんでした。

人間が手作業でチェックする: 回路図を 1 行ずつ読む。→ 時間がかかりすぎる。
精密なシミュレーションをする: 実際の動作をすべてシミュレーションしてチェックする。→ 回路が巨大すぎると、計算が追いつかない。

今回の対象である「アダムズ・ブリッジ」という巨大な回路（117 万個の部品）は、従来の精密ツールではチェックしきれないほど巨大でした。

3. この論文の解決策：「QANARY（カナリー）」という新しい方法

著者たちは、**「QANARY（カナリー）」という新しいツールを開発しました。名前の由来は、昔の炭鉱でガス漏れを察知するために使われた「カナリア（鳥）」です。
「鳥が倒れたら、人間はすぐに逃げろ」というように、このツールは「危険な場所を素早く見つけて、人間に『ここだけ詳しく見ろ』と警告する」**役割を果たします。

4 つの段階で「危険」を絞り込む

このツールは、4 つの段階（フィルター）を順番に通すことで、効率的にチェックを行います。

第 1 段階：構造チェック（「地図」を見る）
- 比喩: 都市の地図を見て、「A 地区と B 地区を結ぶ道が、どこか 1 本でも交差していないか」を瞬時にチェックします。
- 特徴: 非常に速いですが、「交差している＝必ず危険」とは限りません（実は安全な道かもしれない）。そのため、「危険かもしれない」という**「偽の警報（誤検知）」**が大量に出ます。
- 成果: 117 万個の部品をわずか8.7 秒でチェック完了。
第 2 段階：多サイクルチェック（「時間」を見る）
- 比喩: 「1 秒後には A と B が別々の部屋にいるけど、3 秒後には同じ部屋に入ってくる道はないか？」をチェックします。
- 特徴: これまで見逃されていた、時間差で交差する危険な場所を 12 箇所発見しました。
第 3 段階：数学的な精査（「中身」を見る）
- 比喩: 「道が交差しているけど、実はその交差点に『消しゴム』があって、A と B がぶつかった瞬間に消えてしまっている（安全）」ようなケースを、数学的に証明します。
- 特徴: 「偽の警報」を大量に消去します。
第 4 段階：最終確認（「二重チェック」）
- 比喩: 残った「本当に危険かもしれない場所」を、2 人の異なる専門家（Z3 と CVC5 という 2 つの AI）に同時にチェックさせます。2 人が「危険」と一致すれば、それは間違いなく危険です。

4. 驚異的な成果

このツールを「アダムズ・ブリッジ」という巨大な回路に適用した結果は以下の通りです。

スピード: 117 万個の部品を、数分〜数時間でチェック完了（従来のツールでは数日〜数ヶ月、あるいは不可能）。
精度:
- 当初、構造チェックだけで363 箇所が「危険かもしれない」と警告されました。
- しかし、4 つのフィルターを通した結果、198 箇所は「数学的に安全であることが証明された」として**「OK」**になりました。
- 残りの165 箇所だけが「本当に注意が必要」として、設計者に**「ここだけ手動で確認してください」**というリストとして提出されました。
メリット: 設計者は、363 箇所すべてを調べる必要がなくなり、本当に重要な 165 箇所だけに集中すればよくなりました。これにより、製造前の段階でセキュリティを大幅に強化できます。

5. まとめ：なぜこれが画期的なのか？

この研究は、**「巨大な回路のセキュリティチェックを、人間が手作業でやる時代から、AI が『危険箇所を特定して人間に任せる』時代へ」**と変えるものです。

カナリアの役割: 危険なガスを素早く察知し、人間を助ける。
フィルターの役割: 誤った警報を次々と消去し、本当に重要な問題だけを残す。
結果: 「ポスト量子暗号」を実際のチップに実装する際、**「製造前に、数学的に証明されたセキュリティ」**を確保できるようになりました。

これは、FIPS 140-3（セキュリティの国際基準）の認証取得にも不可欠な技術であり、量子コンピュータ時代に向けた安全なデジタル社会の基盤を作る重要な一歩です。

この論文「Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators」は、ポスト量子暗号（PQC）ハードウェア、特に数論的変換（NTT）に基づく加速器のサイドチャネル攻撃耐性（特にマスク化技術）を、大規模な設計規模で検証するための新しい手法とツール「QANARY」を提案するものです。

以下に、問題定義、手法、主要な貢献、結果、そして意義について詳細な技術的サマリーを記述します。

1. 背景と問題定義

課題: FIPS 140-3 認証を取得するためには、ポスト量子暗号アクセラレータ（ML-KEM, ML-DSA など）がサイドチャネル攻撃（電力解析など）に対して耐性があることを証明する必要があります。マスク化（秘密情報を複数のランダムなシェアに分割する技術）は主要な対策ですが、その安全性を検証するのは困難です。
既存ツールの限界: 従来の厳密なマスク検証ツール（SILVER, Prover, Coco-Alma など）は、ブール論理（XOR マスク）や小規模な回路（数千ゲート程度）では成功していますが、PQC で必要となる算術マスク化（加算・乗算・モジュロ演算）や、大規模なパイプライン構造を持つ回路（百万ゲート規模）にはスケーラビリティが不足しています。
具体的な問題: 単一サイクルの解析では見逃される「マルチサイクル依存性」が存在します。シェアがレジスタを跨いで伝搬し、数サイクル後に再結合することで、単一サイクルでは安全に見えても実際には漏洩する経路が生まれる可能性があります。

2. 提案手法：4 段階の検証階層

論文では、スケーラビリティと精度のバランスを取るための 4 段階の検証階層を提案しています。

D0/D1 構造的依存性解析 (Structural Dependency Analysis):
- 目的: 回路の論理構造に基づき、秘密情報のシェア（ $s_0, s_1$ ）がコンボネーショナル論理内で再結合するかどうかを判定します。
- 手法: 各ワイヤの入力依存性をラベル（ $\bot, S_0, S_1, BOTH$ ）で追跡します。両方のシェアに依存するワイヤを「構造的にインセキュア」としてフラグを立てます。
- 特性: 完全性（False Positive あり）を犠牲にして、大規模回路でのスケーラビリティと「漏洩を見逃さない（False Negative なし）」という健全性（Soundness）を保証します。
- 拡張 (MC-D1): 単一サイクル解析に加え、レジスタ境界を跨ぐ固定点反復（Fixed-point iteration）を行うことで、マルチサイクルにわたるシェアの再結合を検出します。
フレッシュマスク精化 (Fresh Masking Refinement, FM):
- 構造的にインセキュアと判定されたワイヤに対し、その入力に「新しいランダム性（フレッシュマスク）」が含まれており、それがワイヤ出力に対して全単射（バイジェクション）として機能するかどうかを確認します。
- 条件を満たせば、そのワイヤは実際には安全であると再分類されます。
ブール SADC (Boolean Single-Authentication Distance Checking):
- 構造的にフラグが立ったワイヤに対し、SMT ソルバ（Z3）を用いて、秘密情報 $x$ とマスク $s_1$ の関係（ $s_0 = x \oplus s_1$ ）を代数的に再パラメータ化し、ワイヤの値が秘密に依存しないか（値独立性）を検証します。
- ブールマスク化（XOR）に対して有効です。
算術 SADC (Arithmetic SADC):
- 核心となる貢献: PQC で必須の算術マスク化（ $s_0 = (x - s_1) \mod q$ ）に対応した検証です。
- 手法: 秘密 $X$ とマスク $S_1$ を記号変数として扱い、 $S_0 = (X - S_1) \mod q$ という関係式を代入して、ワイヤの値が $X$ に依存しないかを SMT ソルバで検証します。
- 特徴: 従来のブール論理への展開では扱えなかった大きなモジュラス（ $q$ ）やキャリー伝搬を、ビットベクトル論理として正確にモデル化します。

3. 主要な貢献

生産規模での構造的依存性検証:
- 117 万セル規模の「Adams Bridge」ML-DSA/ML-KEM アクセラレータ（30 個のマスク化サブモジュール）全体に対して、D0/D1 解析を 8.7 秒で完了させました。
- MC-D1（マルチサイクル拡張）により、単一サイクルでは安全と判定された 12 モジュールが、実際にはシェアが再結合する「構造的にインセキュア」であることが判明しました。
算術マスク化に対する SADC の実装と検証:
- 5,543 セルの ML-KEM Barrett 削減モジュールにおいて、363 本の構造的フラグワイヤに対し、算術 SADC を適用しました。
- 結果: 198 本（54.5%）を「安全」として機械的に証明し、残りの 165 本を「候補インセキュア（上界）」として特定しました。0 本の未判定（Indeterminate）で完了しました。
- 二重ソルバ検証: すべての 363 本のワイヤについて、Z3 と CVC5 の 2 つの独立した SMT ソルバで検証し、結果の一致（0 不一致）を確認しました。
再現性とインフラ:
- 決定論的な実行環境（固定されたシード、リソース制限）を提供し、結果のビットレベルでの再現性を保証しています。
- 代数的基盤（定理 3.9.1 など）を機械的に検証する証明スイート（Z3/CVC5 用スクリプト）を公開しています。

4. 評価結果

Adams Bridge 全体: 30 モジュール中 27 モジュールを解析完了。
- 単一サイクル（SC-D1）では 15 モジュールがクリーンでしたが、マルチサイクル（MC-D1）では 12 モジュールがインセキュアに転落しました。
- 614,126 本のインセキュアワイヤのうち、真の「収束点（True Convergence Points）」は 8,487 点のみであり、残りは伝搬による冗長なフラグであることが示されました（98.6% の圧縮）。
Barrett 削減モジュール:
- 363 本のフラグワイヤに対し、算術 SADC が 198 本を「安全」と証明。これにより、設計者が手動レビューする必要があるワイヤ数を大幅に削減しました。
- 残りの 165 本は、値独立性の条件を満たさないため「候補インセキュア」として扱われますが、これは厳密な分布独立性（Distributional Independence）の過大評価（Over-approximation）であり、漏洩を見逃すことはありません。
既存ツールとの比較:
- 小規模な回路（DOM AND ゲートなど）では、既存の厳密ツール（Coco-Alma など）と一致するか、False Positive をすべて排除して「安全」と判定しました。
- 大規模回路（NTT バタフライなど）では、Coco-Alma などの厳密ツールがメモリ不足や時間制限で解析不能になる中、本手法は構造的な根因を特定できました。

5. 意義と結論

実用性の向上: 従来の厳密検証ツールが扱えない「生産規模の PQC ハードウェア」に対して、事前シリコン（Pre-Silicon）段階でサイドチャネル耐性の証拠を生成できる最初のツールの一つです。
設計者の負担軽減: 数百〜数千の構造的フラグを、機械的に証明された「安全」なワイヤと、重点レビューが必要な「候補インセキュア」なワイヤに分類することで、設計レビューの工数を劇的に削減します。
補完的なアプローチ: 構造的解析（漏洩経路の特定）と、物理的な電力解析や厳密な代数解析（漏洩の有無の確認）は相互に補完し合います。本手法は、大規模設計における「どこを調べるべきか」を特定するためのスケーラブルなフィルタリングとして機能します。
将来展望: 値独立性（Value-independence）から完全な分布独立性へのギャップを埋めるためのモデルカウンティングの導入、高次マスク化（ $d \ge 2$ ）への拡張、およびグリッチ（Glitch）を考慮した解析への発展が今後の課題として挙げられています。

総じて、この論文はポスト量子暗号ハードウェアのセキュリティ検証において、スケーラビリティと数学的厳密性を両立させるための重要なステップを示すものです。