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

1. Il Problema

La verifica della sicurezza dei Sistemi su Chip (SoC) affronta sfide critiche a causa della crescente complessità dei design, dell'uso di IP di terze parti potenzialmente non fidati e della mancanza di regole di sicurezza standardizzate.

• Limiti dei metodi attuali: Le approcci tradizionali di threat modeling (modellazione delle minacce) sono prevalentemente manuali, soggetti a errori e non scalabili di fronte all'espansione delle superfici di attacco.
• Gap conoscitivo: Sebbene esistano database di vulnerabilità ricchissimi (come CWE, CVE, CAPEC), questi sono spesso troppo astratti o frammentati per essere utilizzati direttamente nella verifica formale.
• Difficoltà nella generazione di proprietà: I metodi di verifica formale (come JasperGold) richiedono l'uso di asserzioni (SVA) scritte manualmente. La generazione automatica di queste asserzioni tramite LLM (Large Language Models) esistenti è spesso ad hoc, non generalizzabile e manca di contesto specifico sul design, portando a proprietà inaccurate o incomplete.

2. Metodologia: Il Framework ATLAS

ATLAS è un framework guidato da LLM che automatizza il flusso dalla conoscenza delle vulnerabilità alla prova formale, colmando il divario tra la modellazione delle minacce standardizzata e la verifica basata su proprietà. Il processo si articola in quattro fasi principali:

A. Creazione di un Database di Modelli di Minaccia (TMDB)

ATLAS costruisce un database strutturato (TMDB) che mappa le vulnerabilità note (CWE) a modelli di minaccia specifici.

• Utilizza un template standardizzato che include: Avversari (con diverse capacità), Asset da proteggere, Superfici di attacco, Vulnerabilità e Minacce.
• Sfrutta GPT-5 per generare modelli di minaccia per ogni CWE hardware, integrando dati da CVE e CAPEC, validati poi tramite feedback umano. Questo crea una base di conoscenza dinamica e riutilizzabile.

B. Rilevamento degli Asset Specifici dell'SoC

Il sistema analizza il codice RTL (Register Transfer Level) di un SoC per identificare gli asset critici.

• Utilizza definizioni generiche di asset (es. "Integrità del Runtime", "Dati Sensibili", "Risorse Privilegiate") e le confronta con il codice sorgente tramite LLM.
• Identifica segnali specifici, registri e moduli che corrispondono a queste definizioni, mappandoli ai modelli di minaccia rilevanti nel TMDB.

C. Modellazione delle Minacce Contestuale

Una volta identificati gli asset, ATLAS incrocia l'elenco degli asset con il TMDB per determinare quali CWE sono applicabili a quel design specifico.

• L'LLM esegue un mapping basato su parole chiave tra gli asset rilevati e i modelli di minaccia nel database, filtrando le vulnerabilità non pertinenti.

D. Generazione di Proprietà di Sicurezza e Verifica Formale

Questa è la fase cruciale per la verifica formale. Per generare asserzioni accurate, ATLAS non si basa solo sul codice RTL, ma integra tre fonti contestuali complementari:

1. Documenti di Design (DD): Specifiche architetturali, mappe dei registri e semantica delle modalità.
2. Abstract Syntax Tree (AST): Fornisce dettagli strutturali e topologici (flussi di controllo, connessioni, stati) per comprendere la logica interna.
3. Sintesi RTL (RTL Summary): Un riepilogo generato dall'LLM focalizzato sulla sicurezza, che evidenzia asset critici e regole di controllo senza bias umano.

Utilizzando questi contesti, ATLAS genera proprietà di sicurezza in SystemVerilog (SVA) specifiche per il design, che vengono poi verificate formalmente utilizzando lo strumento JasperGold. Se una proprietà fallisce, viene generato un controesempio che dimostra la vulnerabilità.

3. Contributi Chiave

• Primo approccio standardizzato: ATLAS è il primo tentativo di standardizzare il threat modeling per la sicurezza hardware utilizzando un template unificato e un database di conoscenza strutturato.
• Pipeline End-to-End: Automatizza l'intero flusso: dall'identificazione degli asset e mappatura delle vulnerabilità (CWE) fino alla generazione di script di verifica formale e asserzioni.
• Integrazione Contestuale Multi-sorgente: Dimostra che l'uso combinato di AST, documenti di design e sintesi RTL è fondamentale per guidare l'LLM a produrre asserzioni corrette, superando i limiti degli approcci basati solo sul codice.
• Scalabilità: Trasforma la conoscenza delle vulnerabilità (CWE) in prove formali scalabili, riducendo la dipendenza da esperti di dominio per la scrittura manuale di vincoli di sicurezza.

4. Risultati Sperimentali

Il framework è stato valutato su tre benchmark industriali su larga scala basati su RISC-V (HACK@DAC 2018, 2019, 2021), contenenti un totale di 48 bug noti.

• Rilevamento delle Vulnerabilità: ATLAS ha identificato correttamente 39 su 48 CWE rilevanti (81,25%).
• Generazione di Proprietà Corrette: Su i 39 CWE rilevati, ATLAS è riuscito a generare proprietà di sicurezza corrette per 33 casi (oltre l'82%), dimostrando la vulnerabilità tramite prove formali o controesempi.
• Studio di Ablazione:
  • Senza il TMDB, la capacità di rilevamento dell'LLM è crollata a meno del 30%.
  • L'uso esclusivo di un singolo contesto (es. solo RTL) ha portato a un numero basso di proprietà accurate.
  • L'aggiunta di tutti e tre i contesti (DD, AST, RTL Summary) ha migliorato la generazione di proprietà corrette di un fattore compreso tra 2,3x e 3x rispetto alle configurazioni parziali.
• Casi di Fallimento: I fallimenti sono stati attribuiti principalmente alla mancanza di specifiche funzionali esplicite nei documenti di design (es. comportamenti di reset o latch non documentati), che impediscono all'LLM di dedurre l'intento corretto.

5. Significato e Impatto

Il lavoro ATLAS rappresenta un passo significativo verso il paradigma "Secure-by-Design" per i SoC.

• Automazione della Sicurezza: Dimostra che è possibile automatizzare la trasformazione da ragionamento sulle vulnerabilità a prove formali, riducendo drasticamente i costi di remediation post-silicon.
• Scalabilità Industriale: Offre una soluzione scalabile per gestire la complessità crescente dei design moderni e la vasta gamma di potenziali vettori di attacco.
• Fondamento per il Futuro: Stabilisce una metodologia che integra database di vulnerabilità standardizzati con tecniche di verifica formale assistita dall'IA, ponendo le basi per futuri strumenti di sicurezza hardware più robusti e autonomi.

In sintesi, ATLAS trasforma la verifica della sicurezza da un processo manuale e frammentato in un flusso di lavoro automatizzato, guidato dai dati e basato su prove formali, aumentando la resilienza dei sistemi critici.