論文の概要: Synthesis of Sound and Precise Leakage Contracts for Open-Source RISC-V Processors

• arxiv url: http://arxiv.org/abs/2509.06509v1
• Date: Mon, 08 Sep 2025 10:14:52 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-09 14:07:04.058447
• Title: Synthesis of Sound and Precise Leakage Contracts for Open-Source RISC-V Processors
• Title（参考訳）: オープンソースのRISC-Vプロセッサのための音・高精度漏洩契約の合成
• Authors: Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, Marco Guarnieri,
• Abstract要約: 漏洩契約は、プロセッサがマイクロアーキテクチャー側チャネルを介してリークする可能性のある情報をキャプチャすることを目的としている。 LeaSynは、レジスタ・トランスファーレベルでプロセッサ設計に正確かつ正確である漏洩契約を自動的に合成する最初のツールである。 我々の実験は、LeaSynの契約は、既存のアプローチによって構築された契約よりも、より正確(すなわち、ターゲットプロセッサの実際のリークを忠実に表現する)であることを示している。
• 参考スコア（独自算出の注目度）: 10.160855270787962
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Leakage contracts have been proposed as a new security abstraction at the instruction set architecture level. Leakage contracts aim to capture the information that processors may leak via microarchitectural side channels. Recently, the first tools have emerged to verify whether a processor satisfies a given contract. However, coming up with a contract that is both sound and precise for a given processor is challenging, time-consuming, and error-prone, as it requires in-depth knowledge of the timing side channels introduced by microarchitectural optimizations. In this paper, we address this challenge by proposing LeaSyn, the first tool for automatically synthesizing leakage contracts that are both sound and precise for processor designs at register-transfer level. Starting from a user-provided contract template that captures the space of possible contracts, LeaSyn automatically constructs a contract, alternating between contract synthesis, which ensures precision based on an empirical characterization of the processor's leaks, and contract verification, which ensures soundness. Using LeaSyn, we automatically synthesize contracts for six open-source RISC-V CPUs for a variety of contract templates. Our experiments indicate that LeaSyn's contracts are sound and more precise (i.e., represent the actual leaks in the target processor more faithfully) than contracts constructed by existing approaches.
• Abstract（参考訳）: リーク契約は命令セットアーキテクチャレベルでの新しいセキュリティ抽象化として提案されている。 漏洩契約は、プロセッサがマイクロアーキテクチャー側チャネルを介してリークする可能性のある情報をキャプチャすることを目的としている。 最近、プロセッサが与えられた契約を満たすかどうかを検証する最初のツールが登場した。 しかし、マイクロアーキテクチャ最適化によって導入されたタイミング側チャネルの詳細な知識を必要とするため、与えられたプロセッサの正確かつ正確な契約を思いつくのは困難であり、時間がかかり、エラーが発生しやすい。 本稿では,レジスタ・トランスファーレベルのプロセッサ設計において正確かつ健全なリーク契約を自動合成する最初のツールであるLeaSynを提案する。 考えられるコントラクトの空間をキャプチャするユーザが提供するコントラクトテンプレートから始めると、LeaSynは自動的にコントラクトを構築し、コントラクト合成を交互に行う。 LeaSynを用いて、6つのオープンソースRISC-VCPUのコントラクトを自動的に合成し、さまざまなコントラクトテンプレートを生成する。 我々の実験は、LeaSynの契約は、既存のアプローチによって構築された契約よりも、より正確(すなわち、ターゲットプロセッサの実際のリークを忠実に表現する)であることを示している。

関連論文リスト

• Exploring Microstructural Dynamics in Cryptocurrency Limit Order Books: Better Inputs Matter More Than Stacking Another Hidden Layer [9.2463347238923]
  ニューラルネットワークに余分な隠蔽層やパラメータを追加することで、短期的な価格予測が真に向上するかどうかを検討することを目的としている。 我々は,BTC/USDT LOBスナップショットを100ミリ秒から複数秒間隔で公開して,解釈可能なベースライン,ロジスティック回帰,XGBoostからディープアーキテクチャ(DeepLOB,Conv1D+LSTM)まで,モデルをベンチマークする。
  論文  参考訳（メタデータ） (2025-06-06T05:43:30Z)
