LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation

• URL: http://arxiv.org/abs/2506.17865v1
• Date: Sun, 22 Jun 2025 01:21:03 GMT
• Title: LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation
• Authors: Dinesh Reddy Ankireddy, Sudipta Paria, Aritra Dasgupta, Sandip Ray, Swarup Bhunia,
• Abstract summary: Formal property verification (FPV) provides the capability to model and validate design behaviors.<n>Current practices require significant manual efforts to create such properties, making them time-consuming, costly, and error-prone.<n>This paper presents LASA, a novel framework that leverages LLMs and retrieval-augmented generation (RAG) to produce non-vacuous security properties.
• Score: 7.52190283487474
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Ensuring the security of modern System-on-Chip (SoC) designs poses significant challenges due to increasing complexity and distributed assets across the intellectual property (IP) blocks. Formal property verification (FPV) provides the capability to model and validate design behaviors through security properties with model checkers; however, current practices require significant manual efforts to create such properties, making them time-consuming, costly, and error-prone. The emergence of Large Language Models (LLMs) has showcased remarkable proficiency across diverse domains, including HDL code generation and verification tasks. Current LLM-based techniques often produce vacuous assertions and lack efficient prompt generation, comprehensive verification, and bug detection. This paper presents LASA, a novel framework that leverages LLMs and retrieval-augmented generation (RAG) to produce non-vacuous security properties and SystemVerilog Assertions (SVA) from design specifications and related documentation for bus-based SoC designs. LASA integrates commercial EDA tool for FPV to generate coverage metrics and iteratively refines prompts through a feedback loop to enhance coverage. The effectiveness of LASA is validated through various open-source SoC designs, demonstrating high coverage values with an average of ~88\%, denoting comprehensive verification through efficient generation of security properties and SVAs. LASA also demonstrates bug detection capabilities, identifying five unique bugs in the buggy OpenTitan SoC from Hack@DAC'24 competition.

Related papers

