Assertain: Automated Security Assertion Generation Using Large Language Models

Título: Assertain: Geração Automatizada de Asserções de Segurança Usando Modelos de Linguagem de Grande Porte (LLMs)

1. O Problema

A crescente complexidade dos designs de System-on-Chip (SoC) modernos amplifica os riscos de segurança de hardware, tornando a especificação manual de propriedades de segurança um gargalo crítico na verificação formal de propriedades (FPV).

• Limitações Atuais: A verificação baseada em asserções (ABV) depende fortemente da especificação manual de propriedades e asserções em SystemVerilog (SVAs). Esse processo é demorado, propenso a erros e tende a focar apenas em requisitos conhecidos, deixando vulnerabilidades arquitetônicas sutis e ameaças emergentes descobertas.
• Falhas das Abordagens Baseadas em LLMs: Embora os Modelos de Linguagem de Grande Porte (LLMs) tenham mostrado potencial na síntese de código, as abordagens existentes para geração de asserções de segurança sofrem com:
  • Falta de consciência explícita de ameaças.
  • Mapeamento não sistemático entre comportamentos de design e classes de vulnerabilidades padronizadas.
  • Alucinações (sinais inexistentes) e inconsistências contextuais que tornam as asserções não executáveis por ferramentas de verificação formal.

2. Metodologia

O Assertain é um framework automatizado que integra análise de design RTL, mapeamento para a Common Weakness Enumeration (CWE) e inteligência de modelos de ameaças para gerar automaticamente propriedades de segurança e SVAs executáveis. A arquitetura segue três fases principais:

• Fase I: Mapeamento de Conhecimento (Knowledge Mapping)

  • Alinhamento Estrutural ($M_{rtl}$): Um LLM classifica o design RTL de entrada em categorias de hardware pré-definidas (ex: "Componentes de Memória", "Interfaces de Comunicação"). Isso permite mapear o design para um conjunto relevante de CWEs usando uma base de conhecimento estática, evitando que o LLM "alucine" mapeamentos de vulnerabilidade.
  • Integração de Vetores de Ameaça ($M_{threat}$): Os vetores de ameaça definidos pelo usuário (ex: "Ataque de Canal Lateral", "Elevação de Privilégio") são normalizados e mapeados para identificadores CWE específicos.
  • Interseção de Contexto: O espaço de busca alvo ($C_{target}$) é definido pela interseção entre as fraquezas estruturalmente implícitas e as fraquezas derivadas das ameaças, garantindo que as propriedades geradas sejam estritamente relevantes para a superfície de ataque do hardware.

• Fase II: Geração Consciente de Contexto

  • Para cada fraqueza alvo, o sistema constrói um prompt complexo que inclui: contexto de papel (engenheiro de segurança), contexto de vulnerabilidade (definições e exemplos) e contexto de design completo (código RTL verbatim).
  • O LLM é instruído a gerar um triplo estruturado: Cenário de Segurança, Propriedade em Linguagem Natural e Código SVA candidato.
  • Geração Iterativa: O LLM é consultado múltiplas vezes ($N$ vezes) para cada fraqueza para maximizar a cobertura de cenários, com deduplicação automática dos resultados.
  • Restrições de Prompt: O prompt impõe regras estritas de sintaxe (ex: uso correto de operadores temporais |-> vs |=>, tratamento de reset, uso de sinais existentes) para garantir a validade sintática e semântica.

• Fase III: Refinamento por Auto-Reflexão

  • Esta fase crítica mitiga alucinações. O módulo de refinamento recebe as asserções candidatas brutas e o código RTL completo.
  • Verificação e Filtragem: O sistema verifica se todos os sinais referenciados na asserção existem no RTL. Sinais inexistentes ou macros não definidas são removidos.
  • Síntese: As asserções válidas restantes são emitidas como um módulo .sva compilável, limpo e documentado, pronto para verificação formal.

3. Contribuições Chave

• Framework Unificado: Primeira abordagem que unifica análise estrutural de RTL, mapeamento baseado em CWE e inteligência de modelos de ameaças para geração de asserções de segurança.
• Mecanismo de Auto-Reflexão: Introdução de uma etapa de refinamento que valida semanticamente as asserções contra o código fonte real, eliminando alucinações de sinais e garantindo compilabilidade.
• Geração de "Gap Analysis" Arquitetural: O framework não apenas verifica se o design corresponde à especificação funcional, mas gera propriedades que atuam como testes negativos para princípios de segurança. Se uma asserção falhar, isso indica uma lacuna de segurança arquitetural (ex: falta de proteção contra replay ou falha de tolerância a falhas), mesmo que o design funcione corretamente.
• Mapeamento Dinâmico de CWE: Uso sistemático de CWEs para garantir que as vulnerabilidades geradas estejam alinhadas com padrões industriais de segurança.

4. Resultados Experimentais

O framework foi avaliado em 11 designs de hardware representativos (incluindo MIPS, UART, MMU, módulos criptográficos e subsistemas SoC), comparando o Assertain (usando GPT-5 como motor base) com o uso direto do GPT-5 sem o framework.

• Desempenho Superior: O Assertain superou o baseline (GPT-5 puro) em:
  • 61,22% na geração de asserções corretas.
  • 59,49% na cobertura única de CWEs.
  • 67,92% na detecção de falhas arquitetônicas.
• Qualidade das Asserções: Em designs complexos (como Store_Unit e MMU), o Assertain dobrou a quantidade de asserções corretas em comparação ao baseline.
• Detecção de Falhas: O framework identificou significativamente mais falhas de arquitetura (ex: 15 falhas no design MIPS vs. 8 do baseline), demonstrando capacidade de encontrar vulnerabilidades sutis que a verificação funcional tradicional ignora.
• Casos de Uso: Exemplos práticos mostraram a detecção de riscos de Replay Attack em verificação de senhas, falhas de tolerância a falhas em Door_Lock e isolamento de papéis em controladores I2C.

5. Significado e Impacto

O trabalho do Assertain representa um avanço significativo na verificação de segurança de hardware:

• Escalabilidade: Transforma a verificação de segurança de um processo manual e limitado em um fluxo automatizado e escalável.
• Mudança de Paradigma: Move o foco da verificação de "o que o design faz" para "o que o design deveria fazer em termos de segurança", identificando lacunas entre o comportamento atual e os princípios de segurança ideais.
• Redução de Esforço: Reduz drasticamente o esforço manual necessário para especificar propriedades de segurança, permitindo que equipes de verificação se concentrem na análise de falhas críticas em vez da escrita de código de asserção.
• Robustez: A abordagem de auto-reflexão e validação contra o RTL real resolve o problema fundamental de alucinação em LLMs aplicado a contextos de engenharia de hardware rigorosos.

Em suma, o Assertain estabelece um novo padrão para a geração automatizada de asserções de segurança, demonstrando que a combinação de inteligência artificial com mapeamento de conhecimento estruturado (CWE) e validação rigorosa pode superar as limitações atuais da verificação formal de hardware.