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

Resumo Técnico: ATLAS

1. O Problema

A verificação de segurança em Sistemas em Chip (SoCs) enfrenta desafios críticos devido à complexidade crescente, à integração de IPs de terceiros não confiáveis e à falta de regras padronizadas de segurança.

• Limitações Atuais: As abordagens de modelagem de ameaças tradicionais são manuais, propensas a erros e não conseguem acompanhar a evolução dos vetores de ataque. Métodos de verificação existentes (como verificação formal, análise de código e fuzzing) dependem de restrições de segurança criadas manualmente, o que é trabalhoso, não escalável e requer expertise profunda.
• Falta de Padronização: Embora existam bases de conhecimento robustas sobre vulnerabilidades (como CWE, CVE e CAPEC), elas não são sistematicamente utilizadas para fortalecer a segurança de SoCs durante o design.
• Geração de Propriedades: Trabalhos recentes que usam Grandes Modelos de Linguagem (LLMs) para gerar propriedades de segurança são ad hoc, cobrem apenas um subconjunto pequeno de vulnerabilidades e carecem de generalização.

2. Metodologia: O Framework ATLAS

O ATLAS é um framework unificado e impulsionado por LLMs que transforma conhecimento de vulnerabilidades em provas formais através de raciocínio contextual. O fluxo é dividido em duas etapas principais:

A. Modelagem de Ameaças Centrada em Ativos (Sec. 3)

• Padronização: O ATLAS introduz um template padronizado para modelagem de ameaças, definindo elementos como Adversários, Ativos, Superfícies de Ataque, Vulnerabilidades e Ameaças.
• Banco de Dados de Modelos de Ameaça (TMDB): Utilizando o CWE, CVE e CAPEC, o sistema gera um banco de dados estruturado de modelos de ameaças para cada CWE de hardware conhecido. Isso é feito com a ajuda de um LLM (GPT-5) e feedback humano, criando um conhecimento reutilizável.
• Detecção de Ativos Específicos do SoC: O sistema analisa o código RTL (Register Transfer Level) do SoC para identificar ativos críticos (ex: integridade de estado, dados sensíveis) baseando-se em definições genéricas e no TMDB.
• Mapeamento: O LLM mapeia os ativos detectados no RTL para os modelos de ameaça relevantes no TMDB, identificando quais CWEs são aplicáveis a aquele design específico.

B. Geração de Propriedades de Segurança e Verificação Formal (Sec. 4)

• Contexto Rico: Para gerar propriedades precisas (assertions), o ATLAS não usa apenas o RTL e o modelo de ameaça. Ele integra três fontes de contexto complementares:
  1. Documentos de Design (DD): Especificações, mapas de registradores e semântica de modos.
  2. Árvore de Sintaxe Abstrata (AST): Detalhes topológicos e estruturais do hardware (fluxo de controle, sinais, estados).
  3. Resumo RTL: Um resumo gerado pelo LLM focado em segurança, destacando ativos críticos e regras sem viés humano.
• Geração de SVA: O LLM utiliza esse contexto para gerar propriedades de segurança baseadas em assertivas (SystemVerilog Assertions - SVA) específicas para o design.
• Prova Formal: As propriedades são executadas na ferramenta JasperGold. Se uma propriedade falha, o gerador de contra-exemplo (counterexample) prova a vulnerabilidade; se passa, fornece uma prova formal de segurança.

3. Principais Contribuições

1. Primeira Padronização de Modelagem de Ameaças: Introdução de um template universal para modelagem de ameaças em hardware, preenchendo a lacuna entre conhecimento de vulnerabilidades e verificação prática.
2. Banco de Dados de Modelos de Ameaça (TMDB): Criação de um repositório estruturado e automatizado de modelos de ameaças derivados de CWEs, permitindo mapeamento consistente de ativos para fraquezas.
3. Abordagem "Threat-to-Assertion": Um fluxo completo que vai desde a identificação de ativos e mapeamento de ameaças até a geração automática de propriedades formais verificáveis.
4. Importância do Contexto: Demonstração empírica de que a combinação de AST, Documentos de Design e Resumo RTL é crucial para que o LLM entenda a intenção do design e evite gerar propriedades incorretas ou fora de escopo.

4. Resultados e Avaliação

O ATLAS foi avaliado em três benchmarks da competição HACK@DAC (2018, 2019, 2021), totalizando 48 bugs conhecidos em designs SoC baseados em RISC-V.

• Detecção de Vulnerabilidades: O ATLAS identificou 39 de 48 CWEs relevantes (81% de cobertura).
• Geração de Propriedades Corretas: Desses 39 casos detectados, o ATLAS gerou propriedades corretas para 33 bugs (>82% de precisão na geração de propriedades).
• Verificação Formal: O sistema conseguiu provar formalmente as violações ou a segurança dos módulos correspondentes.
• Estudo de Ablação:
  • Sem o TMDB, a taxa de detecção de CWEs caiu para menos de 30%.
  • Sem o contexto rico (AST, DD, Resumo), a geração de propriedades precisas caiu drasticamente (menos de 5 propriedades corretas em alguns casos), demonstrando que o LLM sozinho não consegue inferir a intenção de segurança sem esses dados estruturados.
• Comparação: O sistema superou abordagens manuais e anteriores baseadas em LLMs, oferecendo escalabilidade e consistência.

5. Significância e Impacto

O trabalho ATLAS representa um avanço significativo em direção ao paradigma de "Segurança por Design" (Secure-by-Design) para SoCs.

• Automação Escalável: Transforma a verificação de segurança de um processo manual e fragmentado em um fluxo automatizado e baseado em conhecimento.
• Redução de Custos: Ao identificar vulnerabilidades cedo no ciclo de design (antes da fabricação de silício), reduz drasticamente os custos de remediação pós-silício.
• Integração de IA e Formal: Demonstra como LLMs podem ser usados de forma robusta e confiável em engenharia de segurança crítica, desde que guiados por contextos estruturados e bases de conhecimento padronizadas.

Em suma, o ATLAS fecha a lacuna entre a teoria de vulnerabilidades (CWE) e a prática de verificação formal, permitindo que equipes de design de chips verifiquem a segurança de seus sistemas de forma mais rápida, abrangente e confiável.