論文の概要: HIVE: Scalable Hardware-Firmware Co-Verification using Scenario-based Decomposition and Automated Hint Extraction

• arxiv url: http://arxiv.org/abs/2309.08002v2
• Date: Wed, 17 Apr 2024 00:39:42 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-04-18 19:40:10.953617
• Title: HIVE: Scalable Hardware-Firmware Co-Verification using Scenario-based Decomposition and Automated Hint Extraction
• Title（参考訳）: HIVE:シナリオベースの分解と自動ヒント抽出によるスケーラブルハードウェアファームウェアの共検証
• Authors: Aruna Jayasena, Prabhat Mishra,
• Abstract要約: ハードウェア確認ソフトの共検証は、信頼できるシステムの設計に不可欠である。 ハードウェアを手動で抽象化したり、ヒントを手動で生成することで、ファームウェア検証中の状態空間を削減できる有望な方法がある。 本稿では,シミュレーションに基づく検証のスケーラビリティと形式検証の完全性とを効果的に組み合わせる。
• 参考スコア（独自算出の注目度）: 2.977255700811213
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Hardware-firmware co-verification is critical to design trustworthy systems. While formal methods can provide verification guarantees, due to the complexity of firmware and hardware, it can lead to state space explosion. There are promising avenues to reduce the state space during firmware verification through manual abstraction of hardware or manual generation of hints. Manual development of abstraction or hints requires domain expertise and can be time-consuming and error-prone, leading to incorrect proofs or inaccurate results. In this paper, we effectively combine the scalability of simulation-based validation and the completeness of formal verification. Our proposed approach is applicable to actual firmware and hardware implementations without requiring any manual intervention during formal model generation or hint extraction. To reduce the state space complexity, we utilize both static module-level analysis and dynamic execution of verification scenarios to automatically generate system-level hints. These hints guide the underlying solver to perform scalable equivalence checking using proofs. The extracted hints are validated against the implementation before using them in the proofs. Experimental evaluation on RISC-V based systems demonstrates that our proposed framework is scalable due to scenario-based decomposition and automated hint extraction. Moreover, our fully automated framework can identify complex bugs in actual firmware-hardware implementations.
• Abstract（参考訳）: ハードウェア確認ソフトの共検証は、信頼できるシステムの設計に不可欠である。 形式的手法は検証の保証を提供するが、ファームウェアとハードウェアの複雑さのため、状態空間の爆発につながる可能性がある。 ハードウェアを手動で抽象化したり、ヒントを手動で生成することで、ファームウェア検証中の状態空間を削減できる有望な方法がある。 抽象化やヒントを手作業で開発するにはドメインの専門知識が必要で、時間がかかりエラーが発生しやすいため、誤った証明や不正確な結果につながる可能性がある。 本稿では,シミュレーションに基づく検証のスケーラビリティと形式検証の完全性とを効果的に組み合わせる。 提案手法は,正式なモデル生成やヒント抽出において手作業による介入を必要とせず,実際のファームウェアやハードウェアの実装に適用可能である。 状態空間の複雑さを低減するため,静的モジュールレベルの解析と検証シナリオの動的実行の両方を用いてシステムレベルのヒントを自動的に生成する。 これらのヒントは、証明を用いてスケーラブルな等価チェックを実行するために、基礎となる解法を導く。 抽出されたヒントは、証明に使用する前に実装に対して検証される。 RISC-Vに基づくシステムにおいて,シナリオベースの分解と自動ヒント抽出により,提案手法がスケーラブルであることを示す。 さらに、我々の完全に自動化されたフレームワークは、実際のファームウェア・ハードウエア実装における複雑なバグを特定することができる。

関連論文リスト

• Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
  シリコングレードの正しさは、 (i) シミュレーション中心の評価の限られたカバレッジと信頼性、 (ii) 回帰と修復幻覚、 (iii) エージェントハンドオフ間で意図が再解釈される意味的ドリフトによってボトルネックが残っている。 エージェントの意図を整合させる設計契約を確立するマルチエージェントフレームワークであるVeri-Sureを提案する。
  論文  参考訳（メタデータ） (2026-01-27T16:10:23Z)
