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

Resumen Técnico: La Barrera de 1 Bit es Universal

Enunciado del Problema
La Transformada Numérica Teórica (NTT) sirve como columna vertebral computacional para los estándares de criptografía postcuántica (PQC) del NIST ML-DSA (FIPS 204) y ML-KEM (FIPS 203). Las implementaciones en hardware de estos estándares dependen del enmascaramiento aritmético para resistir ataques de canal lateral, específicamente el Análisis de Potencia Diferencial (DPA). Si bien el enmascaramiento booleano sobre $GF(2^n)$ ha establecido marcos de composabilidad (por ejemplo, PINI), el enmascaramiento aritmético sobre $\mathbb{Z}_q$ para un primo $q$ presenta desafíos únicos.

Trabajos previos en el programa QANARY (Papers 1–6) establecieron análisis de dependencias estructurales y cuantificaron márgenes de seguridad para componentes específicos, demostrando notablemente que la reducción de Barrett satisface una "Barrera de 1 Bit" (PF-PINI(2)). Sin embargo, permanecían dos brechas críticas:

1. Profundidad de Pipeline Arbitraria: Los teoremas de composición anteriores se limitaban a dos etapas. No existía una garantía formal para pipelines de $k$ etapas arbitrarias con enmascaramiento fresco entre etapas.
2. Reducción de Montgomery: Mientras que la reducción de Barrett fue caracterizada, la reducción de Montgomery —la segunda reducción modular estándar utilizada en hardware NTT (dominante en ML-DSA y algunas implementaciones de ML-KEM)— carecía de una caracterización formal PF-PINI.
3. Límites Unificados de Extremo a Extremo: No existía un único límite de cardinalidad verificado por máquina que ensamblara los resultados para pipelines arbitrarias compuestas por mariposas, reducciones de Barrett y reducciones de Montgomery.

Metodología
El artículo emplea verificación formal utilizando el asistente de pruebas Lean 4. El enfoque es estrictamente constructivo, con cero sorry (suposiciones no probadas) y cero axiomas no estándar. La metodología se basa en:

• Definición PF-PINI: Uso del parámetro de No Interferencia de Aislamiento de Sondas de Campo Primo (PF-PINI), que cuantifica la fuga de un gadget de un solo cable bajo una única máscara aritmética. Un gadget es PF-PINI($M$) si la cardinalidad de la preimagen de cualquier valor de salida es como máximo $M$.
• Modelado de Pipeline: Definición de una pipeline de $k$ etapas donde cada etapa $G_i$ es un gadget PF-PINI, separadas por máscaras aleatorias frescas. La salida de la pipeline se calcula recursivamente.
• Análisis Combinatorio: Demostración de que el enmascaramiento fresco entre etapas "borra" los parámetros de fuga de las etapas intermedias, dejando que el límite final dependa únicamente del parámetro de la última etapa.
• Modelado Fiel al Hardware: Modelado de la reducción de Montgomery para tener en cuenta los anchos de registros de hardware y el comportamiento de desbordamiento (wraparound), analizando específicamente el desplazamiento de colisión $2^{w-s}$.

Contribuciones Clave
El artículo realiza cuatro contribuciones principales, todas formalizadas en Lean 4:

1. El Teorema de Composición de $k$ Etapas (Teorema 3.1):
   Este teorema generaliza el resultado anterior de composición de 2 etapas a una profundidad arbitraria $k \ge 1$. Demuestra que para una pipeline de gadgets $G_0, \dots, G_{k-1}$ con enmascaramiento fresco entre etapas, la cardinalidad de la preimagen de la salida está acotada por:
   $$| \{ (m, f) : \text{salida de pipeline} = v \} | \le G_{k-1}.\text{maxMult} \cdot q^{2k-2}$$
   Crucialmente, el límite está determinado por la última etapa; los parámetros de todas las etapas intermedias son borrados por las máscaras frescas.

