cs.CRMar 1, 2026

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

Authors: Ishraq Tashdid, Kimia Tasnia, Alexander Garcia, Jonathan Valamehr, Sazadur Rahman

Organizations: Department of Electrical and Computer Engineering, University of Central Florida · Intel Corporation

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

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 & tables

Figure 1. (a) Increasing hardware security vulnerabilities in RISC-V based SoCs. (b) Trend in CWE ( Software and CWEs, ) and CVE ( Common Vulnerabilities and Exposures, ) over the years.
TemplateCWE-1245 Threat Model
AdversarySimple Hardware Adversary
AssetsHardware State and Logic Integrity
Attack surfaceHardware Interfaces and State Machine Logic
VulnerabilitiesImproper or insecure FSM design
ThreatsExploiting undefined or insecure FSM transitions
Table 1. Threat model template and example.
Adversary ModelCapabilities
Unprivileged SoftwareLimited capability to run user-code
System SoftwareAdmin/root access to system software
Startup code/SMM 1Can tamper the boot or SMM 1 code
NetworkCan communicate with confidential services
Software Side ChannelCan monitor/extract confidential metadata
Simple HardwarePhysical access w/o expensive equipment/training
Table 2. Adversary models in ATLAS with different capabilities.
Figure 2. LLM assisted threat model database generation in ATLAS .
Figure 3. Asset-centric threat modeling from generic asset definitions (Table 3 ) to SoC-specific asset detection, then CWE identification using the Threat Model Database (TMDB).
Asset TypeDefinitionKeywords
Sensitive DataConfidential information. IP, firmware, or personal data.keys_, pass_, secret_* protected_, user_
Boot IntegrityVerifies and loads boot. Establishes hardware root of trust.boot_, hash_, rom_* otp_, key_
Attestation Data & Measurement ReportsSigned measurements of states. Stored in dedicated registers.pcr_, measurement_ idev_*
Parametric DataDevice-specific non-volatile values. Used for identity and calibration.otp_, trim_, nvm_cfg_* uid_, device_id_, serial_*
Privileged System ResourcesPrivileged control registers. Accessible in trusted modes.debug_* , *_mode _level
Shared ResourcesShared buses or memories. Arbitration to prevent leakage.ready_, valid_, dma_* req_, grant_, crossbar_*
Table 3. Generic assets definition for SoC specific assets detection.
Figure 4. Overview of AI-assisted security verification flow by ATLAS . (a) Asset-centric threat modeling, discussed in Sec. 3 , 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.
HACK@DAC18 ( HACK-EVENT, 2019a )HACK@DAC19 ( HACK-EVENT, 2019b )HACK@DAC21 ( HACK-EVENT, 2021 )
ModuleBugsDetected CWEsProp.FVModuleBugsDetected CWEsProp.FVModuleBugsDetected CWEsProp.FV
adbg_tapLogic bug Checks 31/32 bits Pwd not reset Reset broken1221 , 1191, 1271 1298 , 1221, 1191 1329 , 1271, 276 1419 , 1271, 1191✓ ✓ ✓ ×\times✓ ✓ ✓ ×\timescsr_regfileDebug exit issue Read/Write access Incorrect M-mode Incorrect update1244 , 1191, 1243 1262 , 1220, 269 1262 , 1220, 269 1256 , 200, 203×\times ✓ ✓ ✓×\times ✓ ✓ ✓dmi_jtagPass flag reset Write w/o pass Hardcoded key Unreachable state1239 , 1271, 1191 1245 , 1191, 1244 1329 , 321, 798 1245 , 1191, 1221×\times ✓ ✓ ✓×\times ✓ ✓ ✓
mux_funcWrong mux Out uncleared1240 , 1245, 1221 325 , 226, 1271✓ ✓✓ ✓commit_stageInterrupt ×2\times 2 Commit1281 , 1262, 1220 1281 , 1241, 1271×\times ×\times×\times ×\timescsr_regfileDebug open Privilege leak1220 , 1191, 1243 1262 , 1220, 269✓ ✓✓ ✓
riscv_cs_regWrong privilege1207 , 1262, 269✓✓axi_nodeImproper bypass1220 , 1191, 269×\times×\timesaes_192Counter stuck1240 , 323, 330✓✓
apb_gpioLock writable Reset clears lock1207 , 1220, 276 1206 , 276, 1271×\times ✓×\times ✓arianeNo flush after atomic No flush after priv1281 , 1206, 1271 1281 , 1191, 1241✓ ✓✓ ✓reglk_wrapp.Locks disabled Locks dropped1232 , 1221, 276 1234 , 1232, 1221×\times ×\times×\times ×\times
axi_address_dec.Errors ignored20 , 703, 388×\times×\timescontrollerHalt w/o exception1207 , 1419, 1271✓×\timessha256_wrapp.Input uncleared1239 , 226, 1271×\times×\times
Table 4. Security verification by ATLAS across three HACK@DAC ( Hardware security challenge contest, ) benchmarks by detecting relevant CWE threat models, generating corresponding assertion based security properties, and performing verification by JasperGold.
Figure 6. TMDB ablation across HACK@DAC’18, ’19, and ’21. (a) Number of correct CWEs identified by an LLM without TMDB versus ATLAS with TMDB. (b) Context ablation on accurate properties.
More in this topic

Cybersecurity

Cybersecurity develops methods to protect digital and cyber-physical systems from attacks, vulnerabilities, data loss, and misuse.

See all 354 papers

Explore similar work

CardsList

  1. HardSecBench: Benchmarking the Security Awareness of LLMs for Hardware Code Generation

    Jan 20, 2026Qirui Chen, Jingxian Shuai, Shuangwu Chen +8LLM SecuritySecure Code Generation

    University of Science and Technology of China, China · Xi’an Jiaotong University, China · Nanjing University, China +1

  2. AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications

    May 26, 2026Yuchao Wu, Wenji Fang, Jing Wang +3Formal Hardware VerificationLLM Evaluation

    Hong Kong University of Science and Technology (HKUST)

  3. SMSI: System Model Security Inference: Automated Threat Modeling for Cyber-Physical Systems

    Apr 26, 2026RoÝah Radaideh, Ali KhreisCyber-Physical SystemsCybersecurity

    School of Electrical Engineering and Computer Science, University of Ottawa, Ottawa, ON, Canada