論文の概要: A Scalable Formal Verification Methodology for Data-Oblivious Hardware
- arxiv url: http://arxiv.org/abs/2308.07757v2
- Date: Mon, 11 Mar 2024 08:47:15 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-17 17:20:31.160580
- Title: A Scalable Formal Verification Methodology for Data-Oblivious Hardware
- Title（参考訳）: データ公開ハードウェアのためのスケーラブルな形式検証手法
- Authors: Lucas Deutschmann, Johannes Mueller, Mohammad Rahmani Fadiheh, Dominik Stoffel, Wolfgang Kunz,
- Abstract要約: 本稿では,標準プロパティチェック手法を用いて,ハードウェアにおけるデータ公開動作を正式に検証する手法を提案する。
この帰納的特性の証明は,マイクロアーキテクチャレベルでのデータ公開性を徹底的に検証するのに十分であることを示す。
あるケーススタディでは、広範囲に検証され、高度にセキュアなIBEX RISC-Vコアにおいて、データ依存のタイミング違反を発見した。
- 参考スコア（独自算出の注目度）: 3.518548208712866
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The importance of preventing microarchitectural timing side channels in security-critical applications has surged in recent years. Constant-time programming has emerged as a best-practice technique for preventing the leakage of secret information through timing. It is based on the assumption that the timing of certain basic machine instructions is independent of their respective input data. However, whether or not an instruction satisfies this data-independent timing criterion varies between individual processor microarchitectures. In this paper, we propose a novel methodology to formally verify data-oblivious behavior in hardware using standard property checking techniques. The proposed methodology is based on an inductive property that enables scalability even to complex out-of-order cores. We show that proving this inductive property is sufficient to exhaustively verify data-obliviousness at the microarchitectural level. In addition, the paper discusses several techniques that can be used to make the verification process easier and faster. We demonstrate the feasibility of the proposed methodology through case studies on several open-source designs. One case study uncovered a data-dependent timing violation in the extensively verified and highly secure IBEX RISC-V core. In addition to several hardware accelerators and in-order processors, our experiments also include RISC-V BOOM, a complex out-of-order processor, highlighting the scalability of the approach.
- Abstract（参考訳）: 近年,セキュリティクリティカルなアプリケーションにおける微構造的タイミング側チャネルの防止の重要性が高まっている。
一定時間プログラミングは、タイミングによる秘密情報の漏洩を防止するためのベストプラクティスとして登場した。
これは、特定の基本機械命令のタイミングがそれぞれの入力データとは独立であるという仮定に基づいている。
しかし、命令がデータに依存しないタイミング基準を満たすか否かは、個々のプロセッサマイクロアーキテクチャによって異なる。
本稿では,標準プロパティチェック手法を用いて,ハードウェアにおけるデータ公開動作を正式に検証する手法を提案する。
提案手法は,複雑なアウトオブオーダコアへの拡張性を実現する帰納的特性に基づく。
この帰納的特性の証明は,マイクロアーキテクチャレベルでのデータ公開性を徹底的に検証するのに十分であることを示す。
さらに,本論文では,検証プロセスを迅速かつ迅速にするためのいくつかの手法について論じる。
本稿では,いくつかのオープンソース設計のケーススタディを通じて提案手法の有効性を実証する。
あるケーススタディでは、広範囲に検証され、高度にセキュアなIBEX RISC-Vコアにおいて、データ依存のタイミング違反を発見した。
いくつかのハードウェアアクセラレータとインオーダープロセッサに加えて、我々の実験にはRISC-V BOOMという複雑なアウトオブオーダープロセッサが含まれており、このアプローチのスケーラビリティを強調しています。
関連論文リスト
- Unsupervised Continual Anomaly Detection with Contrastively-learned
Prompt [80.43623986759691]
UCADと呼ばれる新しい非教師付き連続異常検出フレームワークを提案する。
このフレームワークは、対照的に学習したプロンプトを通じて、UDAに継続的な学習能力を持たせる。
我々は総合的な実験を行い、教師なし連続異常検出とセグメンテーションのベンチマークを設定した。
論文 参考訳（メタデータ） (2024-01-02T03:37:11Z) - Secure Instruction and Data-Level Information Flow Tracking Model for RISC-V [0.0]
不正アクセス、障害注入、およびプライバシー侵害は、信頼できないアクターによる潜在的な脅威である。
本稿では,実行時セキュリティがシステム完全性を保護するために,IFT(Information Flow Tracking)技術を提案する。
本研究では,ハードウェアベース IFT 技術とゲートレベル IFT (GLIFT) 技術を統合したマルチレベル IFT モデルを提案する。
論文 参考訳（メタデータ） (2023-11-17T02:04:07Z) - A Discrepancy Aware Framework for Robust Anomaly Detection [51.710249807397695]
本稿では,DAF(Disdisrepancy Aware Framework)を提案する。
本手法は,デコーダの欠陥同定に外見に依存しないキューを利用して,その合成外観への依存を緩和する。
単純な合成戦略の下では,既存の手法を大きなマージンで上回り,また,最先端のローカライゼーション性能も達成している。
論文 参考訳（メタデータ） (2023-10-11T15:21:40Z) - HIVE: Scalable Hardware-Firmware Co-Verification using Scenario-based Decomposition and Automated Hint Extraction [2.977255700811213]
ハードウェア確認ソフトの共検証は、信頼できるシステムの設計に不可欠である。
ハードウェアを手動で抽象化したり、ヒントを手動で生成することで、ファームウェア検証中の状態空間を削減できる有望な方法がある。
本稿では,シミュレーションに基づく検証のスケーラビリティと形式検証の完全性とを効果的に組み合わせる。
論文 参考訳（メタデータ） (2023-09-14T19:24:57Z) - Diagnostic Spatio-temporal Transformer with Faithful Encoding [54.02712048973161]
本稿では,データ生成プロセスが複合時間(ST)依存性を持つ場合の異常診断の課題について述べる。
我々は、ST依存を時系列分類の副産物として学習する、教師付き依存発見として問題を定式化する。
既存のST変圧器で使用される時間的位置符号化は、高周波数(短時間スケール)の周波数をキャプチャする重大な制限を有することを示す。
また、空間的および時間的方向の両方で容易に消費可能な診断情報を提供する新しいST依存性発見フレームワークを提案する。
論文 参考訳（メタデータ） (2023-05-26T05:31:23Z) - PAC-Based Formal Verification for Out-of-Distribution Data Detection [4.406331747636832]
本研究は、VAEの符号化プロセスを用いて、OOD検出に基づくほぼ正しい(PAC)保証を行う。
ユーザ定義の信頼性で不慣れなインスタンスに検出エラーをバインドするために使用される。
論文 参考訳（メタデータ） (2023-04-04T07:33:02Z) - The Wyner Variational Autoencoder for Unsupervised Multi-Layer Wireless
Fingerprinting [6.632671046812309]
識別性能を向上させるための多層署名を共同で検討する多層フィンガープリントフレームワークを提案する。
従来の手法とは対照的に,近年のマルチビュー機械学習のパラダイムを活用して,マルチレイヤ機能間で共有されるデバイス情報を,監督なしでクラスタ化することができる。
実験の結果,提案手法は教師なしと教師なしの両方の設定において,最先端のベースラインよりも優れていた。
論文 参考訳（メタデータ） (2023-03-28T10:05:06Z) - A Robust and Explainable Data-Driven Anomaly Detection Approach For
Power Electronics [56.86150790999639]
本稿では,2つの異常検出・分類手法,すなわち行列プロファイルアルゴリズムと異常変換器を提案する。
行列プロファイルアルゴリズムは、ストリーミング時系列データにおけるリアルタイム異常を検出するための一般化可能なアプローチとして適している。
検知器の感度、リコール、検出精度を調整するために、一連のカスタムフィルタが作成され、追加される。
論文 参考訳（メタデータ） (2022-09-23T06:09:35Z) - Conformance Checking with Uncertainty via SMT (Extended Version) [66.58864135810981]
データ認識参照プロセスに対する不確実なログの適合性を確認する方法を示す。
我々のアプローチはモジュラーであり、異なるタイプの不確実性に均質に適合する。
本研究は,概念実証によるアプローチの正しさと実現可能性を示す。
論文 参考訳（メタデータ） (2022-06-15T11:39:45Z) - CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT
(Extended Version) [62.96267257163426]
我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。
まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。
次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
論文 参考訳（メタデータ） (2021-03-18T20:22:50Z) - Frequency-based Multi Task learning With Attention Mechanism for Fault
Detection In Power Systems [6.4332733596587115]
本稿では,障害検出のための新しいディープラーニングベースのアプローチを導入し,実際のデータセット,すなわち部分放電検出タスクのためのKaggleプラットフォーム上でテストする。
提案手法では,時系列の特徴を抽出するためのアテンション機構を備えたLong-Short Term Memoryアーキテクチャを採用し,信号の周波数情報を利用した1D-Convolutional Neural Network構造を用いて予測を行う。
論文 参考訳（メタデータ） (2020-09-15T02:01:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。