Rank Ceiling for Twiddle-Perturbation Faults on the Forward NTT
Chakshu Gupta
cs.CR
Oct 21, 2026 · v3
TL;DR
A Lean 4/Mathlib artifact certifies the one-per-layer kernel results for 256-coefficient forward NTT shapes over fields with characteristic not two, plus inverse-NTT kernel equalities.
Abstract
ML-KEM and ML-DSA compute forward number-theoretic transforms on secret polynomials. Their fixed multipliers, or twiddles, are a documented fault-attack target. This paper characterises the linear map from a secret polynomial to the difference between correct and faulted transform outputs. Each selected twiddle takes a fixed changed field value at every use during one call; zero and nonzero replacements are covered. For one replacement, rank equals the number of butterflies sharing its twiddle, halving by layer from 128 to 2 for ML-KEM and to 1 for ML-DSA. With one replacement per layer, known fault positions, replacement values and a raw transform difference determine every coefficient except the constant and linear coefficients for ML-KEM, or the constant for ML-DSA. Lean 4 certifies this result for both 256-coefficient shapes over fields of characteristic other than two, with nonzero original twiddles. Those coefficients cancel from the difference for every allowed fault set and replacement choice. Seed storage motivates comparing a known correct public key with a released faulty key from the same seed. If only one ML-KEM secret-polynomial transform is affected and all other computations are unchanged, the decoded key difference is a known matrix column times the transform difference. An invertible column entry reconstructs the latter. For ML-DSA, reconstruction and exact candidate counts from paired compressed keys remain unestablished.
Problem
ML-KEM and ML-DSA apply forward number-theoretic transforms to secret polynomials, and their twiddle factors are a documented fault-attack target. No general rank-and-kernel law was known for the linear map from the input to the correct-minus-faulted transform difference under arbitrary twiddle replacements.
Approach
The faulted NTT is decomposed as a composition of invertible butterfly layers, so each difference map factors as an invertible prefix, a local layer difference, and an invertible suffix. This yields single-fault and per-layer rank results, plus a universal kernel inclusion for every fault set. The one-per-layer kernel claims and the inverse kernel equalities at n=256 are formalized in Lean 4.27.0 with Mathlib, over an arbitrary field with 2≠0 and nonzero original twiddles. Python numerical checks using Gaussian elimination over F_q complement the proofs.
Results
A single replacement has rank equal to the number of butterflies sharing that twiddle, halving by layer from 128 to 2 (ML-KEM) or to 1 (ML-DSA). With one replacement per layer, the kernel is spanned exactly by the constant and linear coefficients for ML-KEM, or the constant coefficient for ML-DSA. For ML-KEM, a correct and a faulty public key from the same seed reconstruct the transform difference when the affected matrix column has an invertible entry.
| Layer | ML-KEM (n=256) | Complete shape (n=32) |
|---|
| 0 | 128 | 16 |
| 1 | 64 | 8 |
| 2 | 32 | 4 |
| 3 | 16 | 2 |
| 4 | 8 | 1 |
Singleton zeroing ranks by layer (complete shape at (n,q)=(32,193))
