Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking

Aquí se presenta un resumen técnico detallado del artículo "PINI de Campo Primo: Teoremas de Composición Verificados por Máquina para el Enmascaramiento NTT Post-Cuántico".

1. Planteamiento del Problema

El artículo aborda una brecha crítica en la verificación formal de seguridad del hardware de Criptografía Post-Cuántica (PQC), específicamente para las implementaciones de la Transformada Numérica Teórica (NTT) utilizadas en los estándares del NIST (ML-KEM y ML-DSA).

• El Contexto: Las implementaciones de hardware de NTT dependen del enmascaramiento aritmético sobre campos primos ($\mathbb{Z}_q$) para resistir ataques de canal lateral como el Análisis de Energía Diferencial (DPA).
• La Brecha: Mientras que el enmascaramiento booleano (sobre $GF(2^n)$) cuenta con una teoría de composición madura (NI, SNI, PINI) con pruebas verificadas por máquina, el enmascaramiento aritmético sobre campos primos carece de teoremas de composición análogos.
• El Problema Específico: En el enmascaramiento aritmético, operaciones como la reducción modular (por ejemplo, la reducción de Barrett) interactúan con las máscaras de formas no triviales. A diferencia del XOR booleano, donde el enmascaramiento preserva la uniformidad perfectamente, el enmascaramiento aritmético puede dar lugar a distribuciones de salida no uniformes (multiplicidad > 1).
• La Vulnerabilidad: Análisis empíricos y estudios estructurales previos identificaron vulnerabilidades en el acelerador PQC "Adams Bridge" de Microsoft, donde los cables intermedios entre etapas del pipeline eran no uniformes, permitiendo ataques DPA. Sin embargo, faltaba una explicación teórica formal sobre por qué ocurre esto y cómo solucionarlo mediante teoremas de composición.

2. Metodología

Los autores emplean verificación formal utilizando el asistente de pruebas Lean 4 para derivar y probar teoremas de composición para el enmascaramiento aritmético.

• Modelo Formal: Definen una métrica de seguridad cuantitativa llamada PF-PINI(k) (No Interferencia de Aislamiento de Sondas en Campo Primo).
  • A diferencia de las nociones de seguridad binarias (seguro/inseguro), PF-PINI mide la multiplicidad de los valores de salida en relación con el espacio de máscaras.
  • $k=1$ implica una distribución perfectamente uniforme.
  • $k=2$ implica una multiplicidad máxima de 2, filtrando hasta 1 bit de información por cable.
• El "Argumento de Renovación": La idea teórica central es que aplicar una máscara aleatoria fresca entre dos etapas del pipeline borra completamente el parámetro de seguridad ($k_1$) de la primera etapa del cable intermedio, independientemente de cuán no uniforme haya sido la salida de la primera etapa.
• Puente de Hardware: Los autores conectan formalmente la brecha entre modelos algebraicos abstractos ($\mathbb{Z}_q$) y la aritmética de números naturales (Nat) fiel al hardware utilizada en diseños RTL, específicamente para la reducción de Barrett.
• Alcance de la Verificación: Toda la obra consta de 18 teoremas verificados por máquina con cero stubs sorry (sin suposiciones no probadas), garantizando seguridades de alta confianza.

3. Contribuciones Clave

El artículo realiza seis contribuciones principales:

