論文の概要: Rigorous Evaluation of Microarchitectural Side-Channels with Statistical Model Checking

• arxiv url: http://arxiv.org/abs/2510.02475v1
• Date: Thu, 02 Oct 2025 18:31:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-06 16:35:52.128854
• Title: Rigorous Evaluation of Microarchitectural Side-Channels with Statistical Model Checking
• Title（参考訳）: 統計的モデル検査によるマイクロアーキテクチャサイドチェンジの厳密性評価
• Authors: Weihang Li, Pete Crowley, Arya Tschand, Yu Wang, Miroslav Pajic, Daniel Sorin,
• Abstract要約: マイクロアーキテクチャー側チャネルの定量的評価に統計モデルチェックを導入する。 SMCではプロセッサを不透明なボックスとして扱うことができ、それらを抽象化したり単純化したりする必要がなくなる。 3つのケーススタディを通してSMCの有効性を実証した。
• 参考スコア（独自算出の注目度）: 10.093795733515181
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Rigorous quantitative evaluation of microarchitectural side channels is challenging for two reasons. First, the processors, attacks, and defenses often exhibit probabilistic behaviors. These probabilistic behaviors arise due to natural noise in systems (e.g., from co-running processes), probabilistic side channel attacks, and probabilistic obfuscation defenses. Second, microprocessors are extremely complex. Previous evaluation methods have relied on abstract or simplified models, which are necessarily less detailed than real systems or cycle-by-cycle simulators, and these models may miss important phenomena. Whereas a simple model may suffice for estimating performance, security issues frequently manifest in the details. We address this challenge by introducing Statistical Model Checking (SMC) to the quantitative evaluation of microarchitectural side channels. SMC is a rigorous statistical technique that can process the results of probabilistic experiments and provide statistical guarantees, and it has been used in computing applications that depend heavily on statistical guarantees (e.g., medical implants, vehicular computing). With SMC, we can treat processors as opaque boxes, and we do not have to abstract or simplify them. We demonstrate the effectiveness of SMC through three case studies, in which we experimentally show that SMC can evaluate existing security vulnerabilities and defenses and provide qualitatively similar conclusions with greater statistical rigor, while making no simplifying assumptions or abstractions. We also show that SMC can enable a defender to quantify the amount of noise necessary to have a desired level of confidence that she has reduced an attacker's probability of success to less than a desired threshold, thus providing the defender with an actionable plan for obfuscation via noise injection.
• Abstract（参考訳）: マイクロアーキテクチャー側チャネルの厳密な定量的評価は2つの理由から困難である。 第一に、プロセッサ、攻撃、防御は確率的な振る舞いを示すことが多い。 これらの確率的挙動は、システムの自然ノイズ(例えば、共走過程からの)、確率的側チャネル攻撃、確率的難読化防御(probabilistic obfuscation defenses)によって生じる。 第二に、マイクロプロセッサは非常に複雑です。 従来の評価手法は抽象的あるいは単純化されたモデルに依存しており、実際のシステムやサイクルバイサイクルシミュレータよりも必ずしも詳細ではないため、これらのモデルは重要な現象を見逃す可能性がある。 単純なモデルがパフォーマンスを推定するのに十分であるのに対して、セキュリティ問題は詳細にしばしば現れます。 本稿では,マイクロアーキテクチャー側チャネルの定量的評価に統計モデル検査(SMC)を導入することで,この問題に対処する。 SMCは確率的実験の結果を処理し、統計的保証を提供するための厳密な統計手法であり、統計的保証(例えば、医療インプラント、車載コンピューティング)に大きく依存する計算アプリケーションで使われている。 SMCではプロセッサを不透明なボックスとして扱うことができ、それらを抽象化したり単純化したりする必要がなくなる。 本研究では,SMCが既存のセキュリティの脆弱性や防御を評価できることを示すとともに,統計的厳密さを生かした定性的に類似した結論を与えるとともに,仮定や抽象化を単純化しない3つのケーススタディを通じて,SMCの有効性を実証する。 また,SMCは,攻撃者の成功確率を所望の閾値以下に減らし,ノイズ注入による難読化の実行可能なプランをディフェンダーに提供することにより,攻撃者の信頼度を所望のレベルに抑えるために必要なノイズ量を定量化できることを示す。

関連論文リスト

