SpecIBT: Formally Verified Protection Against Speculative Control-Flow Hijacking

• URL: http://arxiv.org/abs/2601.22978v1
• Date: Fri, 30 Jan 2026 13:42:43 GMT
• Title: SpecIBT: Formally Verified Protection Against Speculative Control-Flow Hijacking
• Authors: Jonathan Baumann, Yonghyun Kim, Yan Farba, Catalin Hritcu, Julay Leatherman-Brooks,
• Abstract summary: SpecIBT is a formally verified defense against Spectre BTB, RSB, and PHT.<n>It combines CET-style hardware-assisted control-flow integrity with compiler-inserted speculative load hardening.
• Score: 2.684996629761352
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper introduces SpecIBT, a formally verified defense against Spectre BTB, RSB, and PHT that combines CET-style hardware-assisted control-flow integrity with compiler-inserted speculative load hardening (SLH). SpecIBT is based on the novel observation that in the presence of CET-style protection, we can precisely detect BTB misspeculation for indirect calls and set the SLH misspeculation flag. We formalize SpecIBT as a transformation in Rocq and provide a machine-checked proof that it achieves relative security: any transformed program running with speculation leaks no more than what the source program leaks without speculation. This strong security guarantee applies to arbitrary programs, even those not following the cryptographic constant-time programming discipline.

Related papers

• Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
  We propose an unsupervised conformal inference framework for generation.<n>Our gates achieve close-to-nominal coverage and provide tighter, more stable thresholds than split UCP.<n>The result is a label-free, API-compatible gate for test-time filtering.
  arXiv  Detail & Related papers  (2025-09-26T23:40:47Z)
• Can One Safety Loop Guard Them All? Agentic Guard Rails for Federated Computing [0.0]
  We propose Guardian-FC, a novel framework for privacy preserving federated computing.<n>It unifies safety enforcement across diverse privacy preserving mechanisms.<n>We present qualitative scenarios illustrating backend-agnostic safety and a formal model foundation for verification.
  arXiv  Detail & Related papers  (2025-06-24T20:39:49Z)
• Exploiting Inaccurate Branch History in Side-Channel Attacks [54.218160467764086]
  This paper examines how resource sharing and contention affect two widely implemented but underdocumented features: Bias-Free Branch Prediction and Branch History Speculation.<n>We show that these features can inadvertently modify the Branch History Buffer (BHB) update behavior and create new primitives that trigger malicious mis-speculations.<n>We present three novel attack primitives: two Spectre attacks, namely Spectre-BSE and Spectre-BHS, and a cross-privilege control flow side-channel attack called BiasScope.
  arXiv  Detail & Related papers  (2025-06-08T19:46:43Z)
• CANTXSec: A Deterministic Intrusion Detection and Prevention System for CAN Bus Monitoring ECU Activations [53.036288487863786]
  We propose CANTXSec, the first deterministic Intrusion Detection and Prevention system based on physical ECU activations.<n>It detects and prevents classical attacks in the CAN bus, while detecting advanced attacks that have been less investigated in the literature.<n>We prove the effectiveness of our solution on a physical testbed, where we achieve 100% detection accuracy in both classes of attacks while preventing 100% of FIAs.
  arXiv  Detail & Related papers  (2025-05-14T13:37:07Z)
• FSLH: Flexible Mechanized Speculative Load Hardening [0.1398098625978622]
  The Spectre speculative side-channel attacks pose formidable threats for security.<n>Research has shown that code following the cryptographic constant-time discipline can be efficiently protected against Spectre v1.<n>We introduce a flexible SLH notion that achieves the best of both worlds by generalizing both Selective and Ultimate SLH.
  arXiv  Detail & Related papers  (2025-02-05T14:23:43Z)
• Secure Software/Hardware Hybrid In-Field Testing for System-on-Chip [0.0]
  Modern Systems-on-Chips (SoCs) incorporate built-in self-test (BIST) modules deeply integrated into the device's intellectual property (IP) blocks.<n>BIST results potentially reveal the internal structure and state of the device under test (DUT) and hence open attack vectors.<n>So-called result compaction can overcome this vulnerability by hiding the BIST chain structure but introduces the issues of aliasing and invalid signatures.<n>We introduce a low-overhead software/ hardware hybrid approach that overcomes the mentioned limitations.
  arXiv  Detail & Related papers  (2024-10-07T15:04:37Z)
• 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)
• Coding-Based Hybrid Post-Quantum Cryptosystem for Non-Uniform Information [53.85237314348328]
  We introduce for non-uniform messages a novel hybrid universal network coding cryptosystem (NU-HUNCC) We show that NU-HUNCC is information-theoretic individually secured against an eavesdropper with access to any subset of the links.
  arXiv  Detail & Related papers  (2024-02-13T12:12:39Z)
• 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)
• Tamper-Evident Pairing [55.2480439325792]
  Tamper-Evident Pairing (TEP) is an improvement of the Push-Button configuration (PBC) standard. TEP relies on the Tamper-Evident Announcement (TEA), which guarantees that an adversary can neither tamper a transmitted message without being detected, nor hide the fact that the message has been sent. This paper provides a comprehensive overview of the TEP protocol, including all information needed to understand how it works.
  arXiv  Detail & Related papers  (2023-11-24T18:54:00Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  We construct the first fully homomorphic encryption scheme with certified deletion. Our main technical ingredient is an interactive protocol by which a quantum prover can convince a classical verifier that a sample from the Learning with Errors distribution in the form of a quantum state was deleted.
  arXiv  Detail & Related papers  (2022-03-03T10:07:32Z)

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.