ATLAS：基于人工智能的威胁到断言学习用于片上系统安全验证
ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security Verification
AI总结：
ATLAS通过结合人工智能和形式验证技术，实现了基于漏洞知识的自动化SoC安全验证，提高了安全设计的可靠性。
摘要：
本文提出了ATLAS，一个由大型语言模型驱动的框架，旨在连接标准化的威胁建模与基于属性的正式验证，用于片上系统（SoC）安全。从漏洞知识库如常见弱点枚举（CWE）开始，ATLAS识别SoC特定的资产，映射相关弱点，并生成基于断言的安全属性和JasperGold脚本进行验证。通过结合以资产为中心的分析与标准化的威胁模型模板和多源SoC上下文，ATLAS自动化了从漏洞推理到正式证明的转换。在三个HACK@DAC基准测试中评估，ATLAS检测了48个CWE中的39个，并为其中33个错误生成了正确的属性，推动了自动化、知识驱动的SoC安全验证向安全设计范式发展。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