• Overcoming Joint Intractability with Lossless Hierarchical Speculative Decoding [58.92526489742584]
  我々は無益な無益な提案をする。 承認されたトークンの数を大幅に増加させる検証方法。 HSDは様々なモデルファミリやベンチマークの受け入れ率に一貫した改善をもたらすことを示す。
  論文  参考訳（メタデータ） (2026-01-09T11:10:29Z)
• Propose, Solve, Verify: Self-Play Through Formal Verification [75.44204610186587]
  形式的検証が信頼性の高い正当性信号を提供する検証コード生成設定における自己再生について検討する。 本稿では,PSV(Propose, Solve, Verify)という,難易度の高い合成問題を生成可能なプロジェクタと,専門家の反復によって訓練された解決器を作成するための,形式的検証信号を用いた簡単なセルフプレイフレームワークを紹介する。 そこで本研究では,生成した質問数とトレーニングの繰り返し数によるパフォーマンスの尺度を示し,形式的検証と難易度を考慮した提案を,自己再生を成功させる上で不可欠な要素として同定する。
  論文  参考訳（メタデータ） (2025-12-20T00:56:35Z)
• D-REX: A Benchmark for Detecting Deceptive Reasoning in Large Language Models [62.83226685925107]
  Deceptive Reasoning Exposure Suite (D-REX)は、モデルの内部推論プロセスと最終的な出力との相違を評価するために設計された、新しいデータセットである。 D-REXの各サンプルには、敵システムプロンプト、エンドユーザーのテストクエリ、モデルの一見無害な応答、そして重要なことに、モデルの内部チェーンが含まれている。 我々は、D-REXが既存のモデルと安全メカニズムに重大な課題をもたらすことを実証した。
  論文  参考訳（メタデータ） (2025-09-22T15:59:40Z)
• Validating Solidity Code Defects using Symbolic and Concrete Execution powered by Large Language Models [0.0]
  本稿では,Slither-based detectors, Large Language Models (LLMs), Kontrol, Forgeを統合した新しい検出パイプラインを提案する。 私たちのアプローチは、欠陥を確実に検出し、証明を生成するように設計されています。
  論文  参考訳（メタデータ） (2025-09-16T12:46:11Z)
