ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security Verification
This work addresses the challenge of efficient and automated security verification for SoC designers, representing an incremental advance by applying existing methods like LLMs and formal verification to a specific domain.
The paper tackles the problem of automating security verification for System-on-Chip (SoC) designs by introducing ATLAS, an LLM-driven framework that bridges threat modeling and formal verification, resulting in detection of 39 out of 48 CWEs and correct property generation for 33 bugs on benchmark tests.
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.