• Model Tampering Attacks Enable More Rigorous Evaluations of LLM Capabilities [49.09703018511403]
  大規模言語モデル(LLM)のリスクと能力の評価は、AIのリスク管理とガバナンスフレームワークにますます取り入れられている。 現在、ほとんどのリスク評価は、システムから有害な振る舞いを誘発する入力を設計することで実施されている。 本稿では,遅延活性化や重みへの修正が可能なモデル改ざん攻撃を用いたLCMの評価を提案する。
  論文  参考訳（メタデータ） (2025-02-03T18:59:16Z)
• What Are the Odds? Improving the foundations of Statistical Model Checking [3.789219860006095]
  マルコフ決定プロセス(MDP)は不確実性の下での意思決定の基本的なモデルである。 従来の検証アルゴリズムは、MDPの振る舞いを管理する確率の正確な知識を前提としている。 我々はMDPの知識を活用する専門的なアプローチを提案する。
  論文  参考訳（メタデータ） (2024-04-08T11:47:46Z)
• White-box validation of quantitative product lines by statistical model checking and process mining [1.0918484507642576]
  本稿では,統計的モデル検査 (SMC) とプロセスマイニング (PM) を統合することで,ソフトウェア製品ライン (PL) モデルの検証手法を提案する。 提案手法は,PL工学領域における機能指向言語QFLanに着目し,豊富なクロスツリーと量的制約を持つPLのモデリングを可能にする。
  論文  参考訳（メタデータ） (2024-01-23T17:27:13Z)
• Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions [59.605246463200736]
  雑音分布の明示的な表現に依存しない新しい制御器合成法を提案する。 まず、連続制御系を有限状態モデルに抽象化し、離散状態間の確率的遷移によってノイズを捕捉する。 我々は最先端の検証技術を用いてマルコフ決定プロセスの間隔を保証し、これらの保証が元の制御システムに受け継がれるコントローラを演算する。
  論文  参考訳（メタデータ） (2023-01-04T10:40:30Z)
• Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty [68.00748155945047]
  複雑な力学系のモデルにおける不確実性を捉えることは、安全なコントローラの設計に不可欠である。 いくつかのアプローチでは、安全と到達可能性に関する時間的仕様を満たすポリシーを形式的な抽象化を用いて合成する。 我々の貢献は、ノイズ、不確実なパラメータ、外乱を含む連続状態モデルに対する新しい抽象的制御法である。
  論文  参考訳（メタデータ） (2022-10-12T07:57:03Z)
• Random Noise vs State-of-the-Art Probabilistic Forecasting Methods : A Case Study on CRPS-Sum Discrimination Ability [4.9449660544238085]
  対象データの統計的特性がCRPS-Sumの識別能力に影響を及ぼすことを示す。 CRPS-Sum計算は各次元におけるモデルの性能を見落としている。 ダミーモデルに対して,ランダムノイズのように見える,より優れたCRPS-Sumを持つことが容易に可能であることを示す。
  論文  参考訳（メタデータ） (2022-01-21T12:36:58Z)
• Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise [59.47042225257565]
  雑音分布の明示的な表現に依存しない新しい計画法を提案する。 まず、連続系を離散状態モデルに抽象化し、状態間の確率的遷移によってノイズを捕捉する。 いわゆる区間マルコフ決定過程(iMDP)の遷移確率区間におけるこれらの境界を捉える。
  論文  参考訳（メタデータ） (2021-10-25T06:18:55Z)
• SAMBA: Safe Model-Based & Active Reinforcement Learning [59.01424351231993]
  SAMBAは、確率論的モデリング、情報理論、統計学といった側面を組み合わせた安全な強化学習のためのフレームワークである。 我々は,低次元および高次元の状態表現を含む安全な力学系ベンチマークを用いて,アルゴリズムの評価を行った。 アクティブなメトリクスと安全性の制約を詳細に分析することで,フレームワークの有効性を直感的に評価する。
  論文  参考訳（メタデータ） (2020-06-12T10:40:46Z)
• Efficient statistical validation with edge cases to evaluate Highly Automated Vehicles [6.198523595657983]
  自動運転車の大規模展開は、まだ解決されていない多くの安全上の課題にもかかわらず、差し迫っているようだ。 既存の標準は、検証が要求をカバーするテストケースのセットだけを必要とする決定論的プロセスに焦点を当てています。 本稿では, 自動生成テストケースを最悪のシナリオに偏り付け, システムの挙動の統計的特性を計算するための新しい手法を提案する。
  論文  参考訳（メタデータ） (2020-03-04T04:35:22Z)

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

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