Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators

Título: Análisis de Dependencia Estructural para Hardware de NTT Enmascarado: Verificación Pre-Silicio Escalable de Aceleradores de Criptografía Post-Cuántica

1. El Problema

La finalización de los estándares de criptografía post-cuántica (PQC) basados en retículos, como ML-KEM (FIPS 203) y ML-DSA (FIPS 204), ha intensificado la necesidad de aceleradores de hardware resistentes a canales laterales. El enmascaramiento (masking) es la contramedida dominante, pero verificar su seguridad a escala industrial presenta desafíos críticos:

• Escalabilidad: Las herramientas de verificación exacta (como SILVER, Prover, Coco-Alma) suelen limitarse a gadgets de unos pocos miles de celdas (generalmente <5,000), lo que es insuficiente para diseños de hardware completos que superan el millón de celdas.
• Complejidad del Enmascaramiento Aritmético: Los aceleradores PQC utilizan enmascaramiento aritmético (suma modular) en lugar de booleano (XOR) para operaciones como la Transformada Numérica Teórica (NTT) y la reducción modular. Esto, combinado con pipelines profundos, crea dependencias de múltiples ciclos que las herramientas de análisis de un solo ciclo no detectan.
• Brecha de Verificación: Existe una falta de herramientas que puedan realizar una verificación exhaustiva pre-silicio en diseños de producción masivos, obligando a los ingenieros a depender de revisiones manuales o pruebas de trazas de potencia que pueden pasar por alto fugas raras.

2. Metodología: QANARY y la Jerarquía de Verificación

Los autores presentan QANARY, una herramienta de verificación de dependencia estructural diseñada para hardware de gran escala. El núcleo de la metodología es una jerarquía de verificación de cuatro etapas que equilibra la escalabilidad con la precisión:

1. Análisis de Dependencia Estructural (D0/D1):

   • Realiza un análisis de un solo ciclo (SC-D1) y una extensión de múltiples ciclos (MC-D1).
   • Utiliza un retículo de etiquetas $\{⊥, S_0, S_1, BOTH\}$ para rastrear la propagación de las "comparticiones" (shares) de los secretos a través de la red lógica.
   • MC-D1: Extiende el análisis a través de los límites de los registros (DFF) mediante propagación de etiquetas de punto fijo. Esto detecta convergencias de shares que ocurren después de varios ciclos de reloj, invisibles para el análisis combinacional simple.
   • Garantía: Es una condición necesaria pero no suficiente (sin falsos negativos, pero con falsos positivos).

2. Refinamiento de Enmascaramiento Fresco (FM):

   • Verifica si las señales marcadas como inseguras están protegidas por un bit de aleatoriedad fresca que actúa como un "one-time pad" (bijection). Promueve algunas señales a "seguras" si se cumple esta condición.

3. Verificación de Distancia de Autenticación Booleana (Boolean SADC):

   • Aplica una comprobación de independencia de valores para enmascaramiento booleano. Reparametriza las shares en términos del secreto y la máscara para verificar si el valor de la señal depende del secreto.

4. Verificación de Distancia de Autenticación Aritmética (Arithmetic SADC):

   • Innovación Clave: Extiende el SADC al dominio aritmético (módulo $q$). Utiliza una reparametrización simbólica donde $S_0 = (X - S_1) \mod q$.
   • Utiliza solucionadores SMT (Z3 y CVC5) para verificar la independencia de valores. Si la señal es independiente del secreto para cualquier asignación de máscara y aleatoriedad, se marca como segura.
   • Esta etapa convierte las advertencias estructurales en certificaciones matemáticas o las reduce a un conjunto manejable de candidatos inseguros.

3. Contribuciones Clave