• CREDIT: Certified Ownership Verification of Deep Neural Networks Against Model Extraction Attacks [54.04030169323115]
  We introduce CREDIT, a certified ownership verification against Model Extraction Attacks (MEAs)<n>We quantify the similarity between DNN models, propose a practical verification threshold, and provide rigorous theoretical guarantees for ownership verification based on this threshold.<n>We extensively evaluate our approach on several mainstream datasets across different domains and tasks, achieving state-of-the-art performance.
  arXiv  Detail & Related papers  (2026-02-23T23:36:25Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• Multi-Agent Collaborative Intrusion Detection for Low-Altitude Economy IoT: An LLM-Enhanced Agentic AI Framework [60.72591149679355]
  The rapid expansion of low-altitude economy Internet of Things (LAE-IoT) networks has created unprecedented security challenges.<n>Traditional intrusion detection systems fail to tackle the unique characteristics of aerial IoT environments.<n>We introduce a large language model (LLM)-enabled agentic AI framework for enhancing intrusion detection in LAE-IoT networks.
  arXiv  Detail & Related papers  (2026-01-25T12:47:25Z)
• Feature-Space Adversarial Robustness Certification for Multimodal Large Language Models [59.6491828112519]
  Multimodal large language models (MLLMs) exhibit strong capabilities across diverse applications.<n> MLLMs are vulnerable to adversarial perturbations that distort their feature representations and induce erroneous predictions.<n>We propose Feature-space Smoothing (FS), a general framework that provides certified robustness guarantees at the feature representation level of MLLMs.
  arXiv  Detail & Related papers  (2026-01-22T18:52:21Z)
• LLMs in Code Vulnerability Analysis: A Proof of Concept [0.3441021278275805]
  Traditional software security analysis methods struggle to keep pace with the scale and complexity of moderns.<n>This paper explores the incorporation of code-specific and general-purpose Large Language Models to automate critical software security tasks.
  arXiv  Detail & Related papers  (2026-01-13T16:16:11Z)
• Automated Vulnerability Validation and Verification: A Large Language Model Approach [7.482522010482827]
  This paper introduces an end-to-end multi-step pipeline leveraging generative AI, specifically large language models (LLMs)<n>Our approach extracts information from CVE disclosures in the National Vulnerability Database.<n>It augments it with external public knowledge (e.g., threat advisories, code snippets) using Retrieval-Augmented Generation (RAG)<n>The pipeline iteratively refines generated artifacts, validates attack success with test cases, and supports complex multi-container setups.
  arXiv  Detail & Related papers  (2025-09-28T19:16:12Z)
• AttestLLM: Efficient Attestation Framework for Billion-scale On-device LLMs [19.00344718051438]
  We present AttestLLM, the first-of-its-kind attestation framework to protect the hardware-level intellectual property (IP) of device vendors.<n>We show that AttestLLM enforces model legitimacy and exhibits resilience against model forgery and attacks.
  arXiv  Detail & Related papers  (2025-09-08T04:17:02Z)
• White-Basilisk: A Hybrid Model for Code Vulnerability Detection [50.49233187721795]
  We introduce White-Basilisk, a novel approach to vulnerability detection that demonstrates superior performance.<n>White-Basilisk achieves results in vulnerability detection tasks with a parameter count of only 200M.<n>This research establishes new benchmarks in code security and provides empirical evidence that compact, efficiently designed models can outperform larger counterparts in specialized tasks.
  arXiv  Detail & Related papers  (2025-07-11T12:39:25Z)
• ZKPROV: A Zero-Knowledge Approach to Dataset Provenance for Large Language Models [46.71493672772134]
  We introduce ZKPROV, a novel cryptographic framework that enables zero-knowledge proofs of LLM provenance.<n>It allows users to verify that a model is trained on a reliable dataset without revealing sensitive information about it or its parameters.<n>Our method cryptographically binds a trained model to its authorized training dataset(s) through zero-knowledge proofs while avoiding proof of every training step.
  arXiv  Detail & Related papers  (2025-06-26T00:49:02Z)
• SV-LLM: An Agentic Approach for SoC Security Verification using Large Language Models [8.912091484067508]
  We introduce SV-LLM, a novel multi-agent assistant system designed to automate and enhance system-on-chip (SoC) security verification.<n>By integrating specialized agents for tasks like verification question answering, security asset identification, threat modeling, test plan and property generation, vulnerability detection, and simulation-based bug validation, SV-LLM streamlines the workflow.<n>The system aims to reduce manual intervention, improve accuracy, and accelerate security analysis, supporting proactive identification and mitigation of risks early in the design cycle.
  arXiv  Detail & Related papers  (2025-06-25T13:31:13Z)
• BugWhisperer: Fine-Tuning LLMs for SoC Hardware Vulnerability Detection [1.0816123715383426]
  This paper proposes a new framework named BugWhisperer to address the challenges of system-on-chips (SoCs) security verification.<n>We introduce an open-source, fine-tuned Large Language Model (LLM) specifically designed for detecting security vulnerabilities in SoCs.
  arXiv  Detail & Related papers  (2025-05-28T21:25:06Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• Breaking Focus: Contextual Distraction Curse in Large Language Models [68.4534308805202]
  We investigate a critical vulnerability in Large Language Models (LLMs)<n>This phenomenon arises when models fail to maintain consistent performance on questions modified with semantically coherent but irrelevant context.<n>We propose an efficient tree-based search methodology to automatically generate CDV examples.
  arXiv  Detail & Related papers  (2025-02-03T18:43:36Z)
• FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware [4.480157114854711]
  We present FVEval, the first comprehensive benchmark for characterizing large language models (LLMs) performance in tasks pertaining to formal verification (FV) The benchmark consists of three sub-tasks that measure LLM capabilities at different levels. We present both collections of expert-written verification collateral and methodologies to scalably generate synthetic examples aligned with FV.
  arXiv  Detail & Related papers  (2024-10-15T21:48:57Z)
• AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation [6.3585378855805725]
  We present a novel benchmark to evaluate Large-Language Models' effectiveness for assertion generation.<n>AssertioBench contains 100 curated Verilog hardware designs from OpenCores and formally verified assertions for each design generated from GoldMine and HARM.
  arXiv  Detail & Related papers  (2024-06-26T14:47:28Z)
• Detectors for Safe and Reliable LLMs: Implementations, Uses, and Limitations [76.19419888353586]
  Large language models (LLMs) are susceptible to a variety of risks, from non-faithful output to biased and toxic generations. We present our efforts to create and deploy a library of detectors: compact and easy-to-build classification models that provide labels for various harms.
  arXiv  Detail & Related papers  (2024-03-09T21:07:16Z)
• Online Safety Property Collection and Refinement for Safe Deep Reinforcement Learning in Mapless Navigation [79.89605349842569]
  We introduce the Collection and Refinement of Online Properties (CROP) framework to design properties at training time. CROP employs a cost signal to identify unsafe interactions and use them to shape safety properties. We evaluate our approach in several robotic mapless navigation tasks and demonstrate that the violation metric computed with CROP allows higher returns and lower violations over previous Safe DRL approaches.
  arXiv  Detail & Related papers  (2023-02-13T21:19:36Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.