LASP: LLM Assisted Security Property Generation for SoC Verification

As the complexity of System-on-Chips (SoCs) increases, ensuring their security presents escalating challenges. Formal property verification is one of the most robust methods to model and check security behaviors using model checkers. However, the generation of these security properties is a labor-intensive endeavor. Large language models (LLMs) have been applied in multiple fields due to their excellent ability to understand natural language. Hence, this paper presents a novel framework that utilizes LLMs to automate the generation of security properties directly from Register Transfer Level (RTL) designs. By extracting critical features and security assets from both the design specifications and RTL, the framework systematically produces tailored security properties for specific hardware designs. These properties are systematically cataloged in a security property database, providing an essential resource for ongoing and future hardware verification efforts. The effectiveness of this innovative framework is validated through its application to various open-source hardware designs, confirming its ability to significantly improve SoC security verification by efficiently generating robust security properties.