1. El Teorema de Renovación (Teorema 4.1): Prueba que si se aplica una máscara aleatoria fresca entre dos etapas ($G_1 \to G_2$), el cable intermedio se vuelve perfectamente uniforme. El conjunto de pares de máscaras que producen un valor intermedio específico tiene una cardinalidad exactamente igual a $q$, independiente del parámetro de seguridad de $G_1$.
2. Teorema de Composición Positiva (Teorema 4.4): Demuestra que un pipeline de dos etapas con enmascaramiento fresco satisface PF-PINI($k_2$). La seguridad de la salida compuesta depende únicamente del parámetro de la segunda etapa ($k_2$); la debilidad de la primera etapa ($k_1$) se borra completamente.
3. Teoremas de Composición Negativa (Teoremas 5.1–5.3): Prueba que sin enmascaramiento fresco, el cable intermedio retiene la multiplicidad de la primera etapa ($k_1$). Si $k_1 > 1$, el cable es no uniforme, creando una condición necesaria para ataques DPA.
4. Puente Algebraico-Hardware (Teorema 6.1): Prueba formalmente que el mapa de reducción algebraica de Barrett es equivalente al mapa de aritmética Nat fiel al hardware bajo condiciones de alcance estándar ($q \le 2^s$). Esto valida que los límites teóricos se aplican directamente a implementaciones de silicio.
5. Diagnóstico de Adams Bridge: Instancia formalmente los teoremas para diagnosticar el acelerador Adams Bridge de Microsoft. La prueba confirma que la falta de enmascaramiento fresco entre etapas deja los cables de salida de Barrett no uniformes (PF-PINI(2)), explicando el éxito de los ataques DPA empíricos previos.
6. Barrera Universal de 1 Bit: Proporciona evidencia computacional de que el límite PF-PINI(2) es universal para reducciones modulares (tanto Barrett como Montgomery), sugiriendo una "Barrera de 1 Bit" fundamental para estas operaciones.

4. Resultados Clave

• Prueba Formal de Composición: El artículo establece que el enmascaramiento fresco entre etapas es la condición necesaria y suficiente para componer gadgets aritméticos de manera segura.
• Seguridad Cuantitativa:
  • Con Enmascaramiento Fresco: El cable intermedio es uniforme ($k=1$). La salida final está acotada por el parámetro de la segunda etapa ($k_2$).
  • Sin Enmascaramiento Fresco: El cable intermedio es no uniforme (hasta $k_1$). Esta no uniformidad es la causa raíz de la filtración de canal lateral observada en ataques empíricos.
• Solución para Adams Bridge: El diagnóstico confirma que añadir un único registro de máscara aleatoria fresca y una operación de resta entre las etapas de Mariposa y Barrett en el pipeline de Adams Bridge eliminaría la vulnerabilidad DPA en los cables intermedios sin cambiar el parámetro de seguridad de salida final.
• Disponibilidad del Artefacto: El código fuente completo de Lean 4, que incluye 18 teoremas y un script de reproducción, está disponible públicamente, permitiendo la verificación independiente de las pruebas.

5. Significado

• Primera Composición Aritmética Verificada por Máquina: Este es el primer trabajo que proporciona teoremas de composición verificados por máquina para el enmascaramiento aritmético sobre campos primos, llenando un vacío teórico mayor en la seguridad del hardware PQC.
• Uniendo Teoría y Práctica: Al vincular formalmente pruebas algebraicas abstractas con aritmética fiel al hardware, el artículo proporciona una base rigurosa para verificar diseños de silicio del mundo real, yendo más allá de las pruebas empíricas.
• Directriz de Diseño: Establece una regla de diseño clara y demostrable para el hardware PQC: Siempre insertar enmascaramiento fresco entre etapas del pipeline. Este simple cambio arquitectónico garantiza que la seguridad del pipeline compuesto esté determinada únicamente por el eslabón más débil de la etapa final, y no de las intermedias.
• Convergencia de Evidencias: La prueba formal se alinea perfectamente con tres análisis previos independientes (análisis de potencia empírico, revisión de código y análisis de dependencia estructural), confirmando que el defecto arquitectónico identificado en el acelerador Adams Bridge es de hecho la causa raíz de su vulnerabilidad.

En resumen, este artículo proporciona el respaldo matemático y de verificación formal necesario para diseñar aceleradores de hardware seguros, composibles y resistentes a canales laterales para la nueva era de la Criptografía Post-Cuántica.