論文の概要: 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に基づくシステムにおいて,シナリオベースの分解と自動ヒント抽出により,提案手法がスケーラブルであることを示す。
さらに、我々の完全に自動化されたフレームワークは、実際のファームウェア・ハードウエア実装における複雑なバグを特定することができる。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。