The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware

Technical Summary: The 1-Bit Barrier is Universal

Problem Statement
The Number Theoretic Transform (NTT) serves as the computational backbone for NIST post-quantum cryptography (PQC) standards ML-DSA (FIPS 204) and ML-KEM (FIPS 203). Hardware implementations of these standards rely on arithmetic masking to resist side-channel attacks, specifically Differential Power Analysis (DPA). While Boolean masking over $GF(2^n)$ has established composability frameworks (e.g., PINI), arithmetic masking over $\mathbb{Z}_q$ for prime $q$ presents unique challenges.

Prior work in the QANARY program (Papers 1–6) established structural dependency analyses and quantified security margins for specific components, notably proving that Barrett reduction satisfies a "1-Bit Barrier" (PF-PINI(2)). However, two critical gaps remained:

1. Arbitrary Pipeline Depth: Previous composition theorems were limited to two stages. There was no formal guarantee for arbitrary $k$-stage pipelines with fresh inter-stage masking.
2. Montgomery Reduction: While Barrett reduction was characterized, Montgomery reduction—the second standard modular reduction used in NTT hardware (dominant in ML-DSA and some ML-KEM implementations)—lacked a formal PF-PINI characterization.
3. Unified End-to-End Bounds: There was no single, machine-checked cardinality bound that assembled the results for arbitrary pipelines composed of butterflies, Barrett, and Montgomery reductions.

Methodology
The paper employs formal verification using the Lean 4 proof assistant. The approach is strictly constructive, with zero sorry (unproven assumptions) and zero non-standard axioms. The methodology relies on:

• PF-PINI Definition: Using the Prime-Field Probe Isolating Non-Interference (PF-PINI) parameter, which quantifies the leakage of a single-wire gadget under a single arithmetic mask. A gadget is PF-PINI($M$) if the cardinality of the preimage of any output value is at most $M$.
• Pipeline Modeling: Defining a $k$-stage pipeline where each stage $G_i$ is a PF-PINI gadget, separated by fresh random masks. The pipeline output is computed recursively.
• Combinatorial Analysis: Proving that fresh inter-stage masking "erases" the leakage parameters of intermediate stages, leaving the final bound dependent only on the last stage's parameter.
• Hardware-Faithful Modeling: Modeling Montgomery reduction to account for hardware register widths and wraparound behavior, specifically analyzing the collision offset $2^{w-s}$.

Key Contributions
The paper makes four primary contributions, all formalized in Lean 4:

1. The $k$-Stage Composition Theorem (Theorem 3.1):
   This theorem generalizes the previous 2-stage composition result to arbitrary depth $k \ge 1$. It proves that for a pipeline of gadgets $G_0, \dots, G_{k-1}$ with fresh inter-stage masking, the cardinality of the preimage of the output is bounded by:
   $$| \{ (m, f) : \text{pipeline output} = v \} | \le G_{k-1}.\text{maxMult} \cdot q^{2k-2}$$
   Crucially, the bound is last-stage-determined; the parameters of all intermediate stages are erased by the fresh masks.

2. Montgomery Reduction is PF-PINI(2) (Theorem 4.3):
   The paper formally proves that Montgomery reduction satisfies the PF-PINI(2) property, mirroring the structure of Barrett reduction. It demonstrates that the hardware-faithful Montgomery map has a "two-branch" structure (dependent on whether a wraparound occurs), resulting in a preimage cardinality of at most 2. Theorem 4.7 further establishes the tightness of this bound, showing that for standard parameters (ML-KEM and ML-DSA), the multiplicity is exactly 2.

3. End-to-End Multiplicity Bound (Theorem 5.1):
   By combining the $k$-stage composition theorem with the specific PF-PINI(2) results for Barrett (Paper 5), Montgomery (this paper), and butterflies (Paper 4), the paper establishes a unified bound. For any $k$-stage pipeline where every stage satisfies $\text{maxMult} \le 2$, the output preimage cardinality is bounded by:
   $$2 \cdot q^{2k-2}$$
   Under the first-order probing model with uniform masks, this corresponds to a per-observation conditional probability bound of $2/q$, independent of the pipeline depth $k$.

4. Formal Anchoring of Empirical Findings (Theorem 5.4):
   The paper provides a Lean-verified conditional stating that if any stage in a pipeline has $\text{maxMult} \ge 3$ (e.g., an unmasked stage), the hypothesis of the end-to-end bound fails. This formally anchors prior empirical and structural analyses of the "Adams Bridge" PQC accelerator (Papers 1, 2, and external works), confirming that specific unmasked configurations in that design fall outside the sufficient conditions for the depth-independent bound.

Results

• Universality of the 1-Bit Barrier: The paper confirms that the "1-Bit Barrier" (a preimage cardinality of 2) applies to both standard modular reductions (Barrett and Montgomery) used in NIST PQC hardware.
• Depth Independence: The formal proofs demonstrate that adding stages to a pipeline does not degrade the per-observation leakage bound, provided fresh inter-stage masking is used and every stage satisfies PF-PINI($\le 2$).
• Verification Status: The entire artifact consists of 20 declarations across three theorem modules, building in 1,753 jobs with zero errors, zero sorry, and no native decision procedures.

Significance and Claims
The paper positions itself as the completion of a formal verification program for masked NTT hardware. Its significance lies in providing a quantitative, machine-checked compositional foundation for hardware designers.

• For Certification: The derived cardinality bound ($2 \cdot q^{2k-2}$) provides the specific evidence required for DPA-resistance arguments at the architecture level, complementing gate-level tools like SILVER and maskVerif.
• For Designers: It offers a prescriptive remediation path: to achieve a depth-independent bound, designers must ensure every stage is PF-PINI($\le 2$) and insert fresh masks between stages.
• Modesty of Claims: The authors explicitly state that the probability and min-entropy interpretations (e.g., $2/q$) are informal semantic consequences of the cardinality bounds and are not mechanically formalized in Lean. Furthermore, regarding the Adams Bridge analysis, the paper claims only that specific configurations fail the sufficient conditions of Theorem 5.1; it does not claim the hardware is "broken" or "insecure," acknowledging that alternative frameworks or stronger models might yield different conclusions. The work is framed as a tool for compositional analysis rather than a definitive security verdict on specific implementations.