論文の概要: LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation

• arxiv url: http://arxiv.org/abs/2506.17865v1
• Date: Sun, 22 Jun 2025 01:21:03 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-24 19:06:36.622806
• Title: LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation
• Title（参考訳）: LASA: LLM支援プロパティ生成によるSoCセキュリティ検証の強化
• Authors: Dinesh Reddy Ankireddy, Sudipta Paria, Aritra Dasgupta, Sandip Ray, Swarup Bhunia,
• Abstract要約: 形式的プロパティ検証(FPV)は、設計の振る舞いをモデル化し、検証する機能を提供する。 現在のプラクティスでは、そのようなプロパティを作成するためにかなりの手作業が必要で、時間がかかり、コストがかかり、エラーが発生します。 本稿では,LLMと検索拡張生成(RAG)を活用して非空きセキュリティ特性を創出する新しいフレームワークであるLASAを提案する。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: 現代のSystem-on-Chip (SoC) 設計のセキュリティを確保することは、知的財産権 (IP) ブロックをまたいだ複雑さと分散資産の増加により、大きな課題となる。 形式的プロパティ検証(FPV)は、モデルチェッカーを使用してセキュリティプロパティを通じて設計動作をモデル化し、検証する機能を提供するが、現在のプラクティスでは、そのようなプロパティを作成するためにかなりの手作業が必要であるため、時間がかかり、コストがかかり、エラーが発生しやすい。 LLM(Large Language Models)の出現は、HDLコード生成や検証タスクなど、さまざまな領域で顕著な熟練を見せている。 現在のLLMベースの技術は、しばしば空白なアサーションを生成し、効率的なプロンプト生成、包括的な検証、バグ検出を欠いている。 本稿では,LLMと検索拡張生成(RAG)を利用して非空きセキュリティ特性を生成する新しいフレームワークであるLASAと,設計仕様とバスベースのSoC設計に関するドキュメントからSystemVerilog Assertions(SVA)を提案する。 LASAは、FPV用の商用EDAツールを統合して、カバレッジメトリクスを生成し、フィードバックループを通じてプロンプトを反復的に洗練し、カバレッジを強化する。 LASAの有効性は、様々なオープンソースSoC設計を通じて検証され、セキュリティ特性とSVAの効率的な生成による包括的な検証を、平均 88 % の高カバレッジ値で示す。 LASAはまた、Hack@DAC'24コンペティションから5つのユニークなバグを識別するバグ検出機能をデモしている。

関連論文リスト

• BugWhisperer: Fine-Tuning LLMs for SoC Hardware Vulnerability Detection [1.0816123715383426]
  本稿では,システムオンチップ(SoC)セキュリティ検証の課題を解決するために,BugWhispererという新しいフレームワークを提案する。 我々は、SoCのセキュリティ脆弱性を検出するために特別に設計された、オープンソースで微調整されたLarge Language Model (LLM)を紹介する。
  論文  参考訳（メタデータ） (2025-05-28T21:25:06Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• Breaking Focus: Contextual Distraction Curse in Large Language Models [68.4534308805202]
  大規模言語モデル(LLM)の重大な脆弱性について検討する。 この現象は、セマンティック・コヒーレントだが無関係な文脈で修正された質問に対して、モデルが一貫した性能を維持することができないときに発生する。 本稿では,CDVの例を自動生成する効率的な木探索手法を提案する。
  論文  参考訳（メタデータ） (2025-02-03T18:43:36Z)
• FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware [4.480157114854711]
  FVEvalは,形式的検証(FV)に関わるタスクにおいて,大規模言語モデル(LLM)のパフォーマンスを特徴付ける最初の総合ベンチマークである。 ベンチマークは3つのサブタスクで構成され、異なるレベルでLLM能力を測定する。 本稿では,FVに整合した合成例を生成するための,専門家による検証手法と手法のコレクションについて述べる。
  論文  参考訳（メタデータ） (2024-10-15T21:48:57Z)
• AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation [6.3585378855805725]
  本稿では,アサーション生成におけるLarge-Language Modelsの有効性を評価するための新しいベンチマークを提案する。 AssertioBenchにはOpenCoresから100のキュレートされたVerilogハードウェア設計が含まれており、GoldMineとHARMから生成された各設計について正式に承認されている。
  論文  参考訳（メタデータ） (2024-06-26T14:47:28Z)
• Detectors for Safe and Reliable LLMs: Implementations, Uses, and Limitations [76.19419888353586]
  大規模言語モデル(LLM)は、不誠実なアウトプットからバイアスや有害な世代に至るまで、さまざまなリスクを受けやすい。 我々は,様々な害のラベルを提供するコンパクトで容易に構築できる分類モデルである,検出器のライブラリを作成し,展開する取り組みについて述べる。
  論文  参考訳（メタデータ） (2024-03-09T21:07:16Z)
• Online Safety Property Collection and Refinement for Safe Deep Reinforcement Learning in Mapless Navigation [79.89605349842569]
  オンラインプロパティのコレクション・リファインメント(CROP)フレームワークをトレーニング時にプロパティを設計するために導入する。 CROPは、安全でない相互作用を識別し、安全特性を形成するためにコストシグナルを使用する。 本手法をいくつかのロボットマップレスナビゲーションタスクで評価し,CROPで計算した違反量によって,従来のSafe DRL手法よりも高いリターンと低いリターンが得られることを示す。
  論文  参考訳（メタデータ） (2023-02-13T21:19:36Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。