Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware

A continuación se presenta un resumen técnico detallado del artículo "Límites de cardinalidad verificados por máquina para la reducción de Barrett enmascarada: Una barrera de fuga de canal lateral de 1 bit en hardware criptográfico post-cuántico".

1. Enunciado del Problema

Los estándares de Criptografía Post-Cuántica (PQC) como ML-KEM (FIPS 203) y ML-DSA (FIPS 204) dependen en gran medida de las líneas de transformación numérica (NTT). Estas líneas de procesamiento constan de etapas lineales de "mariposa" y etapas no lineales de reducción modular, típicamente implementadas mediante reducción de Barrett.

Aunque los marcos existentes de verificación formal (ISW, t-SNI, PINI, DOM) ofrecen garantías sólidas para el enmascaramiento booleano sobre $GF(2)$, carecen de caracterizaciones verificadas por máquina para el enmascaramiento aritmético sobre campos primos ($\mathbb{Z}_q$), específicamente para la reducción de Barrett.

• La Brecha: Las implementaciones de hardware (por ejemplo, el diseño "Adams Bridge") a menudo sufren vulnerabilidades de canal lateral porque la sustracción condicional no lineal en la reducción de Barrett rompe la estructura afín asumida por los teoremas de composición estándar.
• La Pregunta: Bajo enmascaramiento aritmético de primer orden, ¿cuál es el límite preciso de fuga de los cables internos de un circuito de reducción de Barrett? Las herramientas anteriores no podían proporcionar una respuesta universal verificada por máquina, lo que generaba incertidumbre en la certificación FIPS 140-3.

2. Metodología

Los autores emplean un enfoque de verificación formal utilizando el asistente de pruebas Lean 4 y la biblioteca Mathlib.

• Formalización: Definen el mapa de cables internos de Barrett algebraicamente sobre $\mathbb{Z}_q$ (donde $q$ es el módulo). El mapa $f_x(m)$ toma un secreto $x$ y una máscara aleatoria $m$, produciendo una salida basada en una estructura de dos ramas determinada por una sustracción condicional.
• Estrategia de Prueba: En lugar de simular instancias específicas, prueban teoremas universales que se cumplen para todos los $q > 0$ y parámetros de desplazamiento $s$.
• Concepto Clave: Analizan la cardinalidad de la preimagen: para un secreto fijo $x$ y un valor de salida específico $v$, ¿cuántas máscaras distintas $m$ podrían haber producido $v$?
• Cadena de Herramientas: El artefacto contiene 12 resultados probados con cero sorry (ninguna prueba incompleta), asegurando que cada paso sea verificado por el núcleo de Lean.

3. Contribuciones Clave

A. El Teorema de la Tricotomía

El artículo demuestra que el mapa de cables internos de Barrett exhibe una estructura de preimagen de tres valores. Para cualquier secreto $x$ y cualquier salida $v$, el número de máscaras $m$ tal que $f_x(m) = v$ es exactamente 0, 1 o 2.

• Mecanismo: La sustracción condicional crea dos ramas afines (traslaciones en $\mathbb{Z}_q$). La preimagen de cualquier valor es un subconjunto de como máximo dos candidatos: $\{x - v, x - v + r\}$, donde $r = 2^s \mod q$.
• Universalidad: Esto se cumple para cualquier módulo $q$ y desplazamiento $s$, independientemente de los parámetros específicos de PQC.

B. La Barrera de 1 Bit

Basándose en la tricotomía, los autores establecen un límite de fuga universal:

• Máxima Multiplicidad: Dado que el número máximo de máscaras que producen una sola salida es 2, la probabilidad máxima de observar un valor de salida específico es $2/q$.
• Límite de Entropía Mínima: La entropía mínima condicional $H_\infty(\text{salida} \mid x)$ está acotada inferiormente por $\log_2(q) - 1$.
• Interpretación: La reducción de Barrett filtra como máximo 1 bit de entropía mínima por cable interno bajo sondeo de primer orden. Este es un límite "conservador" porque muchos valores de salida son inalcanzables (conteo de preimagen = 0), lo que significa que la fuga real a menudo es estrictamente menor a 1 bit.

C. El Marco PF-PINI

Los autores introducen PINI de Campo Primo (PF-PINI), una nueva métrica de seguridad para gadgets aritméticos sobre $\mathbb{Z}_q$:

