論文の概要: RTL2M$μ$PATH: Multi-$μ$PATH Synthesis with Applications to Hardware Security Verification
- arxiv url: http://arxiv.org/abs/2409.19478v1
- Date: Sat, 28 Sep 2024 23:01:48 GMT
- ステータス: 処理完了
- システム内更新日: 2024-11-05 22:57:44.734235
- Title: RTL2M$μ$PATH: Multi-$μ$PATH Synthesis with Applications to Hardware Security Verification
- Title（参考訳）: RTL2M$μ$PATH:マルチ$μ$PATH合成とハードウェアセキュリティ検証への応用
- Authors: Yao Hsiao, Nikos Nikoleris, Artem Khyzha, Dominic P. Mulligan, Gustavo Petri, Christopher W. Fletcher, Caroline Trippel,
- Abstract要約: チェックツールは、プロセッサの正式なメモリ一貫性モデルとセキュリティ検証を自動化する。
このアプローチの有効性にもかかわらず、$mu$SPECモデルの検証ギャップは手書きで書かなければならない。
我々は、RTL2M$mu$PATHと呼ばれる自動的なアプローチとツールを提案し、RTL2$mu$SPECの単一実行パス仮定を解決する。
- 参考スコア（独自算出の注目度）: 8.197637524321545
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The Check tools automate formal memory consistency model and security verification of processors by analyzing abstract models of microarchitectures, called $\mu$SPEC models. Despite the efficacy of this approach, a verification gap between $\mu$SPEC models, which must be manually written, and RTL limits the Check tools' broad adoption. Our prior work, called RTL2$\mu$SPEC, narrows this gap by automatically synthesizing formally verified $\mu$SPEC models from SystemVerilog implementations of simple processors. But, RTL2$\mu$SPEC assumes input designs where an instruction (e.g., a load) cannot exhibit more than one microarchitectural execution path ($\mu$PATH, e.g., a cache hit or miss path) -- its single-execution-path assumption. In this paper, we first propose an automated approach and tool, called RTL2M$\mu$PATH, that resolves RTL2$\mu$SPEC's single-execution-path assumption. Given a SystemVerilog processor design, instruction encodings, and modest design metadata, RTL2M$\mu$PATH finds a complete set of formally verified $\mu$PATHs for each instruction. Next, we make an important observation: an instruction that can exhibit more than one $\mu$PATH strongly indicates the presence of a microarchitectural side channel in the input design. Based on this observation, we then propose an automated approach and tool, called SynthLC, that extends RTL2M$\mu$PATH with a symbolic information flow analysis to support synthesizing a variety of formally verified leakage contracts from SystemVerilog processor designs. Leakage contracts are foundational to state-of-the-art defenses against hardware side-channel attacks. SynthLC is the first automated methodology for formally verifying hardware adherence to them.
- Abstract（参考訳）: Checkツールは、$\mu$SPECモデルと呼ばれるマイクロアーキテクチャの抽象モデルを分析することで、プロセッサの正式なメモリ一貫性モデルとセキュリティ検証を自動化する。
このアプローチの有効性にもかかわらず、手書きで書かなければならない$\mu$SPECモデルの検証ギャップがあり、RTLはCheckツールの広範な採用を制限する。
我々の以前の作業は RTL2$\mu$SPEC と呼ばれ、単純なプロセッサのSystemVerilog 実装から形式的に検証された$\mu$SPEC モデルを自動的に合成することで、このギャップを狭める。
しかし、RTL2$\mu$SPECは、命令(例えば、負荷)が1つ以上のマイクロアーキテクチャ実行パス(\mu$PATH、eg、キャッシュヒットまたはミスパス)を示すことができない入力設計を仮定する。
本稿では、まず、RTL2M$\mu$PATHと呼ばれる自動的なアプローチとツールを提案し、RTL2$\mu$SPECの単一実行パス仮定を解決する。
SystemVerilogプロセッサの設計、命令エンコーディング、そして控えめな設計メタデータが与えられた後、RTL2M$\mu$PATHは各命令に対して正式に認証された$\mu$PATHの完全なセットを見つける。
次に, 入力設計におけるマイクロアーキテクチャ側チャネルの存在を強く示し, 1ドル以上を提示できる命令について述べる。
そこで本研究では,RTL2M$\mu$PATHをシンボル情報フロー解析により拡張し,SystemVerilogプロセッサ設計から公式に検証された各種リーク契約の合成を支援する,SynthLCという自動手法とツールを提案する。
漏洩契約は、ハードウェアサイドチャネル攻撃に対する最先端の防御に基礎を置いている。
SynthLCは、ハードウェアの付着を正式に検証する最初の自動化手法である。
関連論文リスト
- Verifying Non-friendly Formal Verification Designs: Can We Start Earlier? [2.1626093085892144]
本稿では,2つの主要なステップからなるメタモデリング技術に基づく自動手法を提案する。
まず、C++で書かれた未使用のアルゴリズム記述を、生成されたアサーションを使用して早期に検証する。
第2に、HLECとそのメタモデルパラメータを用いて、このアルゴリズム記述をシーケンシャルな設計に対して検証する。
論文 参考訳（メタデータ） (2024-10-24T06:09:40Z) - VerilogCoder: Autonomous Verilog Coding Agents with Graph-based Planning and Abstract Syntax Tree (AST)-based Waveform Tracing Tool [4.027984601764008]
We propose VerilogCoder, a system of multiple Artificial Intelligence (AI) agent for Verilog code generation。
提案手法は、構文的に94.2%、機能的に正当なVerilogコードを生成する。
論文 参考訳（メタデータ） (2024-08-15T20:06:06Z) - Cross-Modality Program Representation Learning for Electronic Design Automation with High-Level Synthesis [45.471039079664656]
ドメイン固有アクセラレータ(DSA)は、ディープラーニングや自律運転などのアプリケーションで人気を集めている。
本稿では,ソースコードシーケンスのモダリティとグラフのモダリティを深く,きめ細かな方法で相互作用できるモデルであるProgSGを提案する。
ProgSGは、設計性能予測のRMSEを最大22%の価格で削減し、設計を平均1.10Times$で識別する。
論文 参考訳（メタデータ） (2024-06-13T22:34:58Z) - Transfer Q Star: Principled Decoding for LLM Alignment [105.89114186982972]
Transfer $Q*$は、ベースラインモデルを通してターゲット報酬$r$の最適値関数を推定する。
提案手法は, 従来のSoTA法で観測された準最適差を著しく低減する。
論文 参考訳（メタデータ） (2024-05-30T21:36:12Z) - Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source Processors [6.061386291375516]
本稿では,オープンソースマイクロアーキテクチャのためのハードウェア・ソフトウェアリーク契約を合成する半自動手法を提案する。
我々はRISC-V ISAのためにこの手法をインスタンス化し、IbexおよびCVA6オープンソースプロセッサに適用した。
論文 参考訳（メタデータ） (2024-01-17T17:54:53Z) - Single-Stage Visual Relationship Learning using Conditional Queries [60.90880759475021]
TraCQは、マルチタスク学習問題とエンティティペアの分布を回避する、シーングラフ生成の新しい定式化である。
我々は,DETRをベースとしたエンコーダ-デコーダ条件付きクエリを用いて,エンティティラベル空間を大幅に削減する。
実験結果から、TraCQは既存のシングルステージシーングラフ生成法よりも優れており、Visual Genomeデータセットの最先端の2段階メソッドを多く上回っていることがわかった。
論文 参考訳（メタデータ） (2023-06-09T06:02:01Z) - ProgSG: Cross-Modality Representation Learning for Programs in
Electronic Design Automation [38.023395256208055]
高レベル合成(HLS)により、開発者はCとC++のソフトウェアコード形式で高レベルな記述をコンパイルできる。
HLSツールは相変わらず、プラグマで表されるマイクロアーキテクチャの決定を必要とする。
本稿では,ソースコードシーケンスのモダリティとグラフのモダリティを深く,きめ細かな方法で相互に相互作用させることができるProgSGを提案する。
論文 参考訳（メタデータ） (2023-05-18T09:44:18Z) - Simplifying and Understanding State Space Models with Diagonal Linear
RNNs [56.33053691749856]
本研究は、離散化ステップを解消し、バニラ対角線形RNNに基づくモデルを提案する。
概念的にはるかに単純であるにもかかわらず、$mathrmDLR$は以前提案したSSMと同じくらいのパフォーマンスを示す。
また、合成シーケンス・ツー・シーケンス・タスクのスイートによって、SSMとアテンションベースモデルの表現性も特徴付ける。
論文 参考訳（メタデータ） (2022-12-01T18:53:06Z) - Monitoring ROS2: from Requirements to Autonomous Robots [58.720142291102135]
本稿では,構造化自然言語で記述された要件から自律ロボットのランタイムモニタを生成するための形式的アプローチの概要について述べる。
当社のアプローチでは,Fletal Requirement Elicitation Tool (FRET) とランタイム検証フレームワークであるCopilotを,Ogma統合ツールを通じて統合しています。
論文 参考訳（メタデータ） (2022-09-28T12:19:13Z) - Statistically Meaningful Approximation: a Case Study on Approximating
Turing Machines with Transformers [50.85524803885483]
本研究は,統計的学習性を示すために近似ネットワークを必要とする統計有意(SM)近似の形式的定義を提案する。
回路とチューリングマシンの2つの機能クラスに対するSM近似について検討する。
論文 参考訳（メタデータ） (2021-07-28T04:28:55Z) - Self-Supervised Log Parsing [59.04636530383049]
大規模ソフトウェアシステムは、大量の半構造化ログレコードを生成する。
既存のアプローチは、ログ特化や手動ルール抽出に依存している。
本稿では,自己教師付き学習モデルを用いて解析タスクをマスク言語モデリングとして定式化するNuLogを提案する。
論文 参考訳（メタデータ） (2020-03-17T19:25:25Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。