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

TL;DR

An LLM-driven framework that bridges standardized threat modeling and property-based formal verification for System-on-Chip (SoC) security, ATLAS automates the transformation from vulnerability reasoning to formal proof.

Abstract

This work presents ATLAS, an LLM-driven framework that bridges standardized threat modeling and property-based formal verification for System-on-Chip (SoC) security. Starting from vulnerability knowledge bases such as Common Weakness Enumeration (CWE), ATLAS identifies SoC-specific assets, maps relevant weaknesses, and generates assertion-based security properties and JasperGold scripts for verification. By combining asset-centric analysis with standardized threat model templates and multi-source SoC context, ATLAS automates the transformation from vulnerability reasoning to formal proof. Evaluated on three HACK@DAC benchmarks, ATLAS detected 39/48 CWEs and generated correct properties for 33 of those bugs, advancing automated, knowledge-driven SoC security verification toward a secure-by-design paradigm.

Figures (6)

• Figure 1: (a) Increasing hardware security vulnerabilities in RISC-V based SoCs. (b) Trend in CWE cwe_MITRE and CVE cve_MITRE over the years.
• Figure 2: LLM assisted threat model database generation in ATLAS.
• Figure 3: Asset-centric threat modeling from generic asset definitions (Table \ref{['tab:gen asset def']}) to SoC-specific asset detection, then CWE identification using the Threat Model Database (TMDB).
• Figure 4: Overview of AI-assisted security verification flow by ATLAS. (a) Asset-centric threat modeling, discussed in Sec. \ref{['sec:threat_modeling']}, using a generic asset definition, threat model database, and buggy SoC RTL code. The outcome of this step is SoC threat model of relevant CWEs. (b) Property-based security verification using SoC context (AST, RTL summary, and design document), threat model of the relevant CWEs.
• Figure 5: LLM–assisted security property generation. (a) The same prompt (buggy SoC RTL and Threat Model) is given to both methods. (b) Plain LLM: without context, LLM misreads the design intent and fails to derive the correct security property. (c) ATLAS: adding AST provides control and structural knowledge of the FSM behavior. (d) The design documents (DD) then highlight the trust boundaries and attack-surface. (e) RTL summary exposes the sensitive registers. Taken together, ATLAS is able to generate the correct property.