2. La Reducción de Montgomery es PF-PINI(2) (Teorema 4.3):
   El artículo demuestra formalmente que la reducción de Montgomery satisface la propiedad PF-PINI(2), reflejando la estructura de la reducción de Barrett. Muestra que el mapa de Montgomery fiel al hardware tiene una estructura de "dos ramas" (dependiente de si ocurre un desbordamiento), resultando en una cardinalidad de preimagen de como máximo 2. El Teorema 4.7 establece además la estrechez de este límite, mostrando que para parámetros estándar (ML-KEM y ML-DSA), la multiplicidad es exactamente 2.

3. Límite de Multiplicidad de Extremo a Extremo (Teorema 5.1):
   Combinando el teorema de composición de $k$ etapas con los resultados específicos PF-PINI(2) para Barrett (Paper 5), Montgomery (este artículo) y mariposas (Paper 4), el artículo establece un límite unificado. Para cualquier pipeline de $k$ etapas donde cada etapa satisface $\text{maxMult} \le 2$, la cardinalidad de la preimagen de salida está acotada por:
   $$2 \cdot q^{2k-2}$$
   Bajo el modelo de sondeo de primer orden con máscaras uniformes, esto corresponde a un límite de probabilidad condicional por observación de $2/q$, independiente de la profundidad de la pipeline $k$.

4. Anclaje Formal de Hallazgos Empíricos (Teorema 5.4):
   El artículo proporciona una condición verificada en Lean que establece que si cualquier etapa en una pipeline tiene $\text{maxMult} \ge 3$ (por ejemplo, una etapa sin enmascarar), la hipótesis del límite de extremo a extremo falla. Esto ancla formalmente análisis empíricos y estructurales previos del acelerador PQC "Adams Bridge" (Papers 1, 2 y trabajos externos), confirmando que configuraciones específicas sin enmascarar en ese diseño quedan fuera de las condiciones suficientes para el límite independiente de la profundidad.

Resultados

• Universalidad de la Barrera de 1 Bit: El artículo confirma que la "Barrera de 1 Bit" (una cardinalidad de preimagen de 2) se aplica a ambas reducciones modulares estándar (Barrett y Montgomery) utilizadas en hardware PQC del NIST.
• Independencia de la Profundidad: Las pruebas formales demuestran que agregar etapas a una pipeline no degrada el límite de fuga por observación, siempre que se utilice enmascaramiento fresco entre etapas y cada etapa satisfaga PF-PINI($\le 2$).
• Estado de Verificación: Todo el artefacto consiste en 20 declaraciones a través de tres módulos de teoremas, compilando en 1.753 trabajos con cero errores, cero sorry y sin procedimientos de decisión nativos.

Significado y Afirmaciones
El artículo se posiciona como la finalización de un programa de verificación formal para hardware NTT enmascarado. Su significado radica en proporcionar una base composicional cuantitativa y verificada por máquina para los diseñadores de hardware.

• Para Certificación: El límite de cardinalidad derivado ($2 \cdot q^{2k-2}$) proporciona la evidencia específica requerida para argumentos de resistencia a DPA a nivel de arquitectura, complementando herramientas a nivel de puerta como SILVER y maskVerif.
• Para Diseñadores: Ofrece un camino de remediación prescriptivo: para lograr un límite independiente de la profundidad, los diseñadores deben asegurar que cada etapa sea PF-PINI($\le 2$) e insertar máscaras frescas entre etapas.
• Modestia de las Afirmaciones: Los autores declaran explícitamente que las interpretaciones de probabilidad y entropía mínima (por ejemplo, $2/q$) son consecuencias semánticas informales de los límites de cardinalidad y no están formalizadas mecánicamente en Lean. Además, respecto al análisis de Adams Bridge, el artículo afirma únicamente que configuraciones específicas fallan las condiciones suficientes del Teorema 5.1; no afirma que el hardware esté "roto" o "inseguro", reconociendo que marcos alternativos o modelos más fuertes podrían arrojar conclusiones diferentes. El trabajo se enmarca como una herramienta para el análisis composicional en lugar de un veredicto de seguridad definitivo sobre implementaciones específicas.