On Kernel's Safety in the Spectre Era (Extended Version)

• URL: http://arxiv.org/abs/2406.07278v1
• Date: Tue, 11 Jun 2024 14:04:58 GMT
• Title: On Kernel's Safety in the Spectre Era (Extended Version)
• Authors: Davide Davoli, Martin Avanzini, Tamara Rezk,
• Abstract summary: We show that layout randomization offers a comparable safety guarantee in a system with memory separation. We show that kernel safety cannot be restored for attackers capable of using side-channels and speculative execution. Our research demonstrates that under this condition, the system remains safe without relying on layout randomization.
• Score: 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.

Related papers

• Comprehensive Kernel Safety in the Spectre Era: Mitigations and Performance Evaluation (Extended Version) [2.0436753359071913]
  We show that layout randomization offers a comparable safety guarantee in a system with memory separation. We show that kernel safety cannot be restored for attackers capable of using side-channels and speculative execution. We introduce enforcement mechanisms that can guarantee speculative kernel safety for safe system calls in the Spectre era.
  arXiv  Detail & Related papers  (2024-11-27T07:06:28Z)
• The Illusion of Randomness: An Empirical Analysis of Address Space Layout Randomization Implementations [4.939948478457799]
  Real-world implementations of Address Space Layout Randomization are imperfect and subject to weaknesses that attackers can exploit. This work evaluates the effectiveness of ASLR on major desktop platforms, including Linux, and Windows. We find a significant entropy reduction in the entropy of libraries after the Linux 5.18 version and identify correlation paths that an attacker could leverage to reduce exploitation complexity significantly.
  arXiv  Detail & Related papers  (2024-08-27T14:46:04Z)
• Jailbreaking as a Reward Misspecification Problem [80.52431374743998]
  We propose a novel perspective that attributes this vulnerability to reward misspecification during the alignment process. We introduce a metric ReGap to quantify the extent of reward misspecification and demonstrate its effectiveness. We present ReMiss, a system for automated red teaming that generates adversarial prompts in a reward-misspecified space.
  arXiv  Detail & Related papers  (2024-06-20T15:12:27Z)
• Bridging the Gap: Automated Analysis of Sancus [2.045495982086173]
  We propose a new method to reduce this gap in the Sancus embedded security architecture. Our method either finds attacks in the given threat model or gives probabilistic guarantees on the security of the system.
  arXiv  Detail & Related papers  (2024-04-15T07:26:36Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  We develop scalable formal verification algorithms without shifting the problem to unrealistic assumptions. In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates. We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope.
  arXiv  Detail & Related papers  (2024-03-15T17:32:02Z)
• Citadel: Simple Spectre-Safe Isolation For Real-World Programs That Share Memory [8.414722884952525]
  We introduce a new security property we call relaxed microarchitectural isolation (RMI) RMI allows sensitive programs that are not-constant-time to share memory with an attacker while restricting the information leakage to that of non-speculative execution. Our end-to-end prototype, Citadel, consists of an FPGA-based multicore processor that boots Linux and runs secure applications.
  arXiv  Detail & Related papers  (2023-06-26T17:51:23Z)
• SafeDiffuser: Safe Planning with Diffusion Probabilistic Models [97.80042457099718]
  Diffusion model-based approaches have shown promise in data-driven planning, but there are no safety guarantees. We propose a new method, called SafeDiffuser, to ensure diffusion probabilistic models satisfy specifications. We test our method on a series of safe planning tasks, including maze path generation, legged robot locomotion, and 3D space manipulation.
  arXiv  Detail & Related papers  (2023-05-31T19:38:12Z)
• Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions [59.605246463200736]
  We present a novel controller synthesis method that does not rely on any explicit representation of the noise distributions. First, we abstract the continuous control system into a finite-state model that captures noise by probabilistic transitions between discrete states. We use state-of-the-art verification techniques to provide guarantees on the interval Markov decision process and compute a controller for which these guarantees carry over to the original control system.
  arXiv  Detail & Related papers  (2023-01-04T10:40:30Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers. We then present the pointwise feasibility conditions of the resulting safety controller. We use these conditions to devise an event-triggered online data collection strategy.
  arXiv  Detail & Related papers  (2022-08-23T05:02:09Z)
• Meta-Learning Hypothesis Spaces for Sequential Decision-making [79.73213540203389]
  We propose to meta-learn a kernel from offline data (Meta-KeL) Under mild conditions, we guarantee that our estimated RKHS yields valid confidence sets. We also empirically evaluate the effectiveness of our approach on a Bayesian optimization task.
  arXiv  Detail & Related papers  (2022-02-01T17:46:51Z)
• Sample-Efficient Safety Assurances using Conformal Prediction [57.92013073974406]
  Early warning systems can provide alerts when an unsafe situation is imminent. To reliably improve safety, these warning systems should have a provable false negative rate. We present a framework that combines a statistical inference technique known as conformal prediction with a simulator of robot/environment dynamics.
  arXiv  Detail & Related papers  (2021-09-28T23:00:30Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.