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.

翻译：本工作提出ATLAS，一种基于大语言模型的框架，用于桥接标准化威胁建模与基于属性的形式化验证，以保障系统芯片（SoC）安全。ATLAS从通用弱点枚举（CWE）等漏洞知识库出发，识别SoC特定资产，映射相关弱点，并生成基于断言的属性和用于验证的JasperGold脚本。通过结合以资产为中心的分析、标准化威胁模型模板以及多源SoC上下文，ATLAS实现了从漏洞推理到形式化证明的自动化转换。在三个HACK@DAC基准测试上的评估表明，ATLAS检测到39/48个CWE，并为其中33个漏洞生成了正确的属性，推动了自动化、知识驱动的SoC安全验证向“安全设计”范式迈进。