用大模型自动把漏洞知识转为芯片安全验证代码
ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security Verification
- 基于大模型分析漏洞库，识别芯片资产与弱点
- 在三个基准上检测出48个漏洞中的39个，生成33个正确验证属性
- 适合芯片安全验证工程师快速构建自动化验证流程
本文提出ATLAS，一个由大语言模型驱动的框架，连接标准化威胁建模与基于属性的形式化验证，用于片上系统（SoC）安全。从通用弱点枚举（CWE）等漏洞知识库出发，ATLAS识别SoC特定资产，映射相关弱点，并生成基于断言的安全属性及JasperGold验证脚本。结合资产中心分析、标准威胁模板和多源SoC上下文，实现从漏洞推理到形式证明的自动化转换。在三个HACK@DAC基准上评估，ATLAS成功检测出48个CWE中的39个，并为其中33个漏洞生成了正确的验证属性，推动了面向安全设计的自动化、知识驱动的SoC安全验证。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。