• Specification Mining for Smart Contracts with Trace Slicing and Predicate Abstraction [10.723903783651537]
  過去の取引履歴から契約仕様を推測するための仕様マイニング手法を提案する。 提案手法は,トランザクション履歴から統計的に推測されるプログラム不変量を伴って,関数呼び出しの高レベルな振る舞い自動を導出する。 SMCONは、高いコードカバレッジと最大56%のスピードアップを達成するためのスマートコントラクトのシンボリック分析を強化するために、合理的に正確な仕様をマイニングしている。
  論文  参考訳（メタデータ） (2024-03-20T03:39:51Z)
• Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source Processors [6.061386291375516]
  本稿では,オープンソースマイクロアーキテクチャのためのハードウェア・ソフトウェアリーク契約を合成する半自動手法を提案する。 我々はRISC-V ISAのためにこの手法をインスタンス化し、IbexおよびCVA6オープンソースプロセッサに適用した。
  論文  参考訳（メタデータ） (2024-01-17T17:54:53Z)
• HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
  信頼性コンピューティングは、Trusted Execution Environments(TEEs)と呼ばれる特別なハードウェア隔離ユニットを使用して、コテナントクラウドデプロイメントにおける機密コードとデータの保護を可能にする。 低レベルのC/C++ベースのツールチェーンを提供するTEEは、固有のメモリ安全性の脆弱性の影響を受けやすく、明示的で暗黙的な情報フローのリークを監視するための言語構造が欠如している。 私たちは、Haskellに埋め込まれたドメイン固有言語(cla)であるHasTEE+を使って、上記の問題に対処します。
  論文  参考訳（メタデータ） (2024-01-17T00:56:23Z)
• Gradual Verification for Smart Contracts [0.4543820534430522]
  Algosはスマートコントラクトを通じてセキュアなリソーストランザクションを実現する。 従来の検証技術は、包括的なセキュリティ保証の提供に不足している。 本稿では,段階的検証という段階的なアプローチを紹介する。
  論文  参考訳（メタデータ） (2023-11-22T12:42:26Z)
• ConReader: Exploring Implicit Relations in Contracts for Contract Clause Extraction [84.0634340572349]
  法律契約における暗黙の関係をモデル化し,契約条項の自動抽出(CCE)について検討する。 本研究ではまず,契約の複雑性問題を包括的に分析し,契約に共通する3つの暗黙の関係を抽出する。 本稿では,上記の3つの関係を利用して,より優れたコントラクト理解とCCEの改善を実現するための新しいフレームワークであるConReaderを提案する。
  論文  参考訳（メタデータ） (2022-10-17T02:15:18Z)
• Data post-processing for the one-way heterodyne protocol under composable finite-size security [62.997667081978825]
  本研究では,実用的連続可変(CV)量子鍵分布プロトコルの性能について検討する。 ヘテロダイン検出を用いたガウス変調コヒーレント状態プロトコルを高信号対雑音比で検討する。 これにより、プロトコルの実践的な実装の性能を調べ、上記のステップに関連付けられたパラメータを最適化することができる。
  論文  参考訳（メタデータ） (2022-05-20T12:37:09Z)
• Detecting Logical Relation In Contract Clauses [94.85352502638081]
  契約における節間の論理的関係の抽出を自動化する手法を開発する。 結果として得られたアプローチは、コントラクト作者が節間の潜在的な論理的衝突を検出するのに役立つだろう。
  論文  参考訳（メタデータ） (2021-11-02T19:26:32Z)
• Composably secure data processing for Gaussian-modulated continuous variable quantum key distribution [58.720142291102135]
  連続可変量子鍵分布(QKD)は、ボソニックモードの二次構造を用いて、2つのリモートパーティ間の秘密鍵を確立する。 構成可能な有限サイズセキュリティの一般的な設定におけるホモダイン検出プロトコルについて検討する。 特に、ハイレート(非バイナリ)の低密度パリティチェックコードを使用する必要のあるハイシグネチャ・ツー・ノイズ・システマを解析する。
  論文  参考訳（メタデータ） (2021-03-30T18:02:55Z)

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

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