論文の概要: Global Microprocessor Correctness in the Presence of Transient Execution
- arxiv url: http://arxiv.org/abs/2506.17154v1
- Date: Fri, 20 Jun 2025 16:56:14 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-06-23 19:00:05.553049
- Title: Global Microprocessor Correctness in the Presence of Transient Execution
- Title（参考訳）: 過渡的実行の有無における大域的マイクロプロセッサの正確性
- Authors: Andrew T. Walter, Konstantinos Athanasiou, Panagiotis Manolios,
- Abstract要約: 我々は、洗練の理論を用いて、正式な仕様の使用を提唱する。
我々は、MeltdownやSpectreなど、一時的な実行攻撃に対処するために使用できる正当性の概念を紹介します。
- 参考スコア（独自算出の注目度）: 0.16385815610837165
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Correctness for microprocessors is generally understood to be conformance with the associated instruction set architecture (ISA). This is the basis for one of the most important abstractions in computer science, allowing hardware designers to develop highly-optimized processors that are functionally "equivalent" to an ideal processor that executes instructions atomically. This specification is almost always informal, e.g., commercial microprocessors generally do not come with conformance specifications. In this paper, we advocate for the use of formal specifications, using the theory of refinement. We introduce notions of correctness that can be used to deal with transient execution attacks, including Meltdown and Spectre. Such attacks have shown that ubiquitous microprocessor optimizations, appearing in numerous processors for decades, are inherently buggy. Unlike alternative approaches that use non-interference properties, our notion of correctness is global, meaning it is single specification that: formalizes conformance, includes functional correctness and is parameterized by an microarchitecture. We introduce action skipping refinement, a new type of refinement and we describe how our notions of refinement can be decomposed into properties that are more amenable to automated verification using the the concept of shared-resource commitment refinement maps. We do this in the context of formal, fully executable bit- and cycle-accurate models of an ISA and a microprocessor. Finally, we show how light-weight formal methods based on property-based testing can be used to identify transient execution bugs.
- Abstract（参考訳）: マイクロプロセッサの正確性は、一般的に、関連する命令セットアーキテクチャ(ISA)に準拠していると理解されている。
これはコンピュータ科学において最も重要な抽象化の1つであり、ハードウェア設計者は、原子的に命令を実行する理想的なプロセッサと機能的に「等価」な高度に最適化されたプロセッサを開発することができる。
この仕様は、ほとんど常に非公式であり、例えば、商用マイクロプロセッサは通常、適合仕様を持っていない。
本稿では,改良理論を用いて,形式仕様の活用を提唱する。
我々は、MeltdownやSpectreなど、一時的な実行攻撃に対処するために使用できる正当性の概念を紹介します。
このような攻撃は、何十年にもわたって多くのプロセッサに現れるユビキタスなマイクロプロセッサ最適化が本質的にバグが多いことを示している。
非干渉特性を使用する他のアプローチとは異なり、我々の正当性の概念はグローバルであり、つまり、適合性を形式化し、機能的正当性を含み、マイクロアーキテクチャによってパラメータ化される単一の仕様である。
我々は,新しいタイプの改良であるアクション・スキップ・リファインメントを導入し,共有リソース・コミット・リファインメント・マップという概念を用いて,我々のリファインメントの概念を,自動検証に適する特性に分解する方法について述べる。
我々は、ISAとマイクロプロセッサの形式的、完全な実行可能ビットおよびサイクル精度のモデルでこれを行う。
最後に、プロパティベースのテストに基づく軽量な形式メソッドを用いて、過渡的な実行バグを特定する方法を示す。
関連論文リスト
- Valida ISA Spec, version 1.0: A zk-Optimized Instruction Set Architecture [2.0790368408580138]
Valida命令セットアーキテクチャはzkVMの実装のために設計されており、高速で効率的な実行証明のために最適化されている。
この仕様は、Valida用のzkVMとコンパイラツールチェーンの実装をガイドすることを目的としている。
論文 参考訳（メタデータ） (2025-05-12T23:03:02Z) - Computational Reasoning of Large Language Models [51.629694188014064]
textbfTuring Machine Benchは,Large Language Models(LLM)による推論プロセスの実行能力を評価するベンチマークである。
TMBenchには、自己完結型および知識に依存しない推論、最小主義的な多段階構造、制御可能な難易度、チューリングマシンに基づく理論的基礎の4つの重要な特徴が組み込まれている。
論文 参考訳（メタデータ） (2025-04-29T13:52:47Z) - Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
本稿では,検証対応言語における仕様の質を評価するための指標を提案する。
MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。
また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
論文 参考訳（メタデータ） (2024-06-14T06:52:08Z) - Object-Centric Conformance Alignments with Synchronization (Extended Version) [57.76661079749309]
対象中心のペトリネットが一対多の関係を捉える能力と,その同一性に基づいたオブジェクトの比較と同期を行う識別子を持つペトリネットの能力を組み合わせた,新たな形式主義を提案する。
我々は、満足度変調理論(SMT)の符号化に基づく、そのようなネットに対する適合性チェック手法を提案する。
論文 参考訳（メタデータ） (2023-12-13T21:53:32Z) - A Scalable Formal Verification Methodology for Data-Oblivious Hardware [3.518548208712866]
本稿では,標準プロパティチェック手法を用いて,ハードウェアにおけるデータ公開動作を正式に検証する手法を提案する。
この帰納的特性の証明は,マイクロアーキテクチャレベルでのデータ公開性を徹底的に検証するのに十分であることを示す。
あるケーススタディでは、広範囲に検証され、高度にセキュアなIBEX RISC-Vコアにおいて、データ依存のタイミング違反を発見した。
論文 参考訳（メタデータ） (2023-08-15T13:19:17Z) - Automatic Program Instrumentation for Automatic Verification (Extended
Technical Report) [0.0]
帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。
本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。
我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
論文 参考訳（メタデータ） (2023-05-26T14:55:35Z) - Task-Oriented Over-the-Air Computation for Multi-Device Edge AI [57.50247872182593]
エッジAIをサポートするための6Gネットワークは、AIタスクの効率的かつ効率的な実行に焦点を当てたタスク指向のテクニックを備えている。
本稿では,マルチデバイススプリット推論システムにおけるタスク指向オーバー・ザ・エア計算(AirComp)方式を提案する。
論文 参考訳（メタデータ） (2022-11-02T16:35:14Z) - How Fine-Tuning Allows for Effective Meta-Learning [50.17896588738377]
MAMLライクなアルゴリズムから派生した表現を解析するための理論的フレームワークを提案する。
我々は,勾配降下による微調整により得られる最良予測器のリスク境界を提示し,アルゴリズムが共有構造を有効活用できることを実証する。
この分離の結果、マイニングベースのメソッド、例えばmamlは、少数ショット学習における"frozen representation"目標を持つメソッドよりも優れている。
論文 参考訳（メタデータ） (2021-05-05T17:56:00Z) - Automatic Microprocessor Performance Bug Detection [3.6462412165522466]
本稿では,マイクロプロセッサの性能欠陥を検出するための2段階の機械学習手法を提案する。
我々の最良の手法は、ICCの影響が1%を超えるマイクロプロセッサコアのパフォーマンスバグの91.5%を検知する。
メモリシステムのバグを評価した結果,偽陽性ゼロで100%検出できることがわかった。
論文 参考訳（メタデータ） (2020-11-17T17:18:45Z) - The Advantage of Conditional Meta-Learning for Biased Regularization and
Fine-Tuning [50.21341246243422]
バイアスレギュラー化と微調整は、最近の2つのメタラーニングアプローチである。
本稿では,条件付き関数マッピングタスクの側情報をメタパラメータベクトルに推論する条件付きメタラーニングを提案する。
次に、実際には同等の利点をもたらす凸メタアルゴリズムを提案する。
論文 参考訳（メタデータ） (2020-08-25T07:32:16Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。