From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification

Título: De la Enumeración Finita a la Prueba Universal: Fundamentos Teórico-Anillares para la Verificación de Enmascaramiento en Hardware PQC

1. El Problema

La verificación formal del enmascaramiento (masking) en hardware de criptografía post-cuántica (PQC), específicamente en aceleradores que implementan los estándares NIST ML-KEM (FIPS 203) y ML-DSA (FIPS 204), enfrenta una limitación crítica en los enfoques actuales.

• Limitación de los Solvers SMT: Herramientas anteriores como QANARY (presentadas en trabajos previos de los autores) dependían de solvers SMT (Z3, CVC5) para verificar la independencia de valores en funciones de cable (wire functions). Sin embargo, estos solvers operan mediante enumeración exhaustiva en dominios finitos.
• La Brecha de Escala: En trabajos previos, la corrección del Teorema 3.9.1 (que garantiza que la independencia de valores implica distribución marginal constante) se verificó solo para un módulo pequeño ($q=5$), enumerando 225 funciones booleanas.
• Inviabilidad de Generalización: Este enfoque no es escalable ni estructuralmente válido para los módulos reales utilizados en PQC: $q=3,329$ (ML-KEM) y $q=8,380,417$ (ML-DSA). La enumeración en estos dominios es computacionalmente imposible ($2^{q^2}$ combinaciones) y los solvers SMT no pueden realizar inducción estructural sobre $q$. Esto dejaba una brecha de seguridad: no había garantía formal de que las propiedades verificadas en $q=5$ se mantuvieran en los parámetros de producción.

2. Metodología

Los autores proponen un cambio de paradigma desde la lógica de vectores de bits (bit-vector SAT) hacia la teoría de anillos conmutativos utilizando Lean 4 y su biblioteca matemática Mathlib.

• Abstracción Algebraica: En lugar de modelar el hardware como circuitos booleanos con desbordamientos explícitos, se modela la aritmética modular directamente sobre el anillo de cociente $\mathbb{Z}/q\mathbb{Z}$ (tipo ZMod q en Lean).
• Prueba Interactiva (ITP): Se utiliza Lean 4 para construir pruebas formales verificadas por el núcleo (kernel) del lenguaje. Esto reduce la "base de confianza" (trusted base) de complejos solvers SMT (con cientos de miles de líneas de código no verificadas) al pequeño núcleo de Lean 4.
• Enfoque "Sorry-Free": Todas las pruebas se completan sin estubs no verificados (sorry), garantizando que cada paso lógico ha sido validado formalmente.
• Reparametrización: El núcleo de la metodología es demostrar que la reparametrización del enmascaramiento aritmético ($s_0 = x - s_1$) es una identidad de anillo, no un procedimiento computacional sujeto a errores de desbordamiento.

3. Contribuciones Clave

El artículo presenta la primera prueba formal verificada por máquina que es universal (válida para cualquier $q > 0$) para el sub-teorema libre de $r$ del Teorema 3.9.1. Las contribuciones específicas incluyen:

1. Prueba Universal de 5 Líneas (Teorema 4.1):

   • Se demuestra que para cualquier módulo $q > 0$, cualquier función de cable $w$, y cualquier par de secretos, si la función es independiente del valor del secreto, entonces sus distribuciones marginales son idénticas.
   • Esta prueba, que requiere solo 5 líneas de script en Lean 4, reemplaza la necesidad de verificar 225 casos (o billones en $q$ grandes) mediante enumeración.
   • La prueba se basa únicamente en los axiomas de anillo conmutativo (sub_add_cancel), demostrando que la propiedad es estructural y no dependiente de la representación binaria.

2. Suite de Pruebas de Soporte (9 Teoremas):

   • T1 y T1': Generalización a tipos de salida arbitrarios.
   • T2 y T3: Pruebas de "round-trip" (ida y vuelta) para reparametrización booleana (XOR) y aritmética (resta modular), demostrando que son bijecciones.
   • T4: Límites de no-desbordamiento que conectan la teoría de anillos con la implementación de vectores de bits en hardware.
   • T5: Caracterización del sesgo de los generadores de números aleatorios (RNG) y límites universales para ML-KEM.
   • T6: Un contraejemplo universal que demuestra que la implicación inversa (distribución constante $\implies$ independencia de valor) es falsa para todo $q \ge 2$, validando la naturaleza conservadora de las herramientas de análisis.

3. Cambio Metodológico:

   • Establece que la teoría de anillos es la capa de abstracción natural para la verificación de enmascaramiento aritmético, superando las limitaciones de los enfoques basados en SAT.

4. Resultados

• Verificación Completa: La suite de pruebas consta de 1,739 tareas de compilación en Lean 4, todas completadas con 0 errores y 0 sorry.
• Cobertura Universal: La corrección de la herramienta QANARY ahora está garantizada para todos los conjuntos de parámetros NIST PQC (presentes y futuros), incluyendo ML-KEM ($q=3,329$) y ML-DSA ($q=8,380,417$), sin necesidad de re-verificación.
• Eficiencia: Se logró reducir una verificación que requería millones de evaluaciones booleanas a una demostración algebraica concisa.
• Validación de Conservadurismo: Se demostró formalmente que las advertencias de "INSECURE_CONSERVATIVE" generadas por QANARY en análisis previos no son artefactos de implementación, sino una consecuencia matemática inevitable de la brecha entre independencia de valores y distribución constante.

5. Significado e Impacto

• Certificación FIPS 140-3: Elimina la necesidad de re-verificar cada conjunto de parámetros para la certificación de módulos criptográficos. Una sola prueba verificada por el núcleo cubre todos los casos de uso.
• Portabilidad de Diseño: Las actualizaciones de parámetros o la adopción de nuevos esquemas basados en retículos no invalidan la garantía de seguridad, ya que la prueba es universal sobre $q$.
• Confianza en la Herramienta: Cambia el modelo de confianza de "confiar en solvers SMT complejos" a "confiar en el núcleo formalmente especificado de Lean 4", elevando el nivel de garantía para aplicaciones de alta seguridad.
• Fundamentos Teóricos: Sugiere que otras propiedades complejas del enmascaramiento (enmascaramiento de orden superior, conversiones booleano-aritméticas) podrían admitir pruebas igualmente concisas si se formulan en el contexto algebraico adecuado.

En resumen, este trabajo cierra la brecha metodológica entre la verificación práctica a pequeña escala y la garantía de seguridad formal universal para el hardware de criptografía post-cuántica, demostrando que la estructura algebraica subyacente es suficiente para probar la seguridad sin depender de la enumeración exhaustiva.