• Definición: Un gadget es PF-PINI($k$) si la cardinalidad de la preimagen está acotada por $k$.
• Instanciaciones:
  • Etapa de Mariposa: Satisface PF-PINI(1) (biyección perfecta, fuga cero más allá de la máscara).
  • Reducción de Barrett: Satisface PF-PINI(2) (la Barrera de 1 Bit).
• Observación de Composición: Observan (aunque aún no formalmente probado) que si las etapas de la línea de procesamiento están separadas por enmascaramiento fresco inter-etapa, la máxima multiplicidad de la línea de procesamiento compuesta es $\max(k_1, k_2)$. Esto implica que la Barrera de 1 Bit se propaga a través de toda la línea de procesamiento NTT.

4. Resultados y Análisis

• Pruebas Verificadas por Máquina: El artefacto incluye 12 teoremas verificados, incluyendo la tricotomía, pruebas de ajuste (que muestran que el conteo=2 es alcanzable) e instanciaciones de PF-PINI.
• Descubrimiento de Brecha de Soporte: El análisis revela valores de salida "inalcanzables" (conteo de preimagen = 0). Esto es una característica de seguridad, no un error, ya que reduce la información efectiva del adversario.
• Estudio de Caso Adams Bridge: El artículo analiza la implementación de hardware "Adams Bridge":
  • Fallo intra-etapa: Trabajos anteriores (Papers 1 y 2) mostraron vulnerabilidades debido a la interacción de compartimentos sin enmascaramiento intermedio.
  • Fallo inter-etapa: Este artículo identifica que Adams Bridge falla al aplicar enmascaramiento fresco entre etapas. En consecuencia, el límite de composición PF-PINI no se aplica, permitiendo que la fuga se multiplique ($k_1 \times k_2$) en lugar de permanecer acotada por el máximo ($\max(k_1, k_2)$). Esto explica por qué el diseño es vulnerable a pesar de que la Barrera de 1 Bit existe para las puertas individuales de Barrett.
• Impacto Cuantitativo:
  • Para ML-KEM ($q=3329$): Fuga $\le 1$ bit (Entropía mínima $\ge 10.70$ bits).
  • Para ML-DSA ($q=8,380,417$): Fuga $\le 1$ bit (Entropía mínima $\ge 21.99$ bits).

5. Significado

• Preparación para Certificación: La Barrera de 1 Bit proporciona un certificado universal y verificado por máquina para los diseñadores de hardware. Permite a los evaluadores certificar implementaciones basadas en Barrett para FIPS 140-3 sin volver a verificar conjuntos de parámetros específicos.
• Guía de Diseño: Aclara que el requisito arquitectónico principal para la seguridad es el enmascaramiento fresco inter-etapa. Si esto se implementa, la naturaleza no lineal de la reducción de Barrett no compromete la seguridad de la línea de procesamiento NTT más allá de una pérdida insignificante de 1 bit.
• Cambio Metodológico: El artículo traslada el análisis de canales laterales de la simulación empírica y la verificación basada en SAT a pruebas algebraicas verificadas por el núcleo, estableciendo un nuevo estándar para la verificación de hardware PQC.
• Completando el Programa de Cinco Artículos: Este trabajo cierra la brecha dejada por artículos anteriores en la serie, pasando de la construcción de herramientas (Artículo 1) y la cuantificación de ataques (Artículo 2) a fundamentos algebraicos (Artículo 3), composición lineal (Artículo 4) y, finalmente, caracterización no lineal (Artículo 5).

6. Limitaciones y Trabajo Futuro

• Prueba de Composición: La afirmación de que $\max(k_1, k_2)$ se cumple para líneas de procesamiento compuestas con enmascaramiento fresco es actualmente una observación, no un teorema formal.
• Enmascaramiento de Orden Superior: Los resultados se limitan al enmascaramiento de primer orden ($t=1$). La seguridad de orden superior requiere analizar preimágenes conjuntas a través de múltiples cables.
• Formalización de Entropía: Aunque se ha demostrado el límite algebraico, el límite de entropía mínima teórica de la información depende de definiciones estándar que aún no se han incorporado completamente en Mathlib.
• Otras Reducciones: Los resultados son específicos de la reducción de Barrett; las reducciones de Montgomery y de libro de texto requieren un análisis separado.

En resumen, este artículo establece que la reducción de Barrett es fundamentalmente segura bajo enmascaramiento aritmético de primer orden, filtrando no más de 1 bit de información por cable, siempre que se aplique enmascaramiento fresco entre las etapas de la línea de procesamiento. Esto proporciona una base matemática rigurosa para asegurar el hardware PQC de próxima generación.