LASA：利用 LLM 辅助属性生成增强 SoC 安全验证
密码学与安全
2025-06-24 v1 新兴技术
摘要
由于复杂性的增加和知识产权（IP）模块间分布式资产的存在，确保现代片上系统设计的安全性面临重大挑战。形式化属性验证（FPV）提供了通过安全属性与模型检测器对设计行为进行建模和验证的能力；然而，当前的做法需要大量人工来创建此类属性，这使其耗时、昂贵且容易出错。大型语言模型的出现展示了其在包括 HDL 代码生成和验证任务在内的各个领域的卓越能力。当前基于 LLM 的技术通常产生空洞的断言，并且缺乏高效的提示生成、全面验证和错误检测能力。本文提出了 LASA，一种利用 LLM 和检索增强生成（RAG）的框架，旨在根据设计规范和相关文档，为基于总线的 SoC 设计生成非空洞的安全属性和 SystemVerilog 断言（SVA）。LASA 集成了商用 EDA 工具用于 FPV 以生成覆盖率指标，并通过反馈循环迭代优化提示以提升覆盖率。LASA 的有效性通过各种开源 SoC 设计得到了验证，展示了约 88% 的平均高覆盖率，这表明通过高效生成安全属性和 SVA 实现了全面验证。LASA 还展示了错误检测能力，在 Hack@DAC'24 竞赛存在缺陷的 OpenTitan SoC 中识别出了五个独特的错误。
引用
@article{arxiv.2506.17865,
title = {LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation},
author = {Dinesh Reddy Ankireddy and Sudipta Paria and Aritra Dasgupta and Sandip Ray and Swarup Bhunia},
journal= {arXiv preprint arXiv:2506.17865},
year = {2025}
}
备注
9 pages, 5 figures, 5 tables