論文の概要: On Kernel's Safety in the Spectre Era (Extended Version)
- arxiv url: http://arxiv.org/abs/2406.07278v1
- Date: Tue, 11 Jun 2024 14:04:58 GMT
- ステータス: 処理完了
- システム内更新日: 2024-06-12 15:44:22.896457
- Title: On Kernel's Safety in the Spectre Era (Extended Version)
- Title(参考訳): スペクトル時代のカーネルの安全性について(拡張版)
- Authors: Davide Davoli, Martin Avanzini, Tamara Rezk,
- Abstract要約: レイアウトのランダム化は、メモリ分離を伴うシステムにおいて、同等の安全性を保証できることを示す。
サイドチャネルと投機的実行を使用できる攻撃者に対しては,カーネルの安全性を回復できないことを示す。
この条件下では,レイアウトのランダム化に頼らずに安全であることを示す。
- 参考スコア(独自算出の注目度): 2.0436753359071913
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The efficacy of address space layout randomization has been formally demonstrated in a shared-memory model by Abadi et al., contingent on specific assumptions about victim programs. However, modern operating systems, implementing layout randomization in the kernel, diverge from these assumptions and operate on a separate memory model with communication through system calls. In this work, we relax Abadi et al.'s language assumptions while demonstrating that layout randomization offers a comparable safety guarantee in a system with memory separation. However, in practice, speculative execution and side-channels are recognized threats to layout randomization. We show that kernel safety cannot be restored for attackers capable of using side-channels and speculative execution and introduce a new condition, that allows us to formally prove kernel safety in the Spectre era. Our research demonstrates that under this condition, the system remains safe without relying on layout randomization. We also demonstrate that our condition can be sensibly weakened, leading to enforcement mechanisms that can guarantee kernel safety for safe system calls in the Spectre era.
- Abstract(参考訳): アドレス空間レイアウトのランダム化の有効性は、Abadiらによって共有メモリモデルで正式に実証されている。
しかし、カーネルにレイアウトのランダム化を実装した現代のオペレーティングシステムは、これらの仮定から分岐し、システムコールを介して通信を行う独立したメモリモデルで動作している。
本研究では,メモリ分離システムにおいて,アバディなどの言語仮定を緩和するとともに,レイアウトのランダム化が同等の安全性を保証できることを実証する。
しかし、実際には、投機的実行とサイドチャネルはレイアウトのランダム化に対する脅威として認識される。
我々は、サイドチャネルと投機的実行を使用できる攻撃者に対してカーネルの安全性を復元できず、新しい条件を導入し、Spectre時代においてカーネルの安全性を正式に証明できることを示した。
この条件下では,レイアウトのランダム化に頼らずに安全であることを示す。
我々はまた、我々の状態が賢明に弱まることを示し、Spectre時代の安全なシステムコールに対するカーネルの安全性を保証するための強制機構につながった。
関連論文リスト
- The Illusion of Randomness: An Empirical Analysis of Address Space Layout Randomization Implementations [4.939948478457799]
アドレス空間レイアウトランダム化の現実の実装は不完全であり、攻撃者が悪用できる弱点を負う。
この研究は、LinuxやWindowsを含む主要なデスクトッププラットフォームにおけるASLRの有効性を評価する。
我々は,Linux 5.18以降のライブラリのエントロピーの大幅なエントロピー削減と,攻撃者が利用複雑性を著しく低減するために活用できる相関パスの同定を行う。
論文 参考訳(メタデータ) (2024-08-27T14:46:04Z) - Jailbreaking as a Reward Misspecification Problem [80.52431374743998]
本稿では,この脆弱性をアライメントプロセス中に不特定性に対処する新たな視点を提案する。
本稿では,報酬の相違の程度を定量化し,その有効性を実証する指標ReGapを紹介する。
ReMissは、報酬ミスの空間で敵のプロンプトを生成する自動レッドチームリングシステムである。
論文 参考訳(メタデータ) (2024-06-20T15:12:27Z) - Bridging the Gap: Automated Analysis of Sancus [2.045495982086173]
本研究では,サンクスの組込みセキュリティアーキテクチャにおけるこのギャップを減らすための新しい手法を提案する。
我々の手法は、与えられた脅威モデルにおける攻撃を見つけるか、システムのセキュリティに対する確率的保証を与える。
論文 参考訳(メタデータ) (2024-04-15T07:26:36Z) - Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
問題を非現実的な仮定にシフトすることなく,スケーラブルな形式検証アルゴリズムを開発する。
問題を非現実的な仮定にシフトさせることなく,スケーラブルな形式検証アルゴリズムを開発するためには,バリア証明書の概念を用いる。
本稿では,2乗法最適化とガウス過程エンベロープを用いて効率よくプログラムを解く方法を示す。
論文 参考訳(メタデータ) (2024-03-15T17:32:02Z) - Citadel: Real-World Hardware-Software Contracts for Secure Enclaves Through Microarchitectural Isolation and Controlled Speculation [8.414722884952525]
セキュアなエンクレーブのようなハードウェアアイソレーションプリミティブは、プログラムを保護することを目的としているが、一時的な実行攻撃には弱いままである。
本稿では,マイクロアーキテクチャの分離プリミティブと制御された投機機構をプロセッサに組み込むことを提唱する。
命令外プロセッサにおいて、エンクレーブと信頼できないOS間でメモリを安全に共有する2つのメカニズムを導入する。
論文 参考訳(メタデータ) (2023-06-26T17:51:23Z) - SafeDiffuser: Safe Planning with Diffusion Probabilistic Models [97.80042457099718]
拡散モデルに基づくアプローチは、データ駆動計画において有望であるが、安全保証はない。
我々は,拡散確率モデルが仕様を満たすことを保証するために,SafeDiffuserと呼ばれる新しい手法を提案する。
提案手法は,迷路経路の生成,足歩行ロボットの移動,空間操作など,安全な計画作業の一連のテストを行う。
論文 参考訳(メタデータ) (2023-05-31T19:38:12Z) - Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal
Abstractions [59.605246463200736]
雑音分布の明示的な表現に依存しない新しい制御器合成法を提案する。
まず、連続制御系を有限状態モデルに抽象化し、離散状態間の確率的遷移によってノイズを捕捉する。
我々は最先端の検証技術を用いてマルコフ決定プロセスの間隔を保証し、これらの保証が元の制御システムに受け継がれるコントローラを演算する。
論文 参考訳(メタデータ) (2023-01-04T10:40:30Z) - Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。
次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。
これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
論文 参考訳(メタデータ) (2022-08-23T05:02:09Z) - Meta-Learning Hypothesis Spaces for Sequential Decision-making [79.73213540203389]
オフラインデータ(Meta-KeL)からカーネルをメタ学習することを提案する。
穏やかな条件下では、推定されたRKHSが有効な信頼セットを得られることを保証します。
また,ベイズ最適化におけるアプローチの有効性を実証的に評価した。
論文 参考訳(メタデータ) (2022-02-01T17:46:51Z) - Are We There Yet? Timing and Floating-Point Attacks on Differential Privacy Systems [18.396937775602808]
微分プライベート(DP)システムでよく用いられる雑音発生における2つの実装欠陥について検討する。
まず,浮動小数点表現攻撃に対するガウス機構の感受性について検討する。
第二に、別のチャネルに苦しむラプラスとガウスのメカニズムを個別に研究する。
論文 参考訳(メタデータ) (2021-12-10T02:57:01Z) - Sample-Efficient Safety Assurances using Conformal Prediction [57.92013073974406]
早期警戒システムは、安全でない状況が差し迫ったときに警告を提供することができる。
安全性を確実に向上させるためには、これらの警告システムは証明可能な偽陰性率を持つべきである。
本稿では,共形予測と呼ばれる統計的推論手法とロボット・環境力学シミュレータを組み合わせたフレームワークを提案する。
論文 参考訳(メタデータ) (2021-09-28T23:00:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。