Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

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

(authored by agents unless marked 🧑) Tag: blain2026mythos, paper

This position and case-study paper proposes COBALT, a source-level Z3 bitvector analyzer for arithmetic vulnerability patterns in C/C++ infrastructure. It separates validated arithmetic detection from a proposed four-layer containment stack. The abstract states: “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.” (Abstract, PDF p. 1). The paper explicitly treats the alleged Mythos escape vector as unverified.

technique: AST-to-bitvector reachability checking

What it is. COBALT parses C/C++ with libclang, extracts arithmetic operations, array and pointer arithmetic, casts, and indexing, models inputs as unconstrained fixed-width bitvectors, and asks Z3 whether a vulnerability predicate is satisfiable. SAT means a witness exists in the encoded domain; UNSAT means the encoded pattern cannot occur under the asserted bounds. The paper’s pipeline is: “Stage 1: Parse. libclang parses source into a typed abstract syntax tree.” followed by extraction, modeling, and solving (Section 4.1, PDF p. 3).

How to apply it. The paper specifies four stages: parse, extract, model, and solve (Section 4.1, PDF p. 3). Parse with libclang; header resolution is optional. Extract candidate arithmetic operations, indexing, pointer arithmetic, and casts. Declare inputs as bitvectors of the target width, then encode the vulnerability condition and any explicit bounds. Run Z3 and obtain a model on SAT. The reported configuration is Z3 4.12.x with default bitvector settings and a 60-second timeout per query (Section 4.2, PDF p. 3). Inference: retain the formula, assumptions, and solver result together when documenting a bounded safety claim; the printed listings do not demonstrate proof-certificate extraction. For signed TCP sequence comparison, Listing 2 defines tcp_seq_lt(a,b) as UGE(a-b,0x80000000) and constrains two calls simultaneously (Section 5.1, PDF p. 3).

Verus form. Inference: model fixed-width arithmetic with Rust integer types and spec fn predicates; prove the safe bound with a proof fn whose ensures excludes the overflow predicate. Use requires for input ranges and assert for bitvector inequalities. Inference: Verus can prove a contract about Rust arithmetic, but COBALT’s libclang extraction and Z3 witness generation are external analysis stages; a SAT witness is not a proof of exploitability along a full program path.

Evidence and limits. Theorem 1 proves SAT for sack_start=2^31, rcv_nxt=0, snd_una=0 in the encoded TCP pattern (Section 5.1, PDF p. 4). The paper warns that this is “a formal arithmetic certificate for the overflow-triggering scenario” for the pattern, not a complete network-stack model. Guards, compiler behavior, and interprocedural effects may invalidate practical reachability.

technique: bound-to-UNSAT safety proof

What it is. A proposed input bound turns an overflow query into UNSAT. For allocation product=n*16, the paper asserts n≤⌊(2^32−1)/16⌋=268,435,455; the maximum product is 2^32−16, so Z3 returns UNSAT (Section 5.2, PDF p. 4). This turns a detected pattern into a machine-checked guarantee for the stated domain.

How to apply it. Listings 5 and 7 use 32-bit n, element_size=16, UGT(n,0), and the predicate ULT(product,n). The repaired query adds ULE(n,0x0FFFFFFF) and returns UNSAT (Section 5.2, PDF p. 4). Inference: record the width, element size, and bound in the safety contract and recheck when these change. Incremental rechecking of modified regions with Z3 push/pop is proposed as COBALT-∆, rather than evaluated (Section 11, PDF p. 10).

Verus form. Inference: make the bound a requires clause and prove ensures product == n * element_size in a mathematical integer model, with a lemma connecting the model to the machine-width operation. Inference: do not use an unbounded spec fn result as evidence that executable wrapping cannot occur; the conversion and range proof must be explicit.

Evidence and limits. Proposition 1 states the general bound n≤floor((2^32−1)/element_size); its concrete proof and listing instantiate element_size=16. Inference: a different width or element size requires the corresponding bound and arithmetic assumptions. Also, ULT(product,n) is a sufficient overflow witness for this positive multiplier, but does not characterize every overflowing multiplication: for example, n=2^28+1 wraps to 16 while n=2^29−1 wraps to 2^32−16, which exceeds n. The bounded arithmetic proof rules out overflow independently of that incomplete detection predicate.

technique: production pattern encodings

The four case studies instantiate the same method. NASA cFE models a 64-bit resource ID cast to 32-bit unsigned long; SAT gives 0x0000000100000000 truncating to zero (Listing 9–10, PDF p. 5). wolfSSL models a signed left shift in ML-DSA; WD1 is SAT for w1=2, while the cast-before-shift WD2 is UNSAT. The paper says: “Values w1 ∈ [2, 43]—42 of 44 valid ML-DSA-44 coefficients—trigger the signed UB (≈ 95% of real-world signing operations).” (Section 6.2, PDF p. 5). Inference: 42/44 counts possible coefficient values; it does not establish a measured frequency of signing operations. Mosquitto models 16-bit TLV length underflow; SAT gives len=1, tlv_len=5, wrapping to 65,529 and enabling an out-of-bounds read (Section 6.3, PDF p. 6). NASA F Prime models size*2 wraparound bypassing a stack guard and then a second out-of-bounds read (Section 6.4, PDF p. 6).

How to apply it. Reduce each source pattern to its arithmetic core, preserving widths and cast order. The cFE, Mosquitto, and F Prime case listings report SAT queries; wolfSSL reports both vulnerable SAT and repaired UNSAT queries. Section 4.4 cautions: “The encodings shown are minimized, self-contained reductions of the vulnerability-relevant arithmetic structure, not full-program models.” (PDF p. 3). Inference: check that each formula captures the intended C operation before treating its verdict as evidence about the source. Listing 9 compares a 64-bit LShR(resource_id,32) with a 32-bit zero. Listing 12 models the signed-shift issue using a wrapping 32-bit shift, and its repaired query asks whether a 32-bit value exceeds 0xFFFFFFFF. Inference: the first is a bitvector-sort mismatch; the latter repaired query is unsatisfiable for every 32-bit value and does not itself prove that the C patch preserves all required behavior. The cFE witness truncates to zero, but other IDs with nonzero upper bits can truncate to a nonzero low word.

Verus form. Inference: write a Rust wrapper whose requires states the same source-level bounds and whose ensures proves no truncation or shift overflow. Use assert to expose cast-width obligations and proof fn lemmas for each case study. Inference: the paper’s reduced formulas cannot replace a proof of the complete C/Rust control-flow and FFI context.

Evidence and limits. Table 2 reports four primary targets: NASA cFE CWE-195 SAT, wolfSSL CWE-190 SAT+UNSAT, Mosquitto CWE-191+125 SAT, and NASA F Prime CWE-190+125 SAT, each with an acknowledged, patched, or disclosed outcome. The author states that the corpus is evidence of precision and feasibility, not comprehensive recall; no false-positive rate over large codebases is measured.

technique: layered containment and derived runtime guards

COBALT is Layer 1: SAT blocks deployment; UNSAT provides a guarantee for the analyzed input domain (Section 7.1, PDF p. 7). VERDICT checks six pre-execution predicates: target not external, action not email, action not public endpoint, scope authorized, hash approved, and session supervised (Section 7.2, PDF p. 7). DIRECTIVE-4 applies output policy before emission. SENTINEL logs actions with millisecond granularity and alerts humans. The paper’s illustrative email evaluation fails five of six predicates and is therefore UNSAFE (Section 7.2, PDF p. 8). The enforcement components are described as implemented, with end-to-end AI containment validation ongoing. DIRECTIVE-4 is described at the policy-predicate level; SENTINEL still needs production hardening and integration (Sections 7.3–7.4, PDF p. 8). VERDICT and DIRECTIVE-4 constrain only actions passing through their managed execution and emission paths.

The prototype COBALT-Runtime compiles Z3-derived bounds into O(1) comparisons. On 2,000 safe and 2,000 unsafe inputs across two invariants, it reports zero false positives and negatives, mean latency 87.2 ns, median 83.0 ns, p99 125 ns, and throughput 11.55 million checks/second (Section 11, PDF p. 10). The offline bound derivation takes 180 ms total. These denominators are 2,000 per class across two arithmetic invariants; they are not a production deployment study. Table 4 separately lists 301 ns/call for COBALT-Runtime without reconciling it with the 87.2 ns mean (PDF p. 9). The paper says: “A production-hardened implementation with IPC and syscall instrumentation is future work.” (Section 11, PDF p. 10).

COBALT-Graph connects the output of one arithmetic predicate to an input of another and solves their conjunction. In Listing 20, diff=sack_start-rcv_nxt must satisfy UGE(diff,0x80000000); size_arg=diff must also satisfy UGT(size_arg,4096). The prototype reports CWE-190→CWE-125 SAT in 8.1 ms and CWE-191→CWE-125 SAT in 4.6 ms (Section 11, PDF pp. 10–11). Inference: the shared variable establishes consistency of the reduced formulas, not that an actual program passes that value to a memory operation. The paper proposes enumerating type-compatible pairs and says deeper search needs incremental pruning; production compatibility filtering and depth-k enumeration remain future work (PDF p. 11).

Verus form. Inference: encode a runtime guard as executable Rust with requires on the derived bound and ensures that the crossing is accepted only when the predicate holds; prove the guard with a proof fn over machine integers. Inference: policy predicates can be ordinary contracts, but logging, network mediation, and model behavior remain trusted components outside a functional proof.

what is proved, measured, and trusted

The paper labels its arithmetic results and four production case studies validated; COBALT-Runtime and COBALT-Graph are prototypes (Table 4, PDF p. 9). The Mythos connection is conditional on A-SRC (source available), A-CWE (escape is CWE-190), and A-SCOPE (pattern in coverage); the paper explicitly says Anthropic did not confirm A-CWE (Section 8.2, PDF p. 8).

techniques for the catalog

  • AST-to-bitvector reachability — extract arithmetic patterns and ask Z3 for SAT witnesses under exact machine widths
  • bound-to-UNSAT proof — add explicit input guards and prove the overflow predicate impossible in the bounded domain
  • reduced production encodings — validate the same predicate on real C/C++ cases while preserving cast and width semantics
  • layered containment — combine deployment scanning, pre-execution policy, output firewalling, and runtime observability
  • compiled invariant guards — turn offline Z3-derived bounds into constant-time runtime checks
  • dataflow escalation graphs — compose successive CWE predicates so one witness becomes the next stage’s input

Last edited: