SCHERI: Provably Secure Speculation Under the Constant-Time Policy for CHERI (Extended Version)

• URL: http://arxiv.org/abs/2609.17399v1
• Date: Tue, 15 Sep 2026 16:33:45 GMT
• Title: SCHERI: Provably Secure Speculation Under the Constant-Time Policy for CHERI (Extended Version)
• Abstract summary: We show that providing secure speculation for CHERI is non-trivial, and that existing proposals fail to preserve the confidentiality guarantees.<n>We present SCHERI, a new processor design within this framework, and formally prove that it provides end-to-end secure speculation guarantees for the constant-time policy.
• Score: 9.43713777107964
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Capability-based architectures such as CHERI provide strong support for the architectural isolation of software components. To additionally protect against microarchitectural leakage, software can be written in a constant-time fashion. Modern processors, however, rely heavily on speculative execution, which can invalidate the constant-time guarantees and leak isolated secrets transiently. In this work, we show that providing secure speculation for CHERI is non-trivial, and that existing proposals fail to preserve the confidentiality guarantees. We develop a formal framework for reasoning jointly about capability safety, speculative execution, and information-flow security, and use it to demonstrate potential leaks. We then present SCHERI, a new processor design within this framework, and formally prove that it provides end-to-end secure speculation guarantees for the constant-time policy. Our results provide formal foundations and practical guidance for building future capability-based processors, which are resilient to Spectre attacks for constant-time programs.

Related papers

• SeClaw: Spec-Driven Security Task Synthesis for Evaluating Autonomous Agents [87.26967184869198]
  SeClaw is a framework that combines specification-driven security task synthesis with execution-based security evaluation for Autonomous agents.<n> benchmark covers risks arising from resources, user tasks, environments, and intrinsic agent behaviors.
  arXiv  Detail & Related papers  (2026-06-01T14:23:42Z)
• Provably Secure Agent Guardrail [89.79561918065122]
  Existing defense architectures rely on empirical semantic guardrails and probabilistic large model adjudicators.<n>This paper proposes a new security paradigm for agents based on the fundamental limitations of logical reasoning.
  arXiv  Detail & Related papers  (2026-05-28T02:12:41Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• CaMeLs Can Use Computers Too: System-level Security for Computer Use Agents [60.98294016925157]
  AI agents are vulnerable to prompt injection attacks, where malicious content hijacks agent behavior to steal credentials or cause financial loss.<n>We introduce Single-Shot Planning for CUAs, where a trusted planner generates a complete execution graph with conditional branches before any observation of potentially malicious content.<n>Although this architectural isolation successfully prevents instruction injections, we show that additional measures are needed to prevent Branch Steering attacks.
  arXiv  Detail & Related papers  (2026-01-14T23:06:35Z)
• Towards Verifiably Safe Tool Use for LLM Agents [53.55621104327779]
  Large language model (LLM)-based AI agents extend capabilities by enabling access to tools such as data sources, APIs, search engines, code sandboxes, and even other agents.<n>LLMs may invoke unintended tool interactions and introduce risks, such as leaking sensitive data or overwriting critical records.<n>Current approaches to mitigate these risks, such as model-based safeguards, enhance agents' reliability but cannot guarantee system safety.
  arXiv  Detail & Related papers  (2026-01-12T21:31:38Z)
• TICAL: Trusted and Integrity-protected Compilation of AppLications [0.24919281650930603]
  Tical is a framework for trusted compilation that provides integrity protection and confidentiality in build pipelines from source code to the final executable.<n>Our approach harnesses TEEs as runtime protection but enriches TEEs with file system shielding and an immutable audit log with version history to provide accountability.<n>Our evaluation shows that Tical can protect the confidentiality and integrity of whole CI/CD pipelines with an acceptable performance overhead.
  arXiv  Detail & Related papers  (2025-11-21T09:19:41Z)
• Performance and Storage Analysis of CRYSTALS Kyber as a Post Quantum Replacement for RSA and ECC [45.88028371034407]
  CRYSTALS-Kyber is a post-quantum cryptographic solution standardized by NIST in 2022.<n>This study evaluates Kyber's practical viability through performance testing across various implementation schemes.
  arXiv  Detail & Related papers  (2025-08-03T09:53:45Z)
• Security Enclave Architecture for Heterogeneous Security Primitives for Supply-Chain Attacks [7.9837065464150685]
  This paper explores the range of obstacles encountered when building a unified security architecture capable of addressing multiple attack vectors.<n>We present a thorough evaluation of its impact on silicon area and power consumption across various ASIC technologies.
  arXiv  Detail & Related papers  (2025-07-15T04:28:02Z)
• VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL [4.652188875442064]
  CHERI provides and enforces fine-grained memory protection directly in the hardware. VeriCHERI is conceptionally different from previous works in that it does not require any ISA specification. We demonstrate the effectiveness and scalability of VeriCHERI on a RISC-V based processor implementing a CHERI variant.
  arXiv  Detail & Related papers  (2024-07-26T11:48:55Z)
• HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
  Confidential computing enables the protection of confidential code and data in a co-tenanted cloud deployment using specialized hardware isolation units called Trusted Execution Environments (TEEs) TEEs offer low-level C/C++-based toolchains that are susceptible to inherent memory safety vulnerabilities and lack language constructs to monitor explicit and implicit information-flow leaks. We address the above with HasTEE+, a domain-specific language (cla) embedded in Haskell that enables programming TEEs in a high-level language with strong type-safety.
  arXiv  Detail & Related papers  (2024-01-17T00:56:23Z)
• DECLASSIFLOW: A Static Analysis for Modeling Non-Speculative Knowledge to Relax Speculative Execution Security Measures (Full Version) [9.816078445230305]
  Speculative execution attacks undermine the security of constant-time programming. This paper proposes DECLASSIFLOW to efficiently protect constant-time code from speculative leakage.
  arXiv  Detail & Related papers  (2023-12-14T21:00:20Z)
• Systematic Prevention of On-Core Timing Channels by Full Temporal Partitioning [13.313360308792198]
  We introduce the temporal fence instruction fence.t, which provides the required mechanisms by clearing vulnerable microarchitectural state.<n>We implement fence.t on an experimental version of the seL4 microkernel and CVA6, an open-source, in-order, application class, 64-bit RISC-V core.<n>We find that a complete, systematic, ISA-supported erasure of all non-architectural core components is the most effective implementation.
  arXiv  Detail & Related papers  (2022-02-24T11:17:34Z)

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.