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.
@article{arxiv.2603.01170,
title = {ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security Verification},
author = {Ishraq Tashdid and Kimia Tasnia and Alexander Garcia and Jonathan Valamehr and Sazadur Rahman},
journal= {arXiv preprint arXiv:2603.01170},
year = {2026}
}
Comments
Accepted at the 63rd Design Automation Conference (DAC 2026), Long Beach, CA, USA (July, 2026)