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

TL;DR

ATLAS is an LLM-driven framework that automates the translation of threat models and vulnerabilities into formal assertions for System-on-Chip security verification, improving automation and accuracy.

Contribution

It introduces a novel approach combining threat modeling, vulnerability knowledge bases, and formal verification scripts for automated SoC security analysis.

Findings

Detected 39 out of 48 CWEs in benchmarks

Generated correct security properties for 33 vulnerabilities

Automated 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.