💻 computer science

Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware

Este trabajo presenta la primera verificación formal en Lean 4 que demuestra que el enmascaramiento aritmético con valores frescos en cada etapa garantiza la seguridad de las tuberías de la Transformada Numérica Teórica (NTT) para aceleradores de criptografía postcuántica, cerrando brechas teóricas previas y exponiendo vulnerabilidades arquitectónicas en implementaciones existentes como Adams Bridge.

Autores originales: Ray Iskander, Khaled Kirah

Publicado 2026-04-23

📖 4 min de lectura☕ Lectura para el café

CC BY 4.0

Autores originales: Ray Iskander, Khaled Kirah

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

¡Claro que sí! Imagina que este paper es como un manual de seguridad para una fábrica de llaves secretas que protege nuestros datos contra computadoras del futuro (las "cuánticas").

Aquí tienes la explicación sencilla, usando analogías de la vida real:

1. El Problema: La Fábrica de Ensamblaje (NTT)

Imagina que tienes una línea de montaje muy rápida para crear llaves secretas. Esta línea tiene muchas estaciones de trabajo (llamadas "etapas" o stages). En cada estación, los trabajadores toman dos piezas, las mezclan y las pasan a la siguiente estación.

El problema es que los espías (hackers) pueden poner una pequeña cámara en cualquier estación para ver qué pasa. Si la cámara ve algo que revela la llave secreta, ¡la seguridad se rompe!

Para protegerse, los ingenieros usan un truco llamado "enmascaramiento": en cada estación, mezclan la pieza secreta con un "ruido" aleatorio (una máscara) para que la cámara solo vea basura inútil.

2. La Pregunta de Oro: ¿Funciona si cada estación está segura?

Aquí es donde entra la intuición de los ingenieros: "Si cada estación individual tiene su propia cámara de seguridad y su propio ruido, entonces toda la línea de montaje debería ser segura".

Pero, la intuición no es una prueba matemática. Nadie había demostrado con certeza absoluta (usando un "juez" matemático llamado Lean 4) que esta idea funcionaba para este tipo específico de fábrica. De hecho, había un trampa muy peligrosa.

3. La Trampa: El "Cambio de Valor" vs. La "Distribución Uniforme"

El paper descubre un error común que podría hacer que los ingenieros descarten diseños seguros o acepten diseños inseguros.

La Trampa (Lo que NO debes mirar): Imagina que fijas el "ruido" (la máscara) y cambias la llave secreta. Si la cámara ve que el resultado cambia, el ingeniero piensa: "¡Oh no! La cámara vio el secreto. ¡Es inseguro!".
- La realidad: ¡Falso! En esta fábrica, es normal que el resultado cambie si cambias la llave, siempre y cuando el "ruido" sea aleatorio. Si te fijas solo en un momento fijo, parece inseguro, pero es una ilusión óptica.
La Solución (Lo que SÍ debes mirar): La verdadera seguridad no es que el resultado no cambie, sino que cuando el ruido es fresco y aleatorio, el resultado parece totalmente aleatorio para el espía. Es como lanzar un dado: si lanzas un dado con un número secreto debajo, el resultado (1, 2, 3...) siempre depende del secreto, pero si el dado está "cargado" con una máscara perfecta, el espía no puede adivinar cuál era el secreto porque todos los resultados son igualmente probables.

4. El Hallazgo Principal: "El Puente Adams"

Los autores probaron matemáticamente (sin errores, con un 100% de certeza) que:

Si cada estación de la línea de montaje usa un nuevo ruido fresco (una nueva máscara aleatoria) en cada paso, la línea entera es inmune a los espías.
Esto funciona para cualquier tamaño de fábrica y cualquier tipo de número.

El caso real (Adams Bridge):
Los autores miraron un diseño real llamado "Adams Bridge" (usado en un chip de seguridad famoso). Descubrieron que este diseño rompe la regla de oro:

Usa ruido fresco solo en la primera estación.
En las estaciones siguientes, no usa ruido nuevo.
Consecuencia: Es como si la primera estación tuviera una armadura, pero las siguientes estuvieran desnudas. El espía puede ver cómo se acumula la información a medida que pasa por la línea. Por eso, ese diseño específico es inseguro, y ahora sabemos por qué matemáticamente.

5. ¿Por qué es importante esto? (El "Juez" Lean 4)

Antes, los ingenieros tenían que confiar en su intuición o en pruebas manuales que podían tener errores.

Este paper usa un juez matemático automático (Lean 4) que revisó cada paso de la lógica.
El juez dijo: "¡Cero errores! La matemática es perfecta".
Esto significa que los ingenieros pueden decir con total confianza a los reguladores (como los de FIPS): "No es solo nuestra palabra, tenemos una prueba matemática verificada por computadora de que nuestro diseño es seguro".

Resumen en una frase

Este paper es como un manual de instrucciones verificado por un juez infalible que dice: "Para que tu fábrica de llaves secretas sea segura, debes poner un nuevo ruido aleatorio en cada estación; si no lo haces (como hizo el diseño Adams), los espías podrán ver la llave, y ahora tenemos la prueba matemática de por qué".

Es un trabajo que cierra una brecha peligrosa entre la teoría y la práctica, asegurando que las futuras protecciones contra computadoras cuánticas sean realmente sólidas.

Título: Enmascaramiento Fresco Hace que las Pipelines de NTT sean Composibles: Pruebas Verificadas por Máquina para Enmascaramiento Aritmético en Hardware PQC

1. El Problema

Los aceleradores de criptografía post-cuantica (PQC) para ML-KEM (FIPS 203) y ML-DSA (FIPS 204) dependen de transformadas de número teórico (NTT) implementadas como pipelines de etapas de "mariposa" (butterflies) de Cooley-Tukey sobre el anillo $\mathbb{Z}_q$ .

La Brecha de Seguridad: Aunque existen marcos teóricos robustos para el enmascaramiento booleano (sobre $GF(2)$) como ISW, t-SNI, PINI y DOM, no existía ninguna respuesta verificada por máquina para el caso de enmascaramiento aritmético sobre $\mathbb{Z}_q$ en pipelines de NTT.
La Falacia de la Intuición: Los ingenieros de hardware a menudo asumen que si cada etapa individual es segura, la pipeline completa lo es. Sin embargo, no existía una prueba formal que confirmara esta composición para la estructura específica de la mariposa de NTT.
El "Trampa" de la Independencia de Valor: Existe una propiedad intuitiva pero falsa llamada "independencia de valor puntual" (pointwise value-independence). Si un diseñador verifica esta propiedad (que el valor de un cable no cambie si el secreto cambia manteniendo las máscaras fijas), obtendrá un resultado de "inseguro" para las mariposas de NTT, incluso si el diseño es correcto. Esto puede llevar a rechazar diseños válidos o, peor aún, a ignorar fallos reales en otros componentes.
Caso de Estudio Real: El acelerador Adams Bridge (parte de Caliptra de CHIPS Alliance) presenta una vulnerabilidad arquitectónica donde el enmascaramiento fresco solo se aplica en la ronda 0 de la INTT, dejando las etapas subsiguientes sin protección, lo que viola los principios de composición necesarios para la seguridad.

2. Metodología

Los autores utilizaron Lean 4 con la biblioteca Mathlib para formalizar y verificar matemáticamente las propiedades de seguridad.

Enfoque de Verificación Formal: Se desarrollaron nueve teoremas con cero "sorry" (sin partes no verificadas), cero "admit" y cero axiomas no verificados.
Modelo de Ataque: Se trabajó bajo el modelo de sondeo (probing model) de primer orden ISW, donde un adversario puede observar un solo cable por ciclo de reloj en toda la circuitos.
Abstracción Algebraica: Se demostró que la estructura de la mariposa de NTT es afín respecto a la máscara fresca (similar a la operación XOR en el enmascaramiento booleano). Esto permite una prueba directa de composición que evita la complejidad de los gadgets no lineales.
Herramientas: Se basaron en el trabajo previo de la herramienta QANARY (análisis de dependencias estructurales) y en fundamentos algebraicos universales establecidos en un artículo anterior (Paper 3).

3. Contribuciones Clave

El artículo presenta tres resultados principales verificados por máquina:

El Puente "r-bearing" (r-bearing bridge):
- Se cerró una limitación declarada en trabajos anteriores: se demostró formalmente que la "independencia de valor" implica una distribución marginal constante bajo la presencia de aleatoriedad fresca (fresh randomness).
- Se formalizó esto mediante un proxy algebraico llamado MutualInfoZero, conectando la independencia de valor con la independencia de información mutua ( $I(x; w) = 0$ ).
Uniformidad por Contexto de la Mariposa (Butterfly Per-Context Uniformity):
- Refutación de la propiedad falsa: Se probó que la "independencia de valor puntual" es falsa para las salidas de la mariposa (Teorema 5.1).
- Propiedad Correcta: Se definió y probó la Uniformidad Marginal. Para cualquier mariposa de Cooley-Tukey con una máscara de salida fresca en $\mathbb{Z}_q$ , cada cable de salida tiene exactamente un valor de máscara que produce cada posible valor de salida $v$ .
- Universalidad: Esta prueba es universal para todo $q > 0$ (incluyendo primos y compuestos), todos los factores de giro (twiddle factors) y todas las entradas.
Composición de Pipeline (Pipeline Composition):
- Se demostró que una pipeline de NTT de $k$ etapas, con enmascaramiento fresco por etapa, satisface la uniformidad por contexto en cada etapa bajo el modelo de sondeo de primer orden.
- Esto establece el Principio de Diseño de Enmascaramiento Fresco: si cada etapa inyecta una máscara fresca e independiente, la seguridad de la pipeline completa está garantizada algebraicamente.

4. Resultados

Pruebas Formales: Se compiló un artefacto con 1,738 trabajos de construcción, 0 errores y 0 advertencias.
Explicación de la Inseguridad de Adams Bridge: El análisis formal confirma que el acelerador Adams Bridge es estructuralmente inseguro porque viola la hipótesis del teorema de composición: no inyecta máscaras frescas entre las etapas (solo en la ronda 0). Al no cumplir con el "Principio de Enmascaramiento Fresco", la garantía de seguridad no se aplica, explicando las vulnerabilidades observadas empíricamente en trabajos anteriores.
Distinción de Complejidad: Se aclara que la composición para la mariposa (lineal/afín) es "fácil" y directa, a diferencia de los gadgets no lineales (como la reducción de Barrett o multiplicadores enmascarados), que requieren argumentos más complejos (tratados en trabajos futuros y complementarios).

5. Significado e Impacto

Para la Industria y Certificación: Proporciona a los ingenieros de hardware y a los evaluadores de FIPS (como en FIPS 140-3) una prueba verificada por máquina que pueden citar directamente en la documentación de certificación. Permite demostrar que una implementación de NTT es segura si sigue el principio de enmascaramiento fresco.
Prevención de Errores de Diseño: Al documentar explícitamente que la "independencia de valor puntual" es falsa, previene que los diseñadores descarten incorrectamente diseños seguros o ignoren fallos críticos en gadgets no lineales.
Fundamento para Futuros Trabajos: Establece la base algebraica para extender la verificación formal a gadgets no lineales (como la reducción de Barrett, que se aborda en el artículo complementario [3] con el marco PF-PINI) y a modelos de enmascaramiento de orden superior.
Universalidad: A diferencia de herramientas anteriores limitadas a $GF(2)$, esta prueba es válida para cualquier módulo $q$ , cubriendo tanto ML-KEM ( $q=3329$ ) como ML-DSA ( $q=8380417$ ) y futuras normas PQC.

En resumen, este trabajo cierra una brecha crítica en la verificación formal de hardware PQC, transformando la intuición de seguridad de las pipelines de NTT en una certeza matemática verificada, y exponiendo las causas arquitectónicas de las vulnerabilidades en implementaciones existentes como Adams Bridge.