Detecting speculative leaks with compositional semantics

• URL: http://arxiv.org/abs/2603.29800v1
• Date: Tue, 31 Mar 2026 14:32:12 GMT
• Title: Detecting speculative leaks with compositional semantics
• Abstract summary: We propose a novel framework for detecting information flows introduced by speculative execution and reasoning about software defenses.<n>We develop Spectector, a symbolic analysis tool that uses our compositional framework and leverages SMT solvers to detect vulnerabilities and verify program security.
• Score: 9.009704721347575
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Speculative execution enhances processor performance by predicting intermediate results and executing instructions based on these predictions. However, incorrect predictions can lead to security vulnerabilities, as speculative instructions leave traces in microarchitectural components that attackers can exploit. This is demonstrated by the family of Spectre attacks. Unfortunately, existing countermeasures to these attacks lack a formal security characterization, making it difficult to verify their effectiveness. In this paper, we propose a novel framework for detecting information flows introduced by speculative execution and reasoning about software defenses. The theoretical foundation of our approach is speculative non-interference (SNI), a novel semantic notion of security against speculative execution attacks. SNI relates information leakage observed under a standard non-speculative semantics to leakage arising under semantics that explicitly model speculative execution. To capture their combined effects, we extend our framework with a mechanism to safely compose multiple speculative semantics, each focussing on a single aspect of speculation. This allows us to analyze the complex interactions and resulting leaks that can arise when multiple speculative mechanisms operate together. On the practical side, we develop Spectector, a symbolic analysis tool that uses our compositional framework and leverages SMT solvers to detect vulnerabilities and verify program security with respect to multiple speculation mechanisms. We demonstrate the effectiveness of Spectector through evaluations on standard security benchmarks and new vulnerability scenarios.

Related papers

• AI Slop and Hallucinations in Vulnerability Assessment: A Survey on Reasoning Failures and Trustworthy Mitigation [48.55515767840701]
  "AI slop" is artifacts, hallucinated vulnerabilities, plausible but incorrect patches, and semantically repackaged bug reports.<n>This paper surveys the empirical evidence, identifies a unifying mechanism, and traces a path toward trustworthy triage.
  arXiv  Detail & Related papers  (2026-08-26T11:48:38Z)
• Beyond Runtime Enforcement: Shield Synthesis as Defensibility Analysis for Adversarial Networks [0.0]
  Shielded reinforcement learning is typically presented as a runtime safety mechanism that compiles temporal-logic specifications into automata restricting an agent's actions.<n>We instantiate this through a constrained two-player safety game for network defense.<n>We derive topology-level metrics from the attractor structure and combine them with post-convergence behavior from shield-constrained adversarial multi-agent reinforcement learning.
  arXiv  Detail & Related papers  (2026-06-11T17:35:40Z)
• Who Pays the Price? Stakeholder-Centric Prompt Injection Benchmarking for Real-world Web Agents [93.19140872946842]
  Web agents driven by large language models (LLMs) are increasingly deployed in real-world environments.<n>This makes them vulnerable to prompt-injection attacks, in which seemingly benign content embeds adversarial instructions that manipulate agent behaviour.<n>We introduce textbfsysname, a benchmark to systematically categorize and attribute harm in real-world web agent systems.
  arXiv  Detail & Related papers  (2026-06-11T14:12:43Z)
• 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)
• Provable Robustness against Backdoor Attacks via the Primal-Dual Perspective on Differential Privacy [51.758416625168]
  Randomized smoothing is a powerful tool for certifying robustness to adversarial perturbations.<n>We propose a framework for certification of complex, composed mechanisms.<n>We provide a principled and general framework for using composite mechanisms to certify robustness under complex threat models.
  arXiv  Detail & Related papers  (2026-05-20T22:17:29Z)
• VIGIL: Defending LLM Agents Against Tool Stream Injection via Verify-Before-Commit [44.24310459184061]
  LLM agents operating in open environments face escalating risks from indirect prompt injection.<n>We propose textbfVIGIL, a framework that shifts the paradigm from restrictive isolation to a verify-before-commit protocol.
  arXiv  Detail & Related papers  (2026-01-09T12:19:49Z)
• Servant, Stalker, Predator: How An Honest, Helpful, And Harmless (3H) Agent Unlocks Adversarial Skills [3.0620527758972496]
  This paper identifies and analyzes a novel vulnerability class in Model Context Protocol based agent systems.<n>The attack chain describes and demonstrates how benign, individually authorized tasks can be orchestrated to produce harmful emergent behaviors.
  arXiv  Detail & Related papers  (2025-08-27T01:11:59Z)
• A Survey on Model Extraction Attacks and Defenses for Large Language Models [55.60375624503877]
  Model extraction attacks pose significant security threats to deployed language models.<n>This survey provides a comprehensive taxonomy of extraction attacks and defenses, categorizing attacks into functionality extraction, training data extraction, and prompt-targeted attacks.<n>We examine defense mechanisms organized into model protection, data privacy protection, and prompt-targeted strategies, evaluating their effectiveness across different deployment scenarios.
  arXiv  Detail & Related papers  (2025-06-26T22:02:01Z)
• 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)
• Detecting speculative data flow vulnerabilities using weakest precondition reasoning [4.713817702376467]
  We introduce an approach for detecting the data flow vulnerabilities, Spectre-STL and Spectre-PSF, using weakest precondition reasoning.<n>We validate our approach on a suite of litmus tests used to validate related approaches in the literature.
  arXiv  Detail & Related papers  (2025-04-27T07:02:15Z)
• Jailbreaking as a Reward Misspecification Problem [80.52431374743998]
  We propose a novel perspective that attributes this vulnerability to reward misspecification during the alignment process.<n>We introduce a metric ReGap to quantify the extent of reward misspecification and demonstrate its effectiveness.<n>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)
• Kick Bad Guys Out! Conditionally Activated Anomaly Detection in Federated Learning with Zero-Knowledge Proof Verification [31.38942054994932]
  Federated Learning (FL) systems are susceptible to adversarial attacks.<n>RedJasper is a two-staged anomaly detection method specifically designed for real-world FL deployments.<n>It identifies suspicious activities in the first stage, then activates the second stage conditionally to further scrutinize the suspicious local models.
  arXiv  Detail & Related papers  (2023-10-06T07:09:05Z)
• DRSM: De-Randomized Smoothing on Malware Classifier Providing Certified Robustness [58.23214712926585]
  We develop a certified defense, DRSM (De-Randomized Smoothed MalConv), by redesigning the de-randomized smoothing technique for the domain of malware detection. Specifically, we propose a window ablation scheme to provably limit the impact of adversarial bytes while maximally preserving local structures of the executables. We are the first to offer certified robustness in the realm of static detection of malware executables.
  arXiv  Detail & Related papers  (2023-03-20T17:25:22Z)
• Short Paper: Static and Microarchitectural ML-Based Approaches For Detecting Spectre Vulnerabilities and Attacks [0.0]
  Spectre intrusions exploit speculative execution design vulnerabilities in modern processors. Current state-of-the-art detection techniques utilize micro-architectural features or vulnerable speculative code to detect these threats. We present the first comprehensive evaluation of static and microarchitectural analysis-assisted machine learning approaches to detect Spectre vulnerabilities.
  arXiv  Detail & Related papers  (2022-10-26T03:55:39Z)
• Proper Network Interpretability Helps Adversarial Robustness in Classification [91.39031895064223]
  We show that with a proper measurement of interpretation, it is difficult to prevent prediction-evasion adversarial attacks from causing interpretation discrepancy. We develop an interpretability-aware defensive scheme built only on promoting robust interpretation. We show that our defense achieves both robust classification and robust interpretation, outperforming state-of-the-art adversarial training methods against attacks of large perturbation.
  arXiv  Detail & Related papers  (2020-06-26T01:31:31Z)

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.