• Preguss: It Analyzes, It Specifies, It Verifies [14.717270519465218]
  大規模言語モデル(LLM)は、最近、形式検証における自動化の度合いを高める可能性を実証している。 この記事では、フォーマルな仕様の生成と改善を自動化するモジュール式できめ細かいフレームワークであるPregussの概要を述べる。
  論文  参考訳（メタデータ） (2025-08-20T08:40:22Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation [52.626086874715284]
  我々は、安全でない出力の階層構造を検証する抽象的DNN検証と呼ばれる新しい問題定式化を導入する。 出力到達可能な集合に関する抽象的解釈と推論を活用することにより,形式的検証プロセスにおいて,複数の安全性レベルを評価することができる。 我々の貢献には、新しい抽象的安全性の定式化と既存のアプローチとの関係を理論的に探求することが含まれる。
  論文  参考訳（メタデータ） (2025-05-08T13:29:46Z)
• Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [60.881609323604685]
  ブラックボックスAPIを通じてアクセスされるLarge Language Models (LLM)は、信頼の課題をもたらす。 ユーザーは、宣伝されたモデル機能に基づいたサービスの料金を支払う。 プロバイダは、運用コストを削減するために、特定のモデルを安価で低品質の代替品に隠蔽的に置き換えることができる。 この透明性の欠如は、公正性を損なうとともに、信頼を損なうとともに、信頼性の高いベンチマークを複雑にする。
  論文  参考訳（メタデータ） (2025-04-07T03:57:41Z)
• Thinking Longer, Not Larger: Enhancing Software Engineering Agents via Scaling Test-Time Compute [61.00662702026523]
  より大規模なモデルではなく、推論時間の増加を活用する統合されたテスト時間計算スケーリングフレームワークを提案する。 当社のフレームワークには,内部TTCと外部TTCの2つの補完戦略が組み込まれている。 当社の textbf32B モデルは,DeepSeek R1 671B や OpenAI o1 など,はるかに大きなモデルを上回る 46% の課題解決率を実現している。
  論文  参考訳（メタデータ） (2025-03-31T07:31:32Z)
• Analogous Alignments: Digital "Formally" meets Analog [0.0]
  本稿では,デジタルブロックとアナログブロックを組み合わせた混合信号知的特性(IP)の実用的形式検証に着目する。 Digital and Analog Mixed-Signal (AMS)設計は、本質的に異なるが、形式的な検証設定でシームレスに統合される。
  論文  参考訳（メタデータ） (2024-09-23T13:38:31Z)
• Designing and Implementing a Generator Framework for a SIMD Abstraction Library [53.84310825081338]
  SIMD抽象化ライブラリを生成するための新しいエンドツーエンドフレームワークであるTSLGenを提案する。 私たちのフレームワークは既存のライブラリに匹敵するもので、同じパフォーマンスを実現しています。
  論文  参考訳（メタデータ） (2024-07-26T13:25:38Z)
• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  問題を非現実的な仮定にシフトすることなく,スケーラブルな形式検証アルゴリズムを開発する。 問題を非現実的な仮定にシフトさせることなく,スケーラブルな形式検証アルゴリズムを開発するためには,バリア証明書の概念を用いる。 本稿では,2乗法最適化とガウス過程エンベロープを用いて効率よくプログラムを解く方法を示す。
  論文  参考訳（メタデータ） (2024-03-15T17:32:02Z)
• Unsupervised Continual Anomaly Detection with Contrastively-learned Prompt [80.43623986759691]
  UCADと呼ばれる新しい非教師付き連続異常検出フレームワークを提案する。 このフレームワークは、対照的に学習したプロンプトを通じて、UDAに継続的な学習能力を持たせる。 我々は総合的な実験を行い、教師なし連続異常検出とセグメンテーションのベンチマークを設定した。
  論文  参考訳（メタデータ） (2024-01-02T03:37:11Z)
• Scaling #DNN-Verification Tools with Efficient Bound Propagation and Parallel Computing [57.49021927832259]
  ディープニューラルネットワーク(DNN)は多くのシナリオで異常な結果を示した強力なツールです。 しかし、それらの複雑な設計と透明性の欠如は、現実世界のアプリケーションに適用する際の安全性上の懸念を提起する。 DNNの形式的検証(FV)は、安全面の証明可能な保証を提供する貴重なソリューションとして登場した。
  論文  参考訳（メタデータ） (2023-12-10T13:51:25Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)
• A Scalable Formal Verification Methodology for Data-Oblivious Hardware [3.518548208712866]
  本稿では,標準プロパティチェック手法を用いて,ハードウェアにおけるデータ公開動作を正式に検証する手法を提案する。 この帰納的特性の証明は,マイクロアーキテクチャレベルでのデータ公開性を徹底的に検証するのに十分であることを示す。 あるケーススタディでは、広範囲に検証され、高度にセキュアなIBEX RISC-Vコアにおいて、データ依存のタイミング違反を発見した。
  論文  参考訳（メタデータ） (2023-08-15T13:19:17Z)
• (Security) Assertions by Large Language Models [25.270188328436618]
  セキュリティのためのハードウェアアサーション生成において,コード生成に新たな大規模言語モデル(LLM)を用いることを検討する。 我々は、人気のあるLCMに注目し、プロンプトの様々なレベルの詳細を考慮し、アサーションを箱から書き出す能力を特徴付ける。
  論文  参考訳（メタデータ） (2023-06-24T17:44:36Z)
• Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version) [67.99023219822564]
  我々はリレーショナルアクションベース(RAB)の一般的な枠組みを紹介する。 RABは両方の制限を解除することで既存のモデルを一般化する。 データ対応ビジネスプロセスのベンチマークにおいて、このアプローチの有効性を実証する。
  論文  参考訳（メタデータ） (2022-08-12T17:03:50Z)
• Fingerprint recognition with embedded presentation attacks detection: are we ready? [6.0168714922994075]
  セキュリティアプリケーションのための指紋認証システムの拡散は,ソフトウェアベースのプレゼンテーション攻撃アルゴリズム(PAD)をそのようなシステムに組み込むことを急ぐ。 現在の研究では、指紋認証システムに組み込む際の有効性についてはあまり言及されていない。 本稿では,PADと検証段階を逐次実施する場合の2つの個別システムの受信者動作特性(ROC)の関係を確率論的にモデル化した性能シミュレータを提案する。
  論文  参考訳（メタデータ） (2021-10-20T13:53:16Z)

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

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