💻 computer science

Controller Datapath Aware Verification of Masked Hardware Generated via High Level Synthesis

Este trabajo presenta la herramienta de verificación formal MaskedHLSVerif, diseñada para validar la seguridad contra ataques de canal lateral de potencia en hardware enmascarado generado mediante Síntesis de Alto Nivel, superando las falsas alarmas de herramientas existentes al abordar específicamente las arquitecturas de controlador y ruta de datos compartidas resultantes de las optimizaciones del HLS.

Autores originales: Nilotpola Sarma, Vaishali Ghanshyam Chaudhuri, Chandan Karfa

Publicado 2026-03-20

📖 4 min de lectura☕ Lectura para el café

CC BY 4.0

Autores originales: Nilotpola Sarma, Vaishali Ghanshyam Chaudhuri, Chandan Karfa

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

🛡️ El Guardián de los Secretos: Cómo verificar que los "candados" digitales no se rompan al construirse

Imagina que tienes un secreto muy valioso (como una contraseña bancaria) que necesitas proteger en una caja fuerte. Para hacerlo, decides no guardar el secreto entero, sino partirlo en pedazos (llamados "compartimentos" o shares) y repartirlos entre varios guardias. Ningún guardia por sí solo puede saber el secreto; solo cuando se juntan todos los pedazos se revela la información. A esto los expertos le llaman "enmascaramiento" (masking).

El problema es que los ladrones (hackers) no solo intentan abrir la caja, sino que escuchan el sonido que hace la caja al cerrarse (consumo de energía) para adivinar qué hay dentro. Si los pedazos del secreto se mezclan o se escuchan juntos, el ladrón puede ganar.

🏗️ El Problema: El Constructor Automático (HLS)

Antiguamente, los ingenieros construían estas cajas fuertes a mano, ladrillo a ladrillo. Era lento y propenso a errores.
Hoy en día, usamos un constructor automático (llamado High-Level Synthesis o HLS) que toma un plano escrito en un lenguaje simple (como C) y construye automáticamente el circuito electrónico (el hardware) en segundos.

Pero aquí está el truco:
Este constructor automático es muy rápido y eficiente. Su objetivo es ahorrar espacio y tiempo. Para lograrlo, a veces reutiliza las mismas herramientas para hacer diferentes tareas en momentos distintos.

Analogía: Imagina un chef que tiene solo un cuchillo. Corta la cebolla, luego guarda el cuchillo, luego lo saca para cortar la zanahoria. Funciona, pero si el chef se distrae y usa el cuchillo para cortar la cebolla y la zanahoria al mismo tiempo (o en un orden raro), la ensalada se arruina.

En el mundo de la seguridad, este "chef" a veces reorganiza las tareas de forma que, aunque el circuito funcione bien (la ensalada se come), los pedazos del secreto se mezclan accidentalmente, creando una grieta por donde los ladrones pueden espiar.

🔍 El Problema de los Detectores Antiguos

Existen inspectores de seguridad (herramientas de verificación) que revisan si la caja fuerte está bien construida. Sin embargo, estos inspectores son un poco paranoicos y torpes.

La analogía: Imagina que el inspector revisa el cuchillo del chef y dice: "¡Peligro! Este cuchillo podría teóricamente cortar la cebolla y la zanahoria al mismo tiempo, ¡así que la caja es insegura!".
La realidad: En la caja real, el chef (el controlador) nunca deja que eso pase. Pero el inspector no entiende el "ritmo" o los "estados" del chef. Por eso, falsamente acusa a las cajas bien construidas de ser inseguras. Esto se llama un "falso positivo".

💡 La Solución: MaskedHLSVerif (El Inspector Inteligente)

Los autores de este paper crearon una nueva herramienta llamada MaskedHLSVerif. En lugar de mirar todo el circuito de golpe y asumir lo peor, esta herramienta actúa como un director de escena que observa paso a paso.

Divide y vencerás: En lugar de ver todo el circuito, la herramienta divide el trabajo en "escenas" (estados).
Observa el momento exacto: En la "Escena 1", solo se usa el cuchillo para la cebolla. En la "Escena 2", solo para la zanahoria.
Verifica la lógica: La herramienta pregunta: "¿En esta escena específica, es posible que los pedazos del secreto se mezclen?".
- Si la respuesta es "No, porque el director de escena (el FSM) controla el flujo", entonces está seguro.
- Si la respuesta es "Sí, porque el constructor automático reorganizó las cosas mal", entonces detecta el error.

🧪 Los Resultados: ¿Funciona?

Los autores probaron su herramienta con varios diseños de seguridad (como el cifrado PRESENT y multiplicadores enmascarados).

Los inspectores viejos (como REBECCA): Dijeron que casi todo estaba roto (falsos positivos), porque no entendían que el circuito solo hace una cosa a la vez.
La nueva herramienta (MaskedHLSVerif): Dijo "Está bien" cuando realmente estaba bien, y "¡Alerta!" cuando el constructor automático había cometido un error real al reorganizar las tareas.

Además, lograron atrapar un error real que el constructor automático había cometido al intentar ser demasiado eficiente (una "reagrupación" de tareas que rompió la seguridad).

🎯 En resumen

Este paper nos dice: "No confíes ciegamente en los constructores automáticos de circuitos seguros, y no confíes ciegamente en los inspectores viejos que se asustan con todo."

Han creado un nuevo tipo de inspector que entiende el ritmo y la secuencia de cómo se construye el circuito. Así, puede decirte con certeza si tu caja fuerte digital es realmente segura o si tiene una grieta invisible que solo aparece cuando el constructor automático intenta ahorrar espacio.

La moraleja: Para proteger tus secretos digitales en el futuro, necesitas herramientas que entiendan no solo qué se construye, sino cuándo y cómo se construye.

Título: Verificación Consciente del Controlador y la Ruta de Datos de Hardware Enmascarado Generado mediante Síntesis de Alto Nivel (HLS)

1. El Problema

La implementación de hardware para algoritmos criptográficos es vulnerable a los Ataques de Canal Lateral de Potencia (PSCA). Una contramedida común es el enmascaramiento (masking), que divide la información secreta en "partes" (shares) aleatorias. Sin embargo, diseñar hardware enmascarado manualmente es costoso y propenso a errores.

Para mitigar esto, se utiliza la Síntesis de Alto Nivel (HLS), que convierte especificaciones de software enmascarado en hardware RTL (Register-Transfer Level) automáticamente. El problema central identificado en este trabajo es que:

Las herramientas HLS no fueron diseñadas pensando en la seguridad. Sus optimizaciones (como el balanceo de expresiones, la reasociación y el uso compartido de recursos) pueden introducir vulnerabilidades de seguridad o alterar la lógica de enmascaramiento.
Las herramientas de verificación formal existentes (como REBECCA) asumen que todas las rutas de datos sintácticamente posibles pueden estar activas simultáneamente.
En diseños generados por HLS, el hardware utiliza un Controlador (FSM) y una Ruta de Datos compartida (multiplexada en el tiempo). Esto significa que ciertas combinaciones de entradas en los multiplexores (MUX) nunca ocurren en la práctica.
Las herramientas actuales, al no considerar el estado del FSM, verifican combinaciones de entrada inalcanzables, generando falsos positivos (reportan fugas de seguridad donde no las hay) y, por tanto, una estimación de seguridad inexacta.

2. Metodología: MaskedHLSVerif

Los autores proponen un flujo de trabajo de verificación llamado MaskedHLSVerif, que adapta las herramientas de verificación existentes para manejar la arquitectura específica de los diseños generados por HLS.

La metodología se basa en la verificación estado por estado del FSM:

Análisis del FSM: Se extrae el Controlador (Finite State Machine) del diseño RTL generado por HLS.
Descomposición en Diseños por Estado: En lugar de verificar el diseño completo de una sola vez, el flujo divide el diseño RTL en sub-diseños ( $D_x$ $D_{x}$ ), uno para cada estado del FSM.
- Para cada estado $x$ , se extrae la porción activa de la ruta de datos.
- Se incluyen recursivamente todas las operaciones de estados anteriores de las cuales depende el estado actual.
- Se generan archivos de etiquetas (labels) específicos para cada sub-diseño, asegurando que las entradas intermedias se etiqueten correctamente como "shares", "máscaras" o "públicas" basándose en las entradas originales.
Verificación Formal: Cada sub-diseño ( $D_x$ $D_{x}$ ) se verifica individualmente utilizando la herramienta REBECCA.
- Al restringir la verificación solo a las combinaciones de entrada válidas y alcanzables en un estado específico, se eliminan las combinaciones inalcanzables que causaban los falsos positivos.
- Se verifica bajo los modelos de sondeo estático (S) y transitorio (T) para cubrir fugas por glitches.
Integridad Global: Si todos los sub-diseños de cada estado pasan la verificación, se concluye que el diseño RTL completo es seguro.

3. Contribuciones Clave

Identificación de Limitaciones: Demostraron que las herramientas de verificación de vanguardia (SOTA) fallan al verificar hardware enmascarado generado por HLS debido a la arquitectura de ruta de datos compartida controlada por FSM, produciendo falsos positivos.
Análisis de Impacto de HLS: Discutieron cómo las optimizaciones de HLS (re-asociación, balanceo de expresiones, asignación de recursos) pueden romper la seguridad del enmascaramiento, incluso manteniendo la corrección funcional.
Nueva Metodología de Verificación: Desarrollaron MaskedHLSVerif, un flujo que utiliza la estructura del FSM para abstraer la ruta de datos activa en cada estado, permitiendo una verificación precisa sin falsos positivos.
Validación Experimental: Validaron el método en seis benchmarks criptográficos, incluyendo multiplicadores enmascarados en cascada (DOM, HPC1, HPC2, COMAR) y la S-box del cifrado PRESENT.

4. Resultados

Eliminación de Falsos Positivos: En Experimento 1, aplicaron el flujo a seis diseños generados por Vitis HLS. La herramienta REBECCA estándar reportó falsos positivos (inseguridad) en todos los casos debido a las combinaciones inalcanzables. En contraste, MaskedHLSVerif verificó correctamente que todos los diseños eran seguros.
Validación Física (TVLA): Se confirmó la seguridad de los diseños RTL mediante pruebas de TVLA (Test Vector Leakage Assessment) en silicona simulada, mostrando que los diseños generados por HLS eran efectivamente seguros y que los fallos reportados por REBECCA eran errores de la herramienta.
Detección de Flaws Reales: En Experimento 2, forzaron una optimización de "reasociación" en el código C de entrada. MaskedHLSVerif detectó correctamente una vulnerabilidad de enmascaramiento de primer orden introducida por esta optimización en el segundo estado del diseño, mientras que REBECCA seguía fallando por falsos positivos o no podía distinguir el error real del ruido de las combinaciones inalcanzables.
Métricas: El flujo mostró tiempos de ejecución razonables y escalabilidad, manejando diseños con múltiples estados (de 2 a 4 estados) y diferentes esquemas de enmascaramiento.

5. Significancia

Este trabajo es pionero al abordar específicamente la verificación de seguridad de hardware enmascarado generado automáticamente mediante HLS.

Confianza en la Automatización: Permite a los diseñadores utilizar HLS para generar hardware enmascarado con confianza, sabiendo que pueden verificar la seguridad sin ser engañados por las limitaciones de las herramientas actuales.
Seguridad Robusta: Proporciona un método para detectar no solo errores de diseño, sino también vulnerabilidades introducidas inadvertidamente por las optimizaciones del compilador HLS.
Avance en el Campo: Establece un nuevo estándar para la verificación formal de diseños con arquitecturas de controlador y ruta de datos compartida, llenando un vacío crítico en la seguridad de hardware criptográfico moderno.