ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security Verification

Resumen Técnico: ATLAS

1. El Problema

La verificación de seguridad en Sistemas en Chip (SoC) enfrenta desafíos críticos debido a la creciente complejidad de los diseños, la integración de IP de terceros no confiable y la falta de reglas estandarizadas de seguridad.

• Limitaciones de los métodos actuales: Los enfoques tradicionales de modelado de amenazas son manuales, propensos a errores y no escalan ante la complejidad de los diseños modernos.
• Falta de automatización: Las técnicas de verificación formal, análisis de código y fuzzing dependen en gran medida de restricciones o reglas de seguridad creadas manualmente por expertos, lo que es laborioso y difícil de mantener.
• Brecha de conocimiento: Aunque existen bases de datos de vulnerabilidades masivas (como CWE, CVE y CAPEC), los métodos actuales no logran utilizar sistemáticamente este conocimiento para mapear amenazas específicas de un SoC hacia pruebas formales verificables.
• Ineficacia de las LLMs existentes: Los esfuerzos recientes para usar Modelos de Lenguaje Grande (LLM) para generar propiedades de seguridad son ad hoc, cubren solo un subconjunto pequeño de vulnerabilidades y carecen de generalización.

2. Metodología: El Marco ATLAS

ATLAS es un marco unificado impulsado por LLMs que transforma el conocimiento de vulnerabilidades en pruebas formales mediante razonamiento contextual. El flujo de trabajo se divide en cuatro etapas principales:

A. Generación de Base de Datos de Modelos de Amenazas (TMDB)

• ATLAS construye una base de datos estructurada de modelos de amenazas para cada CWE (Common Weakness Enumeration) de hardware conocido.
• Utiliza una plantilla estandarizada que define: Adversarios (capacidades y acceso), Activos (lo que debe protegerse), Superficies de Ataque, Vulnerabilidades y Amenazas.
• Se utiliza un LLM (GPT-5) asistido por retroalimentación humana para generar estos modelos a partir de CWE, CVE y CAPEC, creando un repositorio de conocimiento evolutivo y reutilizable.

B. Detección de Activos Específicos del SoC

• El sistema analiza el código RTL (Register Transfer Level) de un SoC específico.
• Utilizando definiciones genéricas de activos (ej. integridad de estado, datos sensibles, recursos privilegiados) y la TMDB, el LLM identifica qué activos críticos están presentes en el diseño y mapea qué CWEs son relevantes para ellos.

C. Modelado de Amenazas Centrado en Activos

• Una vez identificados los activos, ATLAS cruza la lista de activos con la TMDB para filtrar y seleccionar los modelos de amenazas específicos que aplican a ese diseño.
• Esto permite pasar de una lista genérica de debilidades a un conjunto de amenazas concretas para el SoC bajo prueba.

D. Generación de Propiedades de Seguridad y Verificación Formal

• Contexto Riqueza: Para generar propiedades de aserción precisas (SystemVerilog Assertions - SVA), ATLAS no se basa solo en el RTL. Integra tres fuentes de contexto:
  1. Documentos de Diseño (DD): Especificaciones, mapas de registros y semántica de modos.
  2. Árbol de Sintaxis Abstracta (AST): Detalles topológicos y estructurales del hardware (flujos de control, señales, estados).
  3. Resumen de RTL: Un resumen generado por LLM centrado en seguridad que destaca activos críticos y reglas de guardia.
• Generación de Propiedades: El LLM utiliza este contexto para traducir los modelos de amenazas en propiedades formales concretas.
• Verificación: Las propiedades se ejecutan en la herramienta formal JasperGold. Si se encuentra una violación, se genera una traza de contraejemplo; si se prueba, se garantiza la seguridad bajo las suposiciones dadas.

3. Contribuciones Clave

• Primera estandarización de modelado de amenazas: ATLAS introduce una plantilla estandarizada para modelar amenazas de hardware, abordando la falta de consistencia en los enfoques manuales.
• Base de datos de conocimiento (TMDB): Crea un repositorio estructurado que conecta CWEs, CVEs y CAPECs con modelos de amenazas específicos, permitiendo un mapeo automatizado y escalable.
• Enfoque "Asset-Centric": Cambia el paradigma de buscar vulnerabilidades genéricas a identificar activos específicos en el RTL y luego determinar qué amenazas los afectan.
• Integración de Contexto Multifuente: Demuestra que la combinación de AST, documentos de diseño y resúmenes de RTL es crucial para que las LLMs generen propiedades de seguridad correctas y no "alucinadas".
• Automatización de extremo a extremo: Conecta el razonamiento de vulnerabilidades con la prueba formal, reduciendo la intervención humana.

4. Resultados y Evaluación

El marco ATLAS fue evaluado en tres conjuntos de pruebas de la competencia HACK@DAC (ediciones 2018, 2019 y 2021), que incluyen diseños de SoC basados en RISC-V con vulnerabilidades conocidas.

• Detección de Vulnerabilidades: ATLAS identificó 39 de 48 CWEs relevantes en los benchmarks.
• Generación de Propiedades Correctas: De las vulnerabilidades detectadas, ATLAS generó propiedades de seguridad correctas para 33 casos (>82%), logrando pruebas formales exitosas o contraejemplos válidos.
• Estudio de Ablación:
  • Sin la TMDB, la tasa de detección de CWEs por parte del LLM cayó a menos del 30%.
  • Sin los contextos adicionales (AST, DD, Resumen), la capacidad de generar propiedades precisas disminuyó drásticamente (menos de 5 propiedades correctas en comparación con el rendimiento completo de ATLAS).
• Comparación: El sistema superó a los enfoques manuales y basados en LLMs anteriores, demostrando una mejora significativa en la escalabilidad y la precisión.

5. Significado e Impacto

• Paradigma "Secure-by-Design": ATLAS avanza hacia un modelo donde la seguridad se verifica formalmente desde las etapas tempranas del diseño, en lugar de depender de parches posteriores al silicio.
• Escalabilidad: Al automatizar la traducción de conocimiento de vulnerabilidades (CWE) a pruebas formales, el marco hace viable la verificación de seguridad para SoCs complejos donde los métodos manuales son inviables.
• Reducción de Costos: Al identificar y mitigar amenazas antes de la fabricación, se reducen los costos exorbitantes asociados con la corrección de vulnerabilidades de seguridad en hardware.
• Reutilización de Conocimiento: La TMDB permite que el conocimiento de vulnerabilidades pasadas se aplique sistemáticamente a nuevos diseños, creando un ciclo de mejora continua en la seguridad del hardware.

En conclusión, ATLAS representa un avance significativo en la automatización de la verificación de seguridad de hardware, demostrando que la combinación de bases de conocimiento estandarizadas, LLMs y verificación formal puede cerrar la brecha entre la teoría de amenazas y la garantía práctica de seguridad en los SoCs.