Assertain: Automated Security Assertion Generation Using Large Language Models

Resumen Técnico: Assertain

1. El Problema

La creciente complejidad de los diseños modernos de Sistemas en Chip (SoC) ha amplificado los riesgos de seguridad en el hardware. La verificación de propiedades formales (FPV), una técnica rigurosa para validar el comportamiento de seguridad, depende tradicionalmente de la especificación manual de propiedades y aserciones en SystemVerilog (SVA). Este proceso manual presenta varios cuellos de botella críticos:

• Escalabilidad: Es difícil de escalar con diseños cada vez más complejos.
• Dependencia de expertos: Requiere un conocimiento profundo del dominio y del diseño específico.
• Sesgo y omisiones: Tiende a verificar solo requisitos conocidos o anticipados, dejando vulnerabilidades arquitectónicas sutiles y emergentes sin detectar.
• Limitaciones de los LLM actuales: Los enfoques anteriores basados en Modelos de Lenguaje Grande (LLM) para generar aserciones carecen de conciencia de amenazas explícita, no mapean sistemáticamente los comportamientos del diseño a clases de vulnerabilidades estandarizadas (CWE) y sufren de "alucinaciones" (generación de señales inexistentes o sintaxis inválida), lo que resulta en aserciones no ejecutables.

2. Metodología

Assertain es un marco de trabajo automatizado que integra el análisis de diseño RTL, el mapeo a la enumeración de debilidades comunes (CWE) y la inteligencia de modelos de amenazas. Su objetivo es traducir intenciones de alto nivel y artefactos de diseño en aserciones formales rigurosas. La arquitectura consta de tres fases principales:

• Fase I: Mapeo de Conocimiento (Knowledge Mapping)

  • Alineación Estructural ($M_{rtl}$): Un LLM clasifica el diseño de entrada (RTL) en categorías predefinidas (ej. "Componentes de Memoria", "Interfaces de Comunicación") y mapea estas categorías a un conjunto de identificadores CWE relevantes utilizando una base de conocimientos estática, evitando que el LLM alucine mapeos directos.
  • Integración de Vectores de Amenaza ($M_{threat}$): Los modelos de amenazas proporcionados por el usuario (ej. "Ataque de Canal Lateral", "Escalada de Privilegios") se normalizan y se mapean a identificadores CWE específicos.
  • Intersección de Contexto: Se define un espacio de búsqueda objetivo ($C_{target}$) como la intersección entre las debilidades estructurales y las derivadas de las amenazas. Esto asegura que las propiedades generadas sean estrictamente relevantes para la superficie de ataque real del hardware.

• Fase II: Generación Consciente del Contexto

  • Se utiliza un LLM para generar propiedades basadas en un prompt híbrido que incluye: contexto de rol (ingeniero de seguridad), contexto de vulnerabilidad (definición CWE) y el código fuente RTL completo inyectado verbatim.
  • Generación Iterativa: Para maximizar la cobertura, el LLM se consulta $N$ veces para cada debilidad objetivo. Los resultados se agregan, se eliminan duplicados y se estructuran en tablas Markdown (CWE ID, Escenario, Propiedad en Lenguaje Natural, Código SVA).
  • Restricciones de Prompt: Se imponen reglas estrictas de sintaxis (uso correcto de operadores temporales |-> vs |=>, manejo de reset, evitar aserciones triviales) y de integridad de señales (solo usar señales existentes en el RTL).

• Fase III: Refinamiento por Auto-Reflexión

  • Para mitigar las alucinaciones, un módulo de refinamiento recibe las aserciones candidatas crudas y el código RTL completo.
  • Verificación y Filtrado: El módulo verifica que todas las señales referenciadas existan en el diseño real. Elimina cualquier aserción que contenga identificadores no definidos.
  • Síntesis: Genera un módulo .sva limpio, compilable y autónomo, con comentarios estructurados y mensajes de error significativos.

3. Contribuciones Clave

• Marco Unificado: Primera solución que integra el análisis estructural RTL, el mapeo CWE y la inteligencia de modelos de amenazas en un flujo automatizado de generación de aserciones de seguridad.
• Mecanismo de Auto-Reflexión: Introduce una etapa de refinamiento crítica que valida semánticamente las aserciones contra el diseño real, resolviendo el problema de las alucinaciones de señales y la sintaxis inválida.
• Enfoque de "Arquitecto de Seguridad": A diferencia de la verificación funcional tradicional que busca coincidencia con la especificación, Assertain genera propiedades que actúan como "pruebas negativas". Si una aserción falla, no indica un bug funcional, sino una brecha arquitectónica de seguridad (falta de protección).
• Cobertura Ampliada: Logra una cobertura de vulnerabilidades mucho más amplia al identificar debilidades que los flujos manuales o los LLMs estándar pasan por alto.

4. Resultados

El marco fue evaluado en 11 diseños de hardware representativos (incluyendo módulos como AES, UART, MMU, MIPS y JTAG) y comparado contra un modelo base (GPT-5).

• Rendimiento Superior: Assertain superó a GPT-5 en:
  • 61.22% en la generación de aserciones correctas.
  • 59.49% en la cobertura única de CWE.
  • 67.92% en la detección de fallos arquitectónicos.
• Cobertura de CWE: En diseños complejos como MIPS y Store_Unit, Assertain identificó hasta el doble de clases de vulnerabilidades únicas (CWE) que el modelo base.
• Detección de Fallos Arquitectónicos: El sistema detectó significativamente más problemas de alto nivel. Por ejemplo, en el diseño MIPS, detectó 15 fallos frente a los 8 del modelo base.
• Casos de Éxito:
  • Identificó la falta de rotación de desafíos en un módulo de verificación de contraseñas (riesgo de ataque de repetición).
  • Detectó la falta de tolerancia a fallos en un mecanismo de bloqueo (riesgo de bloqueo en estados ilegales).
  • Identificó la falta de aislamiento de roles en un controlador I2C (riesgo de "Confused Deputy").
  • Señaló la ausencia de filtros contra glitches en líneas de control.

5. Significado e Impacto

El trabajo Assertain representa un avance significativo en la verificación de seguridad de hardware al:

1. Automatizar la creación de especificaciones de seguridad: Reduce drásticamente el esfuerzo manual y el tiempo de verificación.
2. Elevar el nivel de abstracción de la verificación: Pasa de verificar "¿funciona el diseño?" a "¿es seguro el diseño bajo modelos de amenaza reales?".
3. Mitigar el riesgo de alucinación en IA: Demuestra que, con un flujo de trabajo de refinamiento basado en el contexto real del diseño, los LLM pueden generar código de verificación formal fiable y ejecutable.
4. Cierre de la brecha de seguridad: Proporciona una metodología para descubrir vulnerabilidades arquitectónicas sutiles que escapan a las verificaciones funcionales tradicionales, mejorando la postura de seguridad de los SoC modernos antes de la fabricación.

En conclusión, Assertain establece un nuevo estándar para la integración de la Inteligencia Artificial en el flujo de diseño de hardware seguro, transformando la generación de aserciones de una tarea manual propensa a errores en un proceso sistemático, exhaustivo y consciente de las amenazas.