論文の概要: Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware
- arxiv url: http://arxiv.org/abs/2604.20793v2
- Date: Sat, 25 Apr 2026 05:32:07 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-28 13:03:00.482628
- Title: Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware
- Title（参考訳）: 新鮮なマスキングによるNTTパイプラインの構成:PQCハードウェアにおける算術的マスキングのための機械式証明
- Authors: Ray Iskander, Khaled Kirah,
- Abstract要約: 量子後暗号(PQC)アクセラレーターは、$mathbbZ_q$を超えるパイプライン化された数理論変換ステージに依存している。
我々の以前の研究は大規模な構造依存解析を確立し、部分NTTマスキングのセキュリティマージンを定量化した。
マシンでチェックした3つの結果は、Lean 4でMathlibとともに紹介します。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Post-quantum cryptographic (PQC) accelerators for ML-KEM (FIPS 203) and ML-DSA (FIPS 204) rely on pipelined Number Theoretic Transform (NTT) stages over $\mathbb{Z}_q$. Our prior work established structural dependency analysis at scale [1] and quantified the security margin of partial NTT masking [2]. Whether per-stage arithmetic masking guarantees pipeline-level security had no prior machine-checked answer for the r-bearing case: composition frameworks (ISW, t-SNI, PINI, DOM) were formalized exclusively for Boolean masking over $\mathrm{GF}(2)$; no proof assistant artifact addresses the NTT butterfly over $\mathbb{Z}_q$. We present three machine-checked results in Lean 4 with Mathlib, all zero sorry. First, we close a stated limitation of prior work: value-independence implies constant marginal distribution under fresh randomness (via an algebraic MutualInfoZero proxy). Second, butterfly per-context uniformity: for any Cooley-Tukey butterfly with fresh output mask over $\mathbb{Z}/q\mathbb{Z}$ ($q > 0$), each output wire has exactly one mask value producing each output, a uniform marginal independent of secrets, universal over all moduli, twiddle factors, and inputs. Third, a k-stage NTT pipeline with fresh per-stage masking satisfies per-context uniformity at every stage under the ISW first-order probing model. We document a named warning: pointwise value-independence is false for butterfly outputs. The Adams Bridge accelerator (CHIPS Alliance Caliptra) fails the fresh masking hypothesis, masking active only in INTT round 0, architecturally explaining its structural insecurity. Artifact: nine theorems, 1,738 build jobs, zero sorry. Composition for nonlinear gadgets (Barrett) is addressed in forthcoming manuscripts proving Barrett's PF-PINI(2) satisfaction (one-bit barrier) [3] and k-stage composition for PF-PINI gadgets under fresh-mask renewal [4].
- Abstract（参考訳）: ML-KEM (FIPS 203) と ML-DSA (FIPS 204) の量子後暗号 (PQC) アクセラレータは、パイプライン化された数理論変換 (NTT) の段階を$\mathbb{Z}_q$ に頼っている。
我々の以前の研究はスケール[1]で構造依存性解析を確立し、部分NTTマスキングのセキュリティマージンを定量化した[2]。
構成フレームワーク (ISW, t-SNI, PINI, DOM) は Boolean masking over $\mathrm{GF}(2)$; no proof assistant artifact address the NTT butterfly over $\mathbb{Z}_q$。
マシンでチェックした3つの結果は、Lean 4でMathlibとともに紹介します。
値独立性(value-independence)は、(代数的MutualInfoZeroプロキシを介して)新鮮なランダム性の下で一定の限界分布を意味する。
第二に、バタフライ・コンテクスト毎の一様性:$\mathbb{Z}/q\mathbb{Z}$$$q > 0$の新鮮な出力マスクを持つ任意のクーリー・タキー・バタフライに対して、各出力ワイヤは、正確に1つのマスク値を生成し、秘密とは独立に一様で、全てのモジュラー、ツイドル因子、入力に対して普遍である。
第3に、新しいステージごとのマスキングを備えたkステージNTTパイプラインは、ISW 1次探索モデルの下で、各ステージにおけるコンテキスト毎の均一性を満足する。
我々は、名前付き警告を文書化する: 蝶の出力に対して、ポイントワイドな値独立は偽である。
アダムズ・ブリッジ・アクセラレーター(CHIPS Alliance Caliptra)は、INTTの第0ラウンドでのみアクティブなマスクを行い、その構造的不安全をアーキテクチャ的に説明している。
アーティファクト:9つの定理、1,738のビルドジョブ。
バレットのPF-PINI(2)満足度(1ビット障壁)[3]と、新マスク更新時のPF-PINIガジェットのkステージ組成[4]を証明した近日刊行の原稿に、非線形ガジェットの組成(バレット)を対処する。
関連論文リスト
- From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification [0.0]
ポスト量子暗号(PQC)ハードウェアにおけるマスキングの形式的検証は、有限領域上のSMTソルバに依存する。
我々の以前の研究は大規模な構造依存解析を確立し、部分NTTマスキングのセキュリティマージンを定量化した。
構造依存分析フレームワークであるQANaryは、Adams Bridge ML-DSA/ML-KEMアクセラレーターの30モジュールにわたる117万の細胞を検証した。
論文 参考訳（メタデータ） (2026-04-20T18:17:22Z) - Cryptanalysis of the Legendre Pseudorandom Function over Extension Fields [0.0]
レジェンドレット擬似関数(Regendre Pseudorandom Function、PRF)は、レジェンドレットシンボル上に構築された高効率な暗号プリミティブである。
最近の関心は拡張フィールドの$mathbbF_pr$よりもインスタンス化に移行している。
本稿では, 1 度レジェンダー PRF を $mathbbF_pr$ で動作させる, 包括的な暗号解析手法を提案する。
論文 参考訳（メタデータ） (2026-04-06T16:35:32Z) - Adaptation to Intrinsic Dependence in Diffusion Language Models [5.185131234265025]
拡散言語モデル(DLM)は自己回帰(AR)アプローチに代わる有望な代替手段として登場した。
対象データ分布の(未知の)依存構造に適応するDLMの分布に依存しないアンマスキングスケジュールを提案する。
この結果は, 先行収束理論を著しく改善し, 低複雑さ分布に対する相当なサンプリング加速を得た。
論文 参考訳（メタデータ） (2026-02-23T18:41:34Z) - FIPS 204-Compatible Threshold ML-DSA via Masked Lagrange Reconstruction [0.0]
Masked Lagrange再構成は任意のしきい値が$T$のしきい値ML-DSAを可能にする。
修正されていない204実装で検証可能な標準3.3KBシグネチャを生成する。
論文 参考訳（メタデータ） (2026-01-28T18:13:47Z) - MaskPro: Linear-Space Probabilistic Learning for Strict (N:M)-Sparsity on Large Language Models [53.36415620647177]
半構造化された空間は、M$M$の重みからN$の要素を戦略的に保持することで、有望なソリューションを提供する。
既存の(N:M)互換のアプローチは通常、かなりのエラーに悩まされるルールベースの階層的な欲求探索と、禁止的なトレーニングコストを引き起こす勾配駆動学習の2つのカテゴリに分類される。
MaskProという新しい線形空間確率的フレームワークを提案する。これは、M$連続重みごとに事前のカテゴリー分布を学習し、その後、この分布を活用して(N:M)スパーシリティを$N$-wayサンプリングを通じて生成することを目的としている。
論文 参考訳（メタデータ） (2025-06-15T15:02:59Z) - Learning with Norm Constrained, Over-parameterized, Two-layer Neural Networks [54.177130905659155]
近年の研究では、再生カーネルヒルベルト空間(RKHS)がニューラルネットワークによる関数のモデル化に適した空間ではないことが示されている。
本稿では,有界ノルムを持つオーバーパラメータ化された2層ニューラルネットワークに適した関数空間について検討する。
論文 参考訳（メタデータ） (2024-04-29T15:04:07Z) - Communication-Constrained Bandits under Additive Gaussian Noise [111.06688156723018]
クライアントが学習者にコミュニケーション制約のあるフィードバックを提供する分散マルチアームバンディットについて検討する。
我々は、この下限を小さな加法係数にマッチさせるマルチフェーズ帯域幅アルゴリズム、$mathtUEtext-UCB++$を提案する。
論文 参考訳（メタデータ） (2023-04-25T09:31:20Z) - Minimax-Optimal Multi-Agent RL in Zero-Sum Markov Games With a
Generative Model [50.38446482252857]
2人プレイのゼロサムマルコフゲームは多エージェント強化学習においておそらく最も基本的な設定である。
我々は,$$ widetildeObiggを用いて,$varepsilon$-approximate Markov NEポリシーを学習する学習アルゴリズムを開発した。
我々は、分散型量の役割を明確にするFTRLに対する洗練された後悔境界を導出する。
論文 参考訳（メタデータ） (2022-08-22T17:24:55Z) - BRST-BV Quantum Actions for Constrained Totally-Symmetric Integer HS
Fields [77.34726150561087]
非最小制約BRST-BVラグランジアン定式化は、$d$次元ミンコフスキー空間における完全対称な質量を持たないHS場に対して提示される。
フォック空間量子作用は、全BRST-BV作用におけるゲージ固定フェルミオン$Psi$の変分微分により、全一般化場-反場ベクトルのシフトとして構成される。
論文 参考訳（メタデータ） (2020-10-29T16:40:32Z) - Provably Efficient Safe Exploration via Primal-Dual Policy Optimization [105.7510838453122]
制約付きマルコフ決定過程(CMDP)を用いた安全強化学習(SRL)問題について検討する。
本稿では,関数近似設定において,安全な探索を行うCMDPの効率の良いオンラインポリシー最適化アルゴリズムを提案する。
論文 参考訳（メタデータ） (2020-03-01T17:47:03Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。