Mythos and the Unverified Cage: Z3-Based Pre-Deployment Verification for Frontier-Model Sandbox Infrastructure

• URL: http://arxiv.org/abs/2604.20496v1
• Date: Wed, 22 Apr 2026 12:28:23 GMT
• Title: Mythos and the Unverified Cage: Z3-Based Pre-Deployment Verification for Frontier-Model Sandbox Infrastructure
• Abstract summary: Anthropic has not publicly characterized the escape vector; some secondary accounts hypothesize a CWE-190 arithmetic vulnerability in sandbox networking code.<n>This paper presents COBALT, a Z3 SMT-based formal verification engine for identifying CWE-190/191/195 arithmetic vulnerability patterns in C/C++ infrastructure prior to deployment.<n>Proposed: a four-layer containment framework consisting of COBALT, VERDICT, DIRECTIVE-4, and SENTINEL, mapping pre-deployment verification, pre-execution constraints, output control, and runtime monitoring to the failure modes exposed by the Mythos incident.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The April 2026 Claude Mythos sandbox escape exposed a critical weakness in frontier AI containment: the infrastructure surrounding advanced models remains susceptible to formally characterizable arithmetic vulnerabilities. Anthropic has not publicly characterized the escape vector; some secondary accounts hypothesize a CWE-190 arithmetic vulnerability in sandbox networking code. We treat this as unverified and analyze the vulnerability class rather than the specific escape. This paper presents COBALT, a Z3 SMT-based formal verification engine for identifying CWE-190/191/195 arithmetic vulnerability patterns in C/C++ infrastructure prior to deployment. We distinguish two classes of contribution. Validated: COBALT detects arithmetic vulnerability patterns in production codebases, producing SAT verdicts with concrete witnesses and UNSAT guarantees under explicit safety bounds. We demonstrate this on four production case studies: NASA cFE, wolfSSL, Eclipse Mosquitto, and NASA F Prime, with reproducible encodings, verified solver output, and acknowledged security outcomes. Proposed: a four-layer containment framework consisting of COBALT, VERDICT, DIRECTIVE-4, and SENTINEL, mapping pre-deployment verification, pre-execution constraints, output control, and runtime monitoring to the failure modes exposed by the Mythos incident. Under explicit assumptions, we further argue that the publicly reported Mythos escape class is consistent with a Z3-expressible CWE-190 arithmetic formulation and that pre-deployment formal analysis would have been capable of surfacing the relevant pattern. The broader claim is infrastructural: frontier-model safety cannot depend on behavioral safeguards alone; the containment stack itself must be subjected to formal verification.

Related papers

• Evaluating the NIST Bugs Framework Against CWE as a Successor for Automated Vulnerability Classification [8.57966523475548]
  The Bugs Framework (BF) organizes vulnerabilities into cause, operation, consequence> triples and links such triples into a causal chain.<n>We evaluate the claim that BF is a more structured and automation-friendly framework than the Common Weaknession (CWE)<n>Our exploration reveals specific gaps in BF, including under-specified guidance on availability.
  arXiv  Detail & Related papers  (2026-09-14T23:18:46Z)
• 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)
• CyberFactory: Scaling Cyber Security Capabilities with Instances from the Wild [49.44069582581181]
  CyberFactory transforms public vulnerability artifacts, including CVEs from the wild, into executable and verifiable task instances.<n>It uses a reusable vulnerability-analysis skill to guide the teacher through source inspection, problem solving with domain prior, and evidence-based validation.<n>On CyberGym, modelname reaches 52.4% Pass@1 under a one-hour budget, improving over its Qwen3.5 base model by +22.8 points.
  arXiv  Detail & Related papers  (2026-08-24T12:30:10Z)
• SafeCA: Safe Cross-Attention Localization and Regulation for Text-to-Video Jailbreak Defense [77.70598852234149]
  Text-to-Video (T2V) generative models are vulnerable to jailbreak attacks in real-world deployment.<n>We propose SafeCA, a feature-level defense mechanism for safe cross-attention localization and regularization.<n> Experimental results show that SafeCA reduces the jailbreak success rate by about 20% on mainstream T2V models.
  arXiv  Detail & Related papers  (2026-08-11T14:01:24Z)
• Crushing the Evidence: A Dual-Penalty Evasion Framework for Fooling White-Box Explainable AI Auditors [4.377640147713394]
  Post-hoc model explainers are widely deployed to audit models in high-stakes sensitive domains.<n>A few studies have examined potential attacks in the explainability pipeline.<n>We introduce a more potent white-box, gradient-regularized evasion attack framework.
  arXiv  Detail & Related papers  (2026-08-01T10:03:14Z)
• Routing Ceilings Are Domain-Independent: Structural Prior Injection in Code Security Vulnerability Detection [0.0]
  Large language models (LLMs) exhibit a well-documented gap between latent capability and consistent activation.<n>Prior work reports that structural priors raise in-distribution performance dramatically, yet collapse below the zero-shot baseline out-of-distribution.<n>We test whether this phenomenon is cross-domain by reproducing the SAIR design in source-code security vulnerability detection.
  arXiv  Detail & Related papers  (2026-07-16T06:45:08Z)
• Understanding and Mitigating Prompt Leaking Attacks in Real-World LLM-Based Applications [57.33208520608409]
  This paper presents a systematic study of prompt leaking in large language model (LLM)-based applications.<n>We find that over 80% of deployments leak system prompts under realistic adversarial queries.<n>We propose AREA, a practical defense that re-anchors the model's attention using an optimizable soft prompt.
  arXiv  Detail & Related papers  (2026-06-17T04:20:00Z)
• MOSAIC-Bench: Measuring Compositional Vulnerability Induction in Coding Agents [2.1942030377331245]
  Coding agents often pass per-prompt safety review yet ship exploitable code when their tasks are decomposed into routine engineering tickets.<n>We introduce MOSAIC-Bench, a benchmark of 199 three-stage attack chains paired with deterministic exploit oracles on deployed software substrates.<n>We show that nine production coding agents compose innocuous tickets at 53-86% end-to-end ASR with only two refusals across all staged runs.
  arXiv  Detail & Related papers  (2026-05-05T16:38:23Z)
• Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
  Safety-aligned large language models (LLMs) are increasingly deployed in real-world pipelines.<n> adversaries can distribute backdoored checkpoints that behave normally under standard evaluation but jailbreak when a hidden trigger is present.<n>Recent post-hoc weight-editing methods offer an efficient approach to injecting such backdoors.
  arXiv  Detail & Related papers  (2026-04-14T06:48:33Z)
• The Compliance Paradox: Semantic-Instruction Decoupling in Automated Academic Code Evaluation [11.984098021215878]
  We introduce the Semantic-Preserving Adrial Code Injection (SPACI) Framework and the Abstract Syntax Tree-Aware Semantic Injection Protocol (AST-ASIP)<n>These methods exploit the Syntax-Semantics Gap by embedding adversarial directives into syntactically inert regions (trivia nodes) of the Abstract Syntax Tree.<n>Through a large-scale evaluation of 9 SOTA models across 25,000 submissions in Python, C, C++, and Java, we reveal catastrophic failure rates (>95%) in high-capacity open-weights models like DeepSeek-V3.
  arXiv  Detail & Related papers  (2026-01-29T07:40:58Z)
• Why Does the LLM Stop Computing: An Empirical Study of User-Reported Failures in Open-Source LLMs [50.075587392477935]
  We conduct the first large-scale empirical study of 705 real-world failures from the open-source DeepSeek, Llama, and Qwen ecosystems.<n>Our analysis reveals a paradigm shift: white-box orchestration relocates the reliability bottleneck from model algorithmic defects to the systemic fragility of the deployment stack.
  arXiv  Detail & Related papers  (2026-01-20T06:42:56Z)
• The Trojan Knowledge: Bypassing Commercial LLM Guardrails via Harmless Prompt Weaving and Adaptive Tree Search [58.8834056209347]
  Large language models (LLMs) remain vulnerable to jailbreak attacks that bypass safety guardrails to elicit harmful outputs.<n>We introduce the Correlated Knowledge Attack Agent (CKA-Agent), a dynamic framework that reframes jailbreaking as an adaptive, tree-structured exploration of the target model's knowledge base.
  arXiv  Detail & Related papers  (2025-12-01T07:05:23Z)
• ARMOR: Aligning Secure and Safe Large Language Models via Meticulous Reasoning [64.32925552574115]
  ARMOR is a large language model that analyzes jailbreak strategies and extracts the core intent.<n> ARMOR achieves state-of-the-art safety performance, with an average harmful rate of 0.002 and an attack success rate of 0.06 against advanced optimization-based jailbreaks.
  arXiv  Detail & Related papers  (2025-07-14T09:05:54Z)
• AdversariaL attacK sAfety aLIgnment(ALKALI): Safeguarding LLMs through GRACE: Geometric Representation-Aware Contrastive Enhancement- Introducing Adversarial Vulnerability Quality Index (AVQI) [21.209413521884297]
  Adversarial threats against LLMs are escalating faster than current defenses can adapt.<n>We introduce ALKALI, the first rigorously curated adversarial benchmark.<n>We introduce GRACE, an alignment framework coupling preference learning with latent space regularization.
  arXiv  Detail & Related papers  (2025-06-10T15:14:17Z)
• CRAFT: Characterizing and Root-Causing Fault Injection Threats at Pre-Silicon [3.6158033114580674]
  Fault injection attacks pose significant security threats to embedded systems.<n>Early detection and understanding of how physical faults propagate to system-level behavior are essential to safeguarding cyberinfrastructure.<n>This work introduces CRAFT, a framework that combines pre-silicon analysis with post-silicon validation to systematically uncover and analyze fault injection vulnerabilities.
  arXiv  Detail & Related papers  (2025-03-05T20:17:46Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  Large language models (LLMs) are increasingly integrated into real-world personalized applications.<n>The valuable and often proprietary nature of the knowledge bases used in RAG introduces the risk of unauthorized usage by adversaries.<n>Existing methods that can be generalized as watermarking techniques to protect these knowledge bases typically involve poisoning or backdoor attacks.<n>We propose name for harmless' copyright protection of knowledge bases.
  arXiv  Detail & Related papers  (2025-02-10T09:15:56Z)

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.