1. Verificación a Escala de Producción: Aplicación exitosa del análisis de dependencia estructural a un acelerador de 1.17 millones de celdas (Adams Bridge), completando el análisis de 30 módulos en segundos.
2. Extensión Multi-Ciclo (MC-D1): Demostración de que el análisis de un solo ciclo es insuficiente. MC-D1 reclasificó 12 módulos de "limpios" a "marcados" al detectar dependencias cruzadas entre registros.
3. Jerarquía con SADC Aritmético: Primera integración de una verificación de independencia de valores aritmética en una tubería de verificación estructural a escala industrial. En el módulo de reducción Barrett (5,543 celdas), la herramienta verificó automáticamente el 54.5% de las señales marcadas como seguras.
4. Validación Dual y Reproducibilidad: Cada veredicto aritmético se cruzó con dos solucionadores independientes (Z3 y CVC5), logrando un acuerdo del 100% (0 desacuerdos en 363 señales). Se proporciona un artefacto completo con pruebas formales y scripts de reproducción.

4. Resultados

El estudio se centró en Adams Bridge, un acelerador de hardware de código abierto para ML-KEM y ML-DSA.

• Rendimiento General:

  • El análisis estructural (SC-D1) identificó 59,061 señales inseguras en 8.7 segundos.
  • La extensión multi-ciclo (MC-D1) aumentó este número a 614,126 señales, revelando que 12 módulos previamente considerados seguros eran vulnerables debido a dependencias cruzadas de registros.
  • Se identificaron 8,487 puntos de convergencia reales (raíces de la vulnerabilidad) entre los 1.17 millones de celdas, reduciendo el esfuerzo de triaje en un 98.6%.

• Caso de Estudio: Módulo de Reducción Barrett (ML-KEM):

  • Entrada: 363 señales marcadas como inseguras por el análisis estructural.
  • Proceso:
    • FM: 0 promovidas.
    • SADC Booleano: 146 confirmadas como inseguras, 217 indeterminadas.
    • SADC Aritmético: Resolvió el resto.
  • Resultado Final:
    • 198 señales (54.5%) verificadas como seguras (certificados matemáticos).
    • 165 señales marcadas como candidatas inseguras (límite superior sonoro para revisión manual).
    • 0 indeterminadas.
  • Tiempo: Aproximadamente 3 minutos en un solo núcleo.

• Comparación con Herramientas Existentes:

  • Herramientas exactas (Coco-Alma) no pudieron escalar al módulo completo de Barrett (5,543 celdas) debido a limitaciones de memoria, mientras que QANARY lo procesó exitosamente.
  • En un submódulo de prueba (333 celdas), hubo desacuerdos con Coco-Alma debido a definiciones diferentes de "fuga" (estado estable vs. transitorio/glitch), pero QANARY confirmó su veredicto de seguridad mediante tres métodos independientes.

5. Significado e Impacto

• Cierre de la Brecha Pre-Silicio: La herramienta permite generar evidencia de seguridad de canales laterales antes de la fabricación del chip, algo crítico para la certificación FIPS 140-3 de hardware PQC.
• Reducción de Carga de Trabajo: Convierte cientos de alertas estructurales en un conjunto pequeño y accionable (165 candidatos) con certificados matemáticos para el 54.5% restante, eliminando la necesidad de revisar manualmente señales que son estructuralmente inseguras pero matemáticamente seguras.
• Validación de Compromisos de Diseño: Proporciona una base objetiva para que los diseñadores evalúen si las vulnerabilidades estructurales identificadas son explotables o si son compensadas por otras medidas (como el enmascaramiento parcial o la aleatorización de ejecución).
• Nuevos Estándares de Verificación: Establece que la verificación estructural escalable, seguida de refinamiento algebraico, es viable para diseños de millones de celdas, superando las limitaciones de las herramientas de verificación exacta tradicionales.

En resumen, el papel demuestra que es posible escalar la verificación de enmascaramiento a hardware de producción post-cuántico mediante una combinación de análisis estructural rápido y verificación algebraica precisa, ofreciendo un flujo de trabajo práctico para la industria de seguridad de hardware.