論文の概要: 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ハードウェアにおける算術的マスキングのための機械式証明
- 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]を証明した近日刊行の原稿に、非線形ガジェットの組成(バレット)を対処する。
関連論文リスト
- SSTQ:Privacy-Preserving Vector Quantization via Subsampled Stochastic TurboQuant [79.24089819400126]
Subsampled TurboQuant (SSTQ) は、オーバーコンプリートな等幅のタイトフレーム、座標サブサンプリング、プライバシ対応量子化を組み合わせたフレームワークである。
SSTQは平均2乗誤差スケーリングを実現し、クライアントあたり$lceil log N il + b$ bitsを使用する。
また、コードブックに依存したMSEスケーリングを$O(4b)$から$O(2b)$に削減する、プライバシを意識したコードブックの目的も導出します。
論文 参考訳（メタデータ） (2026-08-05T17:51:25Z) - Minimax Optimal Variance-Aware Regret Bounds for Multinomial Logistic MDPs [56.28491566735463]
既存のマルコフ決定過程のアルゴリズムは、$smashtildeO(dH2sqrtT)$を後悔する。
本稿では,最悪の場合において既存の境界を復元し,構造化されたMDPに対して改善する,$smashtildeO(dH2bar_TsqrtT)$の後悔を実現するアルゴリズムを提案する。
論文 参考訳（メタデータ） (2026-05-19T12:39:32Z) - The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware [0.0]
本稿では,ポスト量子暗号のためのマスク付きNTTハードウェアの一連の公式な解析をクローズする。
ステージ間マスキングとステージごとのPF-PINI($leq 2$)ガジェットを備えた、任意深度$k$ステージのNTTパイプラインは、2 cdot q2k-2$の観測基数を満たす。
論文 参考訳（メタデータ） (2026-05-04T17:32:31Z) - Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking [0.0]
我々は、我々の知る限り、素体上の算術マスキングのための最初の機械チェックされた合成定理を証明した。
パラメータが$k_$と$k$の2つのPF-PINIガジェットの場合、合成された2段パイプラインは、PF-PINI($k$)を満たす。
バレット還元の代数とハードウェアに忠実な算術モデルを正式にブリッジし、定理をインスタンス化し、MicrosoftのAdams Bridge PQCアクセラレーターを診断する。
論文 参考訳（メタデータ） (2026-04-28T17:21:20Z) - Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware [0.0]
バレットリダクションはNTTベースのポスト量子暗号実装のすべての非線形コアである。
既存の構成フレームワークはGF(2)上のマスキングに対処している。
PF-PINIはPF-PINI(2)を満たす。
論文 参考訳（メタデータ） (2026-04-27T16:27:33Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。