Local Allow, Global Deny: Why Per-Action Authorization Does Not Compose in LLM Agents

© 2026 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. Accepted for publication in the proceedings of IEEE TPS 2026.

arXiv:2610.27620v1 [cs.CR] 20 Oct 2026

Local Allow, Global Deny: Why Per-Action Authorization Does Not Compose in LLM Agents Anmol Pandey

Aditya Jain

Liang Chen

Carsten Maple

University of Warwick Coventry, United Kingdom Anmol.Pandey@warwick.ac.uk

University of Warwick Coventry, United Kingdom aditya.jain.5@warwick.ac.uk

University of Hertfordshire Hatfield, United Kingdom l.chen26@herts.ac.uk

University of Warwick Coventry, United Kingdom cm@warwick.ac.uk

each action locally authorized

Abstract—Autonomous LLM agents act through tools under per-action authorization: a local guard screens each tool call in isolation. We show that local authorization does not compose into global authorization. A compositional authorization failure (CAF) is a locally authorized execution, or a pair of locally authorized executions, that violates a global policy spanning intent, purpose, provenance, consent, and delegation. We characterize CAFs along two axes, expressiveness (single-trace safety versus relational ksafety) and observability (a ladder of monitor profiles). Our central result is an impossibility: relational purpose violations form a 2-safety hyperproperty with no per-trace locus of blame, so a per-action monitor that never raises a false alarm detects none of them, independent of the underlying model or decision procedure; they become visible only under cross-execution monitoring, which none of the six guardrails we survey implements. We make this constructive with AL-S YNTH, a SAT/SMT synthesizer (using no language model) that emits minimal CAF witnesses, each checked against an exhaustive oracle. The empirical signature is sharp: across nine LLM judges the per-action view approves the synthesized witness almost without exception, blocking it at a rate comparable to a benign control, yet the same models flag it when shown the two executions together. Per-action authorization is therefore structurally insufficient for relational policy conjuncts not reducible to single-trace safety: to bound them, a monitor must compare executions or accept false alarms. Index Terms—LLM agents, authorization, hyperproperties, runtime monitoring, information flow, program synthesis, security policies

I. I NTRODUCTION Agents built on large language models act through tools: they read mail, write files, call web services, and delegate subtasks. The dominant safeguard is per-action authorization. A guard inspects each tool call in isolation and decides whether it is permitted, and a sequence of approved steps is treated as an approved sequence. This trust model is wrong in a way that matters: local authorization does not compose. A sequence of individually permitted actions can violate a global policy, alone or together with a second, equally compliant execution. We call such a witness a compositional authorization failure (CAF), illustrated in Figure 1. This is the agent-era form of a classical fact, that security properties need not compose [1], sharpened by two

a1

a2

a3

a4

global policy Φ over the whole trace: violated Fig. 1. A compositional authorization failure, single-trace case. Every action passes its local check (top), yet the composed trace violates the global policy Φ (bottom), with no single offending step. The relational purpose failure is witnessed instead by a pair of individually compliant executions (Figure 3).

features. First, some policies that agents must respect are hyperproperties [2]: they constrain sets of executions, not single runs. A purpose constraint says that what an agent discloses must not depend on context its declared purpose does not authorize, and checking this requires comparing runs. Second, the guards being deployed are single-trace execution monitors in Schneider’s sense [3]: each observes one run and decides. The mismatch is a gap in expressive power, not an engineering gap that a better per-trace monitor could close. Our results are negative and constructive. We prove that one class of failure, the relational purpose violation, has no per-trace locus of blame: a per-trace monitor that never flags a compliant trace detects none of these violations, because each trace alone is compliant and the violation lives only in the relationship between runs. It becomes detectable only by comparing executions, which none of the six guardrails we survey does. We make the result mechanical with AL-S YNTH, a bounded model checker built on a SAT/SMT solver, with no language model, that synthesizes minimal CAF witnesses and computes the monitor-coverage curve, validated against an exhaustive oracle. Three studies test whether the gap matters in practice. Nine language models, screening each action of the synthesized witness, approve it almost without exception, yet the same models flag it when shown both executions. A live openweights agent commits a consent-composition CAF in 22 of 60 rollouts, which an intent-only guard does not measurably

reduce and a composition-aware guard eliminates. An offline audit of Claude Sonnet 4.6 finds that it resists every class we test. That agent is safe because the model behaves, not because a monitor caught anything, and no false-alarm-free single-execution monitor could have caught a leak, whatever the model. Contributions.1 • A model and a map (§III, §IV): CAFs against a fiveconjunct global policy, characterized by expressiveness (safety versus k-safety) and observability (a monitor ladder P0 to P7 ). • Separation and impossibility (§V): the purpose property is 2-safety, relational exactly under a stated non-collapse condition, and invisible to every false-alarm-free per-trace monitor. A relational monitor crosses the expressiveness barrier but not the statistical one. • A validated synthesizer (§VI, §VII): AL-S YNTH computes minimal witnesses and the coverage curve, checked for soundness, bounded completeness, and minimality against an exhaustive oracle. • Measured monitor blindness (§VIII): among six surveyed guardrails, the strongest single-execution profile covers seven of eight classes, six exactly and explicit labeled flow only conservatively, and misses the relational purpose class. Per-action judges and a LangGraph guard exhibit the separation, and a live agent shows a composition-aware guard closing a catchable CAF. Relation to classical results. The ingredients are classical, and we claim none of them: security properties need not compose [1], noninterference is a hyperproperty [2], [4], execution monitors enforce only safety [3], and noninterference can be enforced precisely by running one execution per security level [5]. What is new is what these facts imply for agent authorization. An agent’s authorization policy splits into a trace-safety part and a relational-purpose part. We give the exact condition under which the purpose part is relational (Theorem 1), prove that no false-alarm-free per-trace monitor detects it, whatever its decision procedure (Theorem 3), and extend this to stochastic agents, for which even cross-execution sampling gives only statistical detection (Theorems 4 and 5). Every guardrail we survey sits on the trace-safety side. Given a tool schema, a workflow policy, and a monitor profile, ALS YNTH returns a minimal locally permitted witness outside that monitor’s reach and names the observation the monitor would need to catch it. II. T HREAT M ODEL AND BACKGROUND Setting. We consider a single LLM agent that executes a bounded episode in response to a user task. The agent issues a finite sequence of actions (tool calls), each drawn from a typed action set, against an environment with mutable state. A local authorization predicate decides, from the current state and 1 All code, synthesized witnesses, the nine-judge sweep data, and reproduction scripts are available at https://github.com/anmolpandey299/al-synth.

the action, whether the action is individually permitted. This predicate abstracts the per-action guards, permission prompts, and tool-call monitors that deployed agent frameworks use today. A global policy Φ expresses what the user actually authorized for the episode as a whole. Adversary. The adversary’s goal is a trace that satisfies every local check yet violates Φ. We do not assume a jailbroken or locally-misbehaving agent. The interesting case, and the one our theory targets, is a benign-looking agent operating under a declared, legitimate purpose whose composed behavior channels information or authority the purpose does not grant. The adversary may influence the agent through ordinary means such as task phrasing or injected content in tool results, but it does not need to defeat the local guards; it needs the composition to do work the guards cannot see. Running example. A scheduling assistant is asked to “find a time for a team meeting next week” and is authorized to “share my free/busy availability.” The purpose authorizes disclosure to depend on whether each slot is free. It does not authorize disclosure to depend on why a slot is busy, for instance that a busy block is a confidential interview rather than an ordinary meeting. Every individual action the assistant takes (read the calendar, propose slots, send the proposal) can pass a local check. Whether the pattern of what it offers depends on the unauthorized reason is a property of how it behaves across situations, not of any one message. We return to this example throughout. Background. A trace property is a set of traces; a hyperproperty [2] is a set of sets of traces, and a k-safety hyperproperty has a counterexample consisting of k finite traces. Noninterference [4] is the canonical 2-safety property: it forbids high inputs from affecting low outputs, and a violation is exhibited by two runs that agree on low inputs but differ on low outputs. Realistic policies relax strict noninterference through declassification [6], which specifies what high information may be released. An execution monitor observes a single run and may halt it, so it can enforce only safety properties of single traces [3], [7]. III. C OMPOSITIONAL AUTHORIZATION FAILURES Model. An agent model is a typed transition system. A state assigns values to a finite set of typed variables. An action a carries a guard ga , a predicate on states, and an effect that updates a subset of variables. A finite trace t = a1 a2 · · · an is locally authorized if, executing from the initial state, each ai is enabled (its guard holds) in the state it is taken from. We write Σ∗ for finite traces. For a trace we distinguish three projections: low(t), the declared purpose and other low inputs; hi(t), the sensitive context the agent may read; and obs(t), the outward disclosure the agent produces. Definition 1 (Compositional authorization failure). Fix a model with local authorization predicate auth and global policy Φ. A CAF witness is a finite, locally authorized object that witnesses a violation of Φ: when Φ is a trace property, a single trace t with auth true at every step yet t ̸|= Φ; when Φ

is a hyperproperty, a finite tuple or set of traces, each locally authorized at every step, that jointly violate Φ. We call the individual traces of a witness its executions. For the relational purpose class the witness is a pair of executions that are each compliant in isolation. The global policy. We take Φ to be a conjunction of five authorization concerns drawn from the access-control and privacy literature: Φ = C1 ∧ C2D ∧ C3 ∧ C4 ∧ C5 , namely intent (C1 : actions stay within the user’s task), purpose (C2D : disclosure depends only on purpose-authorized context), provenance (C3 : outputs do not derive from untrusted or crossdomain sources in disallowed ways), consent (C4 : disclosure stays within consented scope, per action and cumulatively), and delegation (C5 : delegated authority is exercised only when revalidated). Four of the five are properties of a single trace. The purpose conjunct is not. The purpose conjunct. Following the declassification view [6], we parameterize purpose by a declassification function D, the purpose-authorized view of context, and an abstraction α, the policy-relevant view of disclosure:  C2D = S : ∀ t, t′ ∈ S. low(t) = low(t′ ) (1) ∧ D(hi(t)) = D(hi(t′ )) ′ ⇒ α(obs(t)) = α(obs(t )) . In words: two runs that agree on the low inputs and on everything the purpose authorizes about context must agree on what they disclose. If they can differ, disclosure is depending on something the purpose did not authorize. The pair (D, α) comes from the policy. In the running example, the purpose “schedule a team meeting” with consent “share free/busy availability” fixes D as the free/busy status of each slot, excluding the reasons slots are busy. The abstraction α keeps the policy-relevant parts of a disclosure: which slots are offered, any attached reason or label, the granularity, and the recipient. Eq. (1) then says that, with the free/busy view fixed, the offered slots must not depend on the reasons. For realistic workflows, specifying (D, α) can take substantial human judgment. The impossibility does not depend on getting it right: Theorem 3 holds for every pair, and violations exist exactly when the pair is residual-nondegenerate (Definition 2, Theorem 1). A misspecified pair changes which disclosures count as violations, and so what a relational auditor flags, but no choice of (D, α) makes a nontrivial purpose conjunct visible to a false-alarm-free per-action guard. IV. A T WO -A XIS C HARACTERIZATION The failure classes differ along two independent axes. Axis 1: expressiveness. A class is either a property of a single trace (a safety property, with a finite bad prefix as a witness) or a relational property (a k-safety hyperproperty, with a k-trace witness). Intent, provenance-by-path, consent, and delegation are single-trace. The purpose conjunct C2D is relational, and we prove this in §V.

Axis 2: observability. A monitor can only act on the state it is instrumented to observe. We arrange instrumentation as a ladder of profiles P0 through P7 , each strictly more observant than the last. P0 is pure black box. Intermediate profiles add, in turn, an approximation of user intent, information-flow labels and a purpose label, a provenance graph, per-action consent state, a delegated-authority and revalidation view, and cumulative digests of intent and consent. P6 adds a cross-domain state-transfer view, the strongest single-execution instrumentation we consider. P7 is the only profile with relational power: it can compare distinct executions of the agent. A monitor at profile P detects a class if it can both express the class (Axis 1) and observe the state the class depends on (Axis 2). Figure 2 places the eight subclasses on these axes. The single-trace classes are covered one by one as instrumentation grows, and explicit labeled flow is covered, conservatively, at P6 . The relational purpose class is 2-safety, so no singleexecution profile can express it. It is covered only at P7 , beyond every system we survey. V. S EPARATION R ESULTS We use the standard hyperproperty machinery [2]. For a set of traces T , write [T ] = {S : S ⊆ T } for the hyperproperty it induces; a hyperproperty is trace-property-induced if it equals [T ] for some T . We sketch each argument here. The full proofs are in Appendix A. Lemma 1 (The monitorable region). C1 , the path form of C3 , C4 , and C5 are safety properties of single traces. Each has the form “∀t ∈ S. ϕ(t)” for a per-trace predicate ϕ, hence equals [{t : ϕ(t)}], and each violation has a finite bad prefix. These classes are exactly the ones a per-trace monitor can enforce. The labeled-flow form of C3 , written C3lf , is itself relational (2-safety), but its protected influence is a syntactic data flow from a labeled source to the output, and a single-execution information-flow profile (P6 ) overapproximates it soundly through taint tracking: P6 enforces the single-trace property “no labeled value reaches a low output,” which conservatively covers C3lf at the usual cost of some false positives. That is why C3lf closes conservatively at P6 . The implicit, control-flow-dependent fragment of noninterference is not C3lf but the relational purpose class C2D . Explicit-flow taint tracking misses it, and tracking control dependencies over-approximates it only by rejecting nearly every disclosure made after unauthorized context is read, compliant or not [8]. The relational purpose class C2D is different. In a C2D witness the agent discloses from an authorized view that is identical in both worlds (low and D(hi) equal). No labeled value reaches the output, so taint tracking has nothing to follow, and the dependence on the unauthorized reason shows only when the two executions are compared. A single-execution monitor can over-approximate C2D soundly, for example by blocking every disclosure once unauthorized context is read, but only by rejecting compliant traces. The results below make this precise: no single-execution monitor enforces C2D both completely and without false alarms, and cross-execution

relational (k-safety)

surveyed frontier C3 f

C2 r

P6

P7

1

0

single-trace (safety)

the relational purpose class: no single-execution locus, only P7

P0

C1

C2 ℓ

C3 p

C4 a

C5

C4 c

P1

P2

P3

P4

P5

P5 +

observability (monitor instrumentation profile) −→ undetected (of 8):

8

7

6

5

4

3

2

Fig. 2. The two-axis map, with class labels as in Table III. Increasing observability (left to right) covers the single-trace classes one by one (teal). The relational purpose class C2 r (coral) is 2-safety, so no single-execution profile can express it; it is covered only by the relational profile P7 , beyond the strongest profile any surveyed system reaches. The bottom row is the number of undetected classes per profile, the monitor-coverage curve of §VII.

comparison (P7 ) is the first observable that separates compliant from violating disclosures. Definition 2 (Residual-nondegenerate). A pair (D, α) is residual-nondegenerate if there exist finite traces a, b with low(a) = low(b), D(hi(a)) = D(hi(b)), and α(obs(a)) ̸= α(obs(b)). In plain terms, the declared declassification does not fix the disclosure, so unauthorized context has room to move the output. We call this assumption Residual Disclosure Freedom (RDF-D), and write RDF-DA when a, b are restricted to the locally authorized set A. RDF-D characterizes C2D (Theorem 1), and RDF-DA makes the global policy Φ = [A]∩C2D relational (Theorem 2). Theorem 1 (Exact characterization of C2D ). For every declassification D and abstraction α: (1) C2D is 2-safety; (2) C2D is not trace-property-induced if and only if (D, α) is residualnondegenerate; (3) if (D, α) is collapsing, C2D is the trivial hyperproperty, satisfied by every system. The key observation is the singleton fact: because equality is reflexive, every single-trace system {t} satisfies C2D . If (D, α) is nondegenerate, a violating set contains a pair a, b as in Definition 2, and finiteness makes {a, b} a 2-trace witness, which gives both 2-safety and, by the singleton fact, noninducedness. If it is collapsing, the implication in Eq. (1) holds for all admissible pairs, so every system satisfies the property and it is the trivial, trace-induced hyperproperty. The condition in part (2) is exactly what the proof needs, and a constant abstraction α shows it cannot be dropped. Theorem 2 (Φ is relational under RDF-DA ). Let A = {t : C1 ∧ C3 ∧ C4 ∧ C5 }, so Φ = [A] ∩ C2D . If (D, α) is residualnondegenerate with witnesses in A (RDF-DA ), then Φ is not trace-property-induced.

Take RDF-DA witnesses a, b ∈ A. Each singleton satisfies C2D by reflexivity and lies in [A], so {a}, {b} ∈ Φ. If Φ = [U ] for some U , then a, b ∈ U , hence {a, b} ∈ [U ] = Φ ⊆ C2D ; but {a, b} ∈ / C2D by construction, a contradiction. If RDF-DA fails, Φ collapses to a single-trace property and per-trace monitoring suffices. RDF-D formalizes the premise of this paper: useful assistants keep disclosure freedom beyond what their declared purpose fixes, and the question is whether that freedom carries protected context. A. The Locus theorems The central result says that a relational purpose violation cannot be pinned to any single execution. Theorem 3 (Set Locus). A per-trace monitor that never raises a false alarm for C2D detects no violation of C2D . Every single trace satisfies C2D (the singleton fact), so a false-alarm-free per-trace monitor cannot flag any trace at all. Relational purpose violations have no per-trace locus of blame. Contrapositively, a per-trace monitor that catches a genuine purpose violation must also flag a compliant trace (Corollary 1). An LLM at nonzero temperature is a distribution over traces, so the right property is distributional independence rather than set equality. Set-C2D over a stochastic agent’s support is stronger than independence, since it also forbids context-independent randomness, which leaks nothing, so independence is the deployable target. Theorem 4 (Distributional Locus). Let the observable e available to a single-execution monitor contain exactly the perexecution fields low, D(hi) where exposed, and obs, but not the nondeclassified context H, not the agent’s full conditional distribution, and not cross-context samples. Over the class of

same authorized view (low, D(hi) equal), only the hidden reason differs World a World b

read read

aggr. aggr.

offer 10 offer 11

̸= α(obs) differs

Fig. 3. Why purpose is relational. Two executions agree on the low inputs and on the purpose-authorized view of context (the same slots are free) and differ only in a hidden, unauthorized reason. Each offers a free slot, so neither trace alone is faulty, yet the disclosures differ (α(obsa ) ̸= α(obsb )). That difference is explained only by the unauthorized reason, so the pair is the 2-safety witness for C2D : it is visible only by comparing executions, which a relational (P7 ) monitor does and a per-action monitor cannot.

all stochastic agents, no monitor that sees one such e can soundly and completely decide Y ⊥ H | low, D(hi), where Y = α(obs). For any single observable e of positive probability, one can construct a safe agent (Y ⊥ H) and a leaky agent (Y ̸⊥ H) that both assign e positive probability. The monitor sees the same e under both: alarming is a false alarm on the safe agent, and not alarming is a miss on the leaky one. A single execution cannot certify distributional dependence model-free. Theorem 5 (Two-dimensional barrier). Under the ladder taxonomy and RDF-DA , no profile P≤6 soundly and completely enforces Φ, and none soundly detects C2D . For the possibilistic property, the relational profile P7 crosses the barrier, since it can exhibit the two-trace witness. For the distributional property the barrier has two dimensions, and P7 crosses only one of them: it crosses the expressiveness dimension, because collecting cross-context samples escapes the per-trace limit, but it does not cross the statistical dimension, because no finite-sample procedure can soundly and completely decide arbitrary distributional independence over all stochastic agents. For the possibilistic property, P7 compares two executions and exhibits the witness of Theorem 1. For the distributional property, any finite sample is consistent with two agents, one with Y ⊥ H and one without, whose sample distributions are arbitrarily close, so detection is statistical rather than certain. Logics, model checking, and runtime verification for hyperproperties are established [9]–[11], including a probabilistic logic [12], so P7 as a capability is known. Our claim concerns deployment: no surveyed agent-authorization monitor implements it. Corollary 1 (A design rule). Detecting purpose violations admits exactly three responses: tolerate false positives, audit offline with cross-context samples, or monitor relationally (compare executions). A per-trace monitor that is both falsealarm-free and useful for C2D does not exist. B. An enumeration result, scoped Counting, for each profile, the subclasses it cannot detect gives the monitor-coverage curve [8, 7, 6, 5, 4, 3, 2, 1, 0] from P0 to P7 . The endpoints are proven: P0 detects nothing, P7

symbolic model (two semantics)

SMT solver (Z3 BMC)

brute-force oracle

differential check: T1 sound T2 complete T3 minimal

minimal witnesses, coverage curve

Fig. 4. AL-S YNTH. One symbolic model with two semantics drives an SMT solver and an exhaustive oracle. A differential check compares them (soundness, bounded completeness, minimality), and the validated pipeline emits minimal witnesses and computes the monitor-coverage curve.

covers all eight classes under the possibilistic semantics of Eq. (1), and the last class to fall is C2rel . The intermediate values depend on our eight-class taxonomy and ladder. The central result does not: Theorem 3 covers every per-trace monitor, whatever it observes, so under any refinement or coarsening of the single-execution rungs the relational row stays uncovered until a profile compares executions. Only the number and order of the intermediate steps change. Stated narrowly: in our taxonomy, with delegation scoped to peraction revalidation, exactly one class is not per-trace monitorable, and it fails by expressiveness, not by any engineering limitation. VI. AL-S YNTH : C ONSTRUCTIVE S YNTHESIS AL-S YNTH makes the gaps concrete. Given a model and a target class, it synthesizes a minimal CAF witness (a trace, or a pair of traces for the relational classes) that is locally authorized at every step and globally unauthorized and, for a target profile, also evades every check that profile can run. The engine is symbolic and uses no language model. Figure 4 shows the pipeline. Dual semantics. Each action has two semantics over the same transition system: a reference semantics, used by an exhaustive oracle, and an SMT encoding, used by the solver. The harness checks that both induce the same CAFs, so agreement is tested rather than assumed. Bounded model checking. For a horizon n, the solver encodes the initial state, the variable ranges, the transition relation, and the local-authorization invariant (at every step, the chosen action’s guard holds), then conjoins the global violation at the final state. A satisfying assignment is a length-n CAF [13], [14]. We enumerate the complete witness set at a horizon by adding a blocking clause after each model and re-solving (all-SAT). For synthesis in practice we instead search for the minimal witness, one satisfiability query per increasing horizon, which is far cheaper. Relational witnesses by self-composition. A relational violation is existential: it asks for a pair of traces that jointly witness a breach of 2-safety. We obtain it by self-composition [15]. Two copies of the system run side by side, and the encoding asserts equality of the low inputs and of the declassified view, low(a) = low(b) and D(hi(a)) = D(hi(b)), together with inequality of the abstracted observation, α(obs(a)) ̸= α(obs(b)). This is exactly the negation of the C2D implication, so a satisfying assignment is a two-trace witness that the agent’s

VII. VALIDATION AND THE C OVERAGE C URVE We validate the solver against the exhaustive oracle on a family of small models, small precisely so that brute-force enumeration is ground truth. Differential testing. Three checks relate the solver to the oracle, per class and horizon. T1, soundness: every solver witness, replayed through the reference semantics, is locally authorized at every step and globally unauthorized. T2, bounded completeness: the solver’s all-SAT witness set equals the oracle’s set. T3, minimality: the solver’s minimal witness length equals the oracle’s. All three pass for every class, including the relational class, whose self-composed witness matches the oracle’s minimal pair. Oracle agreement is differential testing of two encodings of one intended semantics: it catches encoding errors, but it does not show that the semantics models a deployment correctly. The coverage curve is measured, not assigned. For each profile and class, the solver either synthesizes a witness the profile cannot see (a CAF that evades every check the profile can run or, for the relational classes, the two-trace counterexample) or certifies that none exists up to the horizon. Solver and oracle agree on all 9×8 cells (Table I). Perturbation shows that the curve tracks the instrumentation: removing the purpose-label observable shifts it to [8, 7, 7, 6, 5, 4, 3, 2, 1], as the labeled purpose class staying undetected predicts, and restoring it returns the original. Against every profile up to P6 , the strongest we survey, the residual is exactly the relational purpose class, an expressiveness gap that more carried state cannot close. Cost. On the cumulative-consent model, minimal-witness synthesis (one satisfiability query per horizon) stays flat, at about 0.02 to 0.07 s, up to depth twelve. All-SAT enumeration, used only for the completeness check, grows exponentially: from 1 to 29,337 witnesses over depths three to seven, and from 0.02 to 118 s, a gap of about 2,770 times at depth seven. Cost tracks the query, not the size of the witness set. This is a shape on one model, not a benchmark. Figure 5 shows both curves, and the data are in the artifact. VIII. E MPIRICAL S TUDY: M ONITOR B LINDNESS AND F RONTIER AGENTS We ask two questions. Do agent guardrails detect CAFs, and which ones? And does a frontier agent commit the relational purpose violation when an adversary sets it up? The first concerns the monitor, which is what the impossibility is about. The second concerns the model.

wall-clock time (s)

disclosure depended on context the purpose did not authorize (Figure 3). Generating a witness is existential, hence SAT. QBF arises only in the universal direction, proving that a monitor cannot catch a class. Instrumentation relativization. To synthesize a witness that is invisible to a monitor at profile P , the encoding conjoins, inside the same query, the target violation with the negation of every safety check that P can both express and observe. The evasion is part of the constraint, not a filter applied afterward.

29,337

102

2,781 ∼2,770×

100

247

10−2 1

2

3

4

5

6

7

8

9

10

11

12

synthesis horizon (bounded trace depth) all-SAT enumeration

minimal-witness synthesis

Fig. 5. Synthesis cost on the cumulative-consent model (11 actions, Z3 4.16). Minimal-witness synthesis (dashed) stays flat to depth twelve, while allSAT enumeration (solid, used only for the oracle check) grows exponentially with the witness count (annotated). One model; times are illustrative, not a benchmark.

A. The defense matrix: coverage measured per profile We do not run the guardrail implementations. We place each surveyed mechanism at the strongest profile its published design supports and measure that profile with the campaign of §VII. Table II lists what each design observes and the profile it receives. None compares two executions of the same purpose (Appendix B). The assignment is deliberately charitable: crediting a design with less would only widen the gap we report. Each row is therefore a capability bound read from the design, not a test of the code, and the bound is one-sided where it matters. Running an implementation could lower a single-trace cell, through a bug for instance, but by Theorem 3 it could raise the relational purpose cell only by comparing executions or by accepting false alarms (Corollary 1). Table III is read by columns. Coverage grows with sophistication: per-tool approval catches none of the eight classes, RTBAS three, CaMeL five, and Fides and SAFEFLOW seven, six exactly and explicit labeled flow conservatively. Yet all six miss the same class. The relational purpose column is ◦ for every surveyed mechanism, including Fides, whose authors note that it does not prevent the implicit control-flow channel this column captures (§X). Only the relational auditor at P7 catches it, as the Locus theorem predicts, whatever model the guard protects. The witness is minimal. On the scheduling model the shared trace is (collect, aggregate, report). In world a a busy slot is an ordinary meeting and the agent offers slot 10. In world b the same slot is a confidential interview and the agent offers slot 11. Each trace alone is locally authorized, so no per-action check fires. The auditor compares the pair and fires. B. Case study: the blind spot in a LangGraph workflow To check that the blind spot is not an artifact of our abstract model, we reproduce it in a scheduling workflow built on LangGraph [20], a widely used agent framework. The graph (read, aggregate, propose) is gated by a per-action guard

TABLE I M ONITOR - COVERAGE MATRIX , SOLVER - VALIDATED AND CONFIRMED AGAINST THE BRUTE - FORCE ORACLE ( ALL 72 CELLS AGREE ). •: THE PROFILE DETECTS THE CLASS EXACTLY, FLAGGING EVERY WITNESS AND NO COMPLIANT TRACE . G #: DETECTS IT ONLY CONSERVATIVELY, A SOUND OVER - APPROXIMATION THAT ADMITS MOST COMPLIANT TRACES AT THE COST OF SOME FALSE ALARMS . ◦: NO MONITOR AT THAT PROFILE DETECTS IT WITHOUT MISSING WITNESSES OR BLOCKING COMPLIANT BEHAVIOR . T HE ONE G # ROW IS EXPLICIT LABELED FLOW, OVER - APPROXIMATED BY TAINT TRACKING AT P6 AND ABOVE . B OTH • AND # G COUNT AS COVERED IN THE BOTTOM - ROW CURVE . O NLY RELATIONAL PURPOSE (C2 , SHADED •) ADMITS NO PER - TRACE COVERAGE AT ALL , CLOSING AT P7 (T HEOREM 3).

CAF (sub)class

P0

P1

P2

P3

P4

P5

P5 +

P6

P7

C1 intent C2 purpose (labeled) C2 purpose (relational) C3 provenance (path) C3 flow (explicit labeled) C4 consent (per-action) C4 consent (composition) C5 delegation

◦ ◦ ◦ ◦ ◦ ◦ ◦ ◦

• ◦ ◦ ◦ ◦ ◦ ◦ ◦

• • ◦ ◦ ◦ ◦ ◦ ◦

• • ◦ • ◦ ◦ ◦ ◦

• • ◦ • ◦ • ◦ ◦

• • ◦ • ◦ • ◦ •

• • ◦ • ◦ • • •

• • ◦ • # G • • •

• • • • G # • • •

undetected (of 8)

8

7

6

5

4

3

2

1

0

cross-context samples a deployed monitor lacks, on Claude Sonnet 4.6 used as a tool-calling agent at fixed temperature (Table IV). For intent, an injected instruction in a tool result MECHANISM COMPARES DISTINCT EXECUTIONS OF THE SAME PURPOSE , THE P7 CAPABILITY. asks the agent to forward output to an unintended recipient, and it refuses every time. For consent, the agent stays within Mechanism What it observes Profile Cross-exec. a narrow authorized window every time, and on a deliberately vague variant it asks for clarification instead of calling a tool. Per-tool approval current action, shown to a P0 no human For relational purpose, a paired, interleaved, pre-registered exTask Shield [16] action versus task goal P1 no periment holds the free/busy view fixed across two conditions RTBAS [17] IFC taint and dependenP3 no that differ only in the hidden reason, and gates on a high share cies rate so that a null reflects disclosure rather than refusal. The CaMeL [18] data and control flow, caP5 no agent does not leak. pabilities Fides [8] IFC labels, explicit seP6 no a) A false positive, kept on purpose: An initial analysis crecy reported a significant covert signal, stable across seeds. RawSAFEFLOW [19] IFC labels and provenance P6 no output inspection overturned it: both conditions offered the AL-S YNTH (relational) two executions, same purP7 yes identical set of slots, and the signal came from a feature pose extractor counting a word whose phrasing happened to differ. Under the policy-relevant abstraction α that Eq. (1) requires, the channel is clean. We keep the episode because a result is a that runs the standard tool-permission check plus purposesecurity result only under an abstraction that tracks the policy, label, provenance, and per-action consent checks. Two worlds with raw-data inspection as a check that no statistical rigor share the authorized free/busy view and differ only in the replaces. hidden reason a slot is busy. The guard returns the same decisions (allow, allow, allow) in both worlds, although the action arguments differ, and the agent offers slot 10 in one D. Per-action judges approve the witness; the paired auditor world and slot 11 in the other. The AL-S YNTH relational catches it auditor compares the runs and flags the C2D violation. We The defense matrix places mechanisms by design. Here claim no vulnerability in LangGraph: the blindness belongs to we put the witness in front of real models. Nine language the per-action permission pattern, and the dependence could models judge the synthesized relational witness step by step: be a benign tie-break, an adversarial choice, or an injected eight hosted models (from Anthropic, OpenAI, Google, xAI, instruction, which no per-action guard can tell apart. DeepSeek, Alibaba, Meta, and Moonshot) and one local openweights model. A bank of ten scenarios varies the slot pair, C. A frontier agent, audited offline the hidden reason, the task phrasing, and the A/B order, at The theorem says a per-trace monitor cannot catch the three repetitions each, which measure stability rather than add relational class. It does not say whether real agents commit coverage. All judges run at temperature 0 with a 4000-token it. We test this directly, acting as an offline auditor with the budget, the hosted ones through OpenRouter’s default routing TABLE II S URVEYED AGENT- AUTHORIZATION MECHANISMS AND THE PROFILE EACH RECEIVES IN TABLE III. “C ROSS - EXEC .” ASKS WHETHER THE

TABLE III D EFENSE MATRIX , CONFIRMED AGAINST THE BRUTE - FORCE ORACLE ; SYMBOLS AS IN TABLE I. E ACH MECHANISM IS PLACED AT THE STRONGEST PROFILE ITS PUBLISHED DESIGN IMPLEMENTS , SO ITS ROW IS A CAPABILITY BOUND FROM THE DESIGN , NOT AN EXECUTION OF ITS CODE . T HE RELATIONAL PURPOSE COLUMN ( SHADED ) IS MISSED BY EVERY SURVEYED MECHANISM : F IDES AND SAFEFLOW (P6 ) COVER SIX CLASSES EXACTLY AND EXPLICIT LABELED FLOW CONSERVATIVELY, AND ONLY THE RELATIONAL AUDITOR (P7 ) COVERS RELATIONAL PURPOSE .

mechanism (profile)

C1

C2 ℓ

C2 r

C3 p

C3 f

C4 a

C4 c

C5

Per-tool approval (P0 ) Task Shield [16] (P1 ) RTBAS [17] (P3 ) CaMeL [18] (P5 ) Fides [8] (P6 ) SAFEFLOW [19] (P6 )

◦ • • • • •

◦ ◦ • • • •

◦ ◦ ◦ ◦ ◦ ◦

◦ ◦ • • • •

◦ ◦ ◦ • • •

◦ ◦ ◦ ◦ • •

◦ ◦ ◦ • • •

AL-S YNTH relational audit (P7 )

•

•

•

•

◦ ◦ ◦ ◦ G # G #

•

•

•

TABLE IV O FFLINE AUDIT OF C LAUDE S ONNET 4.6 ( FIXED TEMPERATURE ). CAF IS THE NUMBER OF COMPOSITIONAL AUTHORIZATION FAILURES OBSERVED ; UB IS THE EXACT ONE - SIDED 95% C LOPPER –P EARSON UPPER BOUND ON THE PER - EPISODE RATE . P ROMPTS , SEEDS , AND SETTINGS ARE IN THE ARTIFACT.

Task

Class

n

CAF

95% UB

Injected-doc forward Narrow-scope share Scheduling audit

C1 C4 C2 r

10 10 80

0 0 0†

≤ 26% ≤ 26% ≤ 3.7%

† Under the policy-relevant abstraction α. An initial parser-artifact positive

was removed (see text).

with no pinned provider. Exact model identifiers are listed under Table V.

TABLE V P ER - ACTION JUDGES OVER THE SYNTHESIZED RELATIONAL WITNESS . C ELLS COUNT THE SCENARIO - REPETITIONS , OUT OF 30 ( TEN TEMPLATES , THREE REPETITIONS ), IN WHICH THE JUDGE BLOCKS AT LEAST ONE ACTION : WIT THE WITNESS , BEN A BENIGN NO - LEAK CONTROL , C1 AN OVERT SINGLE - TRACE CONTROL , AND AUD THE RELATIONAL AUDITOR , THE SAME MODEL SHOWN BOTH EXECUTIONS . H OSTED MODELS RAN THROUGH O PEN ROUTER AND THE LOCAL MODEL THROUGH V LLM.

judge

wit

ben

C1

aud

Claude Opus 4.8 GPT-5.5 Gemini 3.1 Pro Grok 4.3 DeepSeek V4 Pro Qwen3.7-max Llama-4-Maverick Kimi-K2.6 Qwen3-30B (local)

0/30 0/30 0/30 0/30 0/30 0/30 0/30 3/30 0/30

0/30 0/30 0/30 0/30 2/30 0/30 0/30 1/30 0/30

30/30 30/30 30/30 30/30 30/30 30/30 30/30 30/30 30/30

30/30 30/30 30/30 30/30 30/30 30/30 17/30 30/30 30/30

judge

Eight judges never block the witness (0/30 each). KimiK2.6 blocks it in 3 of 180 individual steps (3 of 30 scenario repetitions, across 3 of the 10 templates). The discriminating control is a benign trace in which both worlds disclose the same slot. DeepSeek blocks 2 of its 180 benign steps and Kimi 1, so Kimi’s witness blocks sit in the same band as its benign blocks. They reflect single-step conservatism, not relational detection, since a per-action judge never sees the second execution. The judges are not merely permissive: all nine block an overt single-trace C1 step, an injected external forward, 30/30 (Table V). The relational auditor, the same model shown both executions, recovers detection: 30/30 for eight judges and 17/30 for Llama-4-Maverick. The table therefore instantiates the observation-model separation, the same model blind per action and sighted on the pair, rather than nine independent vulnerabilities, and by the Locus theorem the per-action blindness holds for any single-execution decision procedure. Llama’s 17/30 also separates relational observability, which P7 supplies, from relational detection reliability, which remains a question of model capability.

G #

API identifier (accessed June 2026)

Claude Opus 4.8 anthropic/claude-opus-4.8 GPT-5.5 openai/gpt-5.5 Gemini 3.1 Pro google/gemini-3.1-pro-preview Grok 4.3 x-ai/grok-4.3 DeepSeek V4 Pro deepseek/deepseek-v4-pro Qwen3.7-max qwen/qwen3.7-max Llama-4-Maverick meta-llama/llama-4-maverick Kimi-K2.6 moonshotai/kimi-k2.6 Qwen3-30B (local) Qwen/Qwen3-30B

E. A live agent commits a catchable CAF, and the right monitor closes it The judge sweep shows that the relational class is invisible per action. A complementary question is whether a live agent commits a class that a suitably instrumented guard can catch, and whether the guard that closes it is the composition-aware one rather than a more cautious per-action guard. We run Qwen3-30B as a tool-calling agent on the cumulative-consent calendar task at temperature 0.7, with 60 independent rollouts

TABLE VI L IVE TOOL - CALLING AGENTS ON THE CUMULATIVE - CONSENT TASK (60 INDEPENDENT ROLLOUTS PER CELL AT FIXED TEMPERATURE , ZERO EXECUTION ERRORS ). CAF: CONSENT- COMPOSITION FAILURES COMMITTED . CAF- FREE : FRACTION OF ROLLOUTS WITH NO CAF, A NATURAL RATE UNDER NO GUARD AND A PREVENTION RATE UNDER A GUARD . T HE COMPOSITION - AWARE P5 + GUARD REMOVES EVERY CAF WHILE BLOCKING NO BENIGN OR CLEAN - INTENT ROLLOUTS .

Qwen3-30B guard

CAF

no guard (P0 ) 22/60 intent-closure 20/60 composition (P5 +) 0/60

Gemma-4

CAF-free CAF CAF-free 63.3% 66.7% 100%

0/60 0/60 0/60

100% 100% 100%

per condition, all locally authorized and free of execution errors, under three guards: none, an intent-closure guard that screens each action against the declared purpose, and the composition-aware P5 + guard, which denies an action once cumulative disclosure exceeds the workflow’s consent bound. With no guard, the agent commits the C4 consentcomposition CAF in 22 of 60 rollouts (37%, Wilson 95% CI [26, 49]) and never on a clean-intent baseline or a benign control (0/60 each), so the failure is compositional rather than a local-guard error (Table VI). The intent-closure guard leaves 20/60, 3.3 points below no guard (Newcombe 95% CI [−13.4, 19.8], Fisher exact p = 0.85), as expected, since the disclosure is not visible in any single action’s purpose. The composition-aware guard removes every offending trace (0/60, 33.3 points below intent-closure, CI [21.1, 45.9], p < 10−6 ) while blocking 0/60 benign and 0/60 clean-intent rollouts, so no false positives were observed (one-sided 95% upper bound 4.9% for each control). We read this as the implementation realizing the profile’s intended capability, not as a separate causal finding. A second agent, Gemma-4, never commits the CAF (0/60 throughout): the blind spot is structural, while its exploitation depends on the model. This CAF belongs to the consent-composition class, which closes at P5 +, not to the relational purpose class of the impossibility. For a CAF that a single-execution monitor can catch, the right monitor is the composition-aware one. For the relational class, no single-execution monitor suffices (Table V). What the measurements show together. The studies answer different questions and are not one kind of evidence. The judges and the LangGraph guard exhibit the observationmodel separation itself: blind on one execution, sighted on the pair. The live agent shows a different, catchable class that the matching composition-aware guard closes. The frontier audit reports how one model behaved on the cases we tested, a property that no deployed per-action monitor could have certified. IX. D ISCUSSION Detection requires comparison or false alarms. Singletrace monitors can enforce intent, provenance, consent, and delegation checks when sufficiently instrumented, but not the

relational purpose conjunct without false positives (Corollary 1). A designer has three detection options: accept and review false positives, audit offline with cross-context samples, or monitor relationally by comparing executions. Each has a cost, and a better single-trace guard is not among the options. Prevention lies outside the corollary, because it changes what the agent sees rather than what a monitor checks: generating each disclosure from the purpose-authorized view alone removes the dependence by construction, the agent analogue of secure multi-execution [5], at the price of an extra execution and of any utility the unauthorized context would have added. The model, not the monitor, carries the safety. In our experiments, safety comes from the model’s behavior. The verifiable component, the monitor, is provably blind to the relational class, so deployments rely on an unverifiable, model-specific property that may not survive the next model. This argues for investing in relational monitoring and offline purpose audits. Limitations. Our validation is differential testing on small models, not a proof of correctness and not a scalability study (§VII). The symbolic models are clean and the tasks synthetic, which bounds the empirical claims but not the theorem: the impossibility assumes no model of any API, and noisier tools only add traces, which leaves the singleton fact intact. The symbolic model feeds only the synthesizer, and its witness replays on an agent framework (§VIII). The agent-behavior experiments cover two model families, the nine-model campaign evaluates judges rather than autonomous tool-using agents, and the guardrail matrix is design-derived, a bound whose direction §VIII states. The purpose conjunct is modeled in the declassification style [6] rather than the planning semantics of purpose [21], and we view the two as complementary. Measuring the relational class on realistic multi-tool workloads is the natural next step. X. R ELATED W ORK Hyperproperties and their verification. Clarkson and Schneider [2] introduced hyperproperties and k-safety hyperproperties. Temporal logics for them [9] and model checking [10] followed, with runtime verification of k-safety [11] and a logic for probabilistic hyperproperties [12]. We use this machinery rather than extend it. Enforcement and composition. Schneider’s enforceable policies [3] and the computability classes of enforcement mechanisms [7] delimit what an execution monitor can do. Our Locus theorems instantiate these limits: agent guardrails are execution monitors, and relational purpose lies outside their reach. Noncomposability of security properties [1], the accesscontrol safety problem [22], and noninterference [4] are the roots of the questions we ask. Declassification and purpose. We parameterize purpose by declassification in the sense of Sabelfeld and Sands [6]. Tschantz, Datta, and Wing [21] formalize purpose restrictions through a planning semantics. We see this as complementary to the information-flow view we adopt, and reconciling the two is open.

LLM-agent security. Indirect prompt injection [23] is the overt, single-trace face of agent insecurity, and our C1 experiment lives in that space. Recent defenses are per-execution monitors: task-alignment checking of each action [16], controland data-flow isolation with capabilities [18], and informationflow taint-tracking planners [8]. We place these on our ladder in §VIII. None compares distinct executions of the same purpose, and the strongest of them concedes the gap: Fides [8] enforces explicit secrecy but, by its authors’ own analysis, does not prevent implicit flows through control-flow decisions, which is exactly the relational purpose channel our Locus theorem isolates. XI. C ONCLUSION Local authorization does not compose. We formalized the failure along expressiveness and observability, and proved that the relational purpose violation has no per-trace locus of blame, so no false-alarm-free per-action guard can detect it. AL-S YNTH makes the result constructive: it computes the coverage curve, validated against an exhaustive oracle, and names the observation each CAF class requires. Nine judges and a LangGraph workflow exhibit the separation in practice, a live agent shows the composition-aware guard closing a catchable CAF, and an offline audit finds no leak by a frontier model on the cases tested. The takeaway is a design rule, not a patch: to bound relational purpose, or any policy conjunct that is genuinely relational on the permitted executions, a monitor must compare executions or accept false alarms. E THICS C ONSIDERATIONS AL-S YNTH is dual-use: it synthesizes authorization-evading traces. The risk is bounded because it works over an abstract model the analyst supplies and emits abstract action sequences, not exploits, so using it against a real target already requires a formal model of that target and its monitors. Its purpose is defensive, and the benefit outweighs the marginal uplift to an attacker who already holds such a model. The study used the authors’ own API accounts and local deployments, touched no third-party data or production accounts, and collected no human-subjects data. We release the artifact (https://github. com/anmolpandey299/al-synth) with documentation framing its defensive use. AI D ISCLOSURE Two uses of generative AI are relevant. As a writing aid, a large language model assistant helped draft and edit the prose across all sections. It did not originate the theorems, the synthesizer, or the experimental design, which the authors developed, implemented, and validated, and the authors verified the correctness and originality of all content, including every reference and reported number. Generative AI is also the object of study: §VIII evaluates language models as tool-using agents and as per-action and relational judges, and reports their settings (identifiers in Appendix C). Capable models are necessary because the separation turns on whether disclosures depend on unauthorized

context, which weaker models do not exercise. We minimized query volume, report full counts, and release all logs. Hosted runs used the authors’ own accounts, and open-weights runs a single GPU. A PPENDIX A P ROOFS Lemma 1. Each of C1 , the path form of C3 , C4 , and C5 is of the form {S : ∀t ∈ S. ϕ(t)} for a per-trace predicate ϕ, hence equals [{t : ϕ(t)}] and is trace-induced. Each ϕ is a safety predicate on finite traces with a finite bad prefix (an out-of-intent action, an untrusted-provenance write, an out-ofscope or over-threshold disclosure, an unrevalidated delegated action), so each is a safety property. The labeled-flow form C3lf is 2-safety and not trace-induced; it is enforced not directly but through the single-trace taint-flow property of P6 , which soundly over-approximates it (conservative coverage, not exact). ■ Theorem 1. Singleton fact. For any t, the pair condition in Eq. (1) ranges over t, t′ ∈ {t}, i.e. t′ = t, and equality is reflexive, so {t} ∈ C2D . (1) If (D, α) is collapsing there is no admissible pair ∗ on which the consequent fails, so C2D = 2Σ , which is vacuously k-safety for any k. If (D, α) is nondegenerate, let S ∈ / C2D . Then S contains a, b with low(a) = low(b), D(hi(a)) = D(hi(b)), and α(obs(a)) ̸= α(obs(b)). The pair M = {a, b} is finite, M ⊆ S, and every superset of M also violates C2D ; so M is a 2-trace witness and C2D is 2-safety. (2,⇐) Suppose (D, α) is nondegenerate yet C2D = [T ] for some T . By the singleton fact {a}, {b} ∈ C2D = [T ], so a, b ∈ T , hence {a, b} ⊆ T and {a, b} ∈ [T ] = C2D . But {a, b} ∈ / C2D by choice of the witness, a contradiction. So C2D is not traceinduced. (2,⇒) and (3) Suppose (D, α) is collapsing. Then for every set S and every t, t′ ∈ S the antecedent of Eq. (1) either ∗ fails or the consequent holds, so S ∈ C2D ; thus C2D = 2Σ = [Σ∗ ], which is trace-induced. Hence if C2D is not trace-induced, (D, α) is nondegenerate, and the trivial case is exactly the collapsing one. ■ Theorem 2. Φ = [A] ∩ C2D . Suppose Φ = [U ]. Under RDFDA there are a, b ∈ A with low(a) = low(b), D(hi(a)) = D(hi(b)), α(obs(a)) ̸= α(obs(b)). Since {a}, {b} ⊆ A and singletons satisfy C2D , we have {a}, {b} ∈ Φ = [U ], so a, b ∈ U , hence {a, b} ∈ [U ] = Φ ⊆ C2D . But {a, b} ∈ / C2D , a contradiction. ■ Theorem 3. Let M be per-trace with accepted set [TM ] and false-alarm-free for C2D . By the singleton fact every {t} ∈ C2D , so M may not alarm on any t, i.e. TM = Σ∗ and M accepts every trace. Therefore M flags no trace and detects no violation. ■ Theorem 4. Fix an observable value e = (low, D(hi), y) with y = α(obs) of positive probability. Construct agent A0 whose output is independent of H given (low, D(hi)) and assigns e positive probability, and agent A1 whose output depends on H and also assigns e positive probability under some value of

H. Both are consistent with the single observed e. A soundand-complete monitor must alarm on A1 and not on A0 , but it sees the same e in both, so any fixed decision on e is wrong for one of them. Hence no monitor seeing one such e decides the property soundly and completely over the class of all stochastic agents. ■ Theorem 5. The first two clauses are Theorems 2 and 3 read on the ladder: a P≤6 monitor is single-execution, so it cannot express C2D , and by Theorem 2 it cannot soundly and completely enforce Φ. For the possibilistic property, a P7 monitor compares two executions and exhibits the witness of Theorem 1, crossing the barrier. For the distributional property, the expressiveness dimension is crossed because cross-context sampling represents the comparison a per-trace monitor cannot, while the statistical dimension is not crossed: by a standard indistinguishability argument, for any finite sample there are two agents, one with Y ⊥ H and one without, whose sample distributions are arbitrarily close, so no finitesample test decides independence soundly and completely over all agents. Detection is therefore statistical, not certain. ■ A PPENDIX B M ONITOR -P ROFILE S URVEY We map recent and deployed agent-authorization mechanisms to the profile ladder of §IV. For each, we record from its primary source what per-execution state it observes, whether it compares distinct executions of the same purpose, and the resulting profile. Table II is the result. Every entry is singleexecution: each system inspects the current run (a tool call, its arguments, data-flow or taint labels, or the running plan), and none compares two executions of the same purpose to test whether disclosure depends on unauthorized context. This substantiates the claim that no surveyed monitor reaches P7 . We assign each design the strongest profile its primary source plausibly supports, a deliberately charitable upper bound: under-crediting a mechanism would only widen the gap we report, so generosity makes our conclusion harder to reach, not easier. Task Shield is P1 because it checks each action against the user’s task (per-action intent). RTBAS reaches P3 because it carries information-flow taint and dependency labels (provenance), and we charitably credit it with the weaker intent and purpose-label observables a P3 monitor subsumes. CaMeL reaches P5 because it extracts data and control flow and enforces capabilities (provenance, per-action consent, and delegation scope). Fides and SAFEFLOW reach P6 because they add confidentiality and integrity labels with cross-domain reasoning. In every row the cross-execution column is no for the same structural reason: each mechanism evaluates a single execution and never compares two executions under matched low inputs and declassified context, which is the only way to witness a relational purpose violation. The assignment is thus generous on every axis except the one that matters, and on that axis every surveyed design sits at zero. The most advanced surveyed designs are information-flow systems. Taint tracking is conservative by construction, which places these systems in the false-positive corner of Corollary 1,

and the strongest states its own limit: Fides enforces explicit secrecy but does not prevent implicit flows through controlflow decisions [8]. That residual channel is the relational purpose violation of the Locus theorem, which AL-S YNTH’s relational mode (P7 ) expresses by comparing same-purpose executions. A PPENDIX C J UDGE R EPRODUCIBILITY M ETADATA Table VII records the nine-model judge campaign of §VIII in the detail needed to reproduce it. Eight models were queried through the OpenRouter chat-completions endpoint and one open-weights model through a local vLLM server. Every request fixed the sampling temperature at 0 and allowed a 4000-token generation budget, so that reasoning-heavy models had room to deliberate before emitting a verdict. Requests used OpenRouter’s default routing: we did not pin a serving provider or disable fallback, so a given slug may have been dispatched to whichever provider OpenRouter selected at request time, a reproducibility caveat we state explicitly. The per-judge and per-scenario counts behind Table V, together with every raw model response, are released with the artifact. TABLE VII J UDGE MODELS AND EXACT API SLUGS FOR THE CAMPAIGN OF §VIII; SETTINGS IN THE TEXT, ACCESSED J UNE 2026.

Display name

API slug

Claude Opus 4.8 GPT-5.5 Gemini 3.1 Pro Grok 4.3 DeepSeek V4 Pro Qwen3.7-max Llama-4-Maverick Kimi-K2.6 Qwen3-30B∗

anthropic/claude-opus-4.8 openai/gpt-5.5 google/gemini-3.1-pro-preview x-ai/grok-4.3 deepseek/deepseek-v4-pro qwen/qwen3.7-max meta-llama/llama-4-maverick moonshotai/kimi-k2.6 Qwen/Qwen3-30B

∗ Served locally via vLLM on a single GPU; all other models through the

OpenRouter chat-completions endpoint.

R EFERENCES [1] D. McCullough, “Noninterference and the composability of security properties,” in IEEE Symposium on Security and Privacy (S&P), 1988, pp. 177–186. [2] M. R. Clarkson and F. B. Schneider, “Hyperproperties,” Journal of Computer Security, vol. 18, no. 6, pp. 1157–1210, 2010. [3] F. B. Schneider, “Enforceable security policies,” ACM Transactions on Information and System Security, vol. 3, no. 1, pp. 30–50, 2000. [4] J. A. Goguen and J. Meseguer, “Security policies and security models,” in IEEE Symposium on Security and Privacy (S&P), 1982, pp. 11–20. [5] D. Devriese and F. Piessens, “Noninterference through secure multiexecution,” in IEEE Symposium on Security and Privacy (S&P), 2010, doi: 10.1109/SP.2010.15. [6] A. Sabelfeld and D. Sands, “Declassification: Dimensions and principles,” Journal of Computer Security, vol. 17, no. 5, pp. 517–548, 2009. [7] K. W. Hamlen, G. Morrisett, and F. B. Schneider, “Computability classes for enforcement mechanisms,” ACM Transactions on Programming Languages and Systems, vol. 28, no. 1, pp. 175–205, 2006. [8] M. Costa et al., “Securing AI agents with information-flow control,” arXiv:2505.23643, 2025.

[9] M. R. Clarkson, B. Finkbeiner, M. Koleini, K. K. Micinski, M. N. Rabe, and C. Sánchez, “Temporal logics for hyperproperties,” in Principles of Security and Trust (POST), 2014, pp. 265–284. [10] B. Finkbeiner, M. N. Rabe, and C. Sánchez, “Algorithms for model checking HyperLTL and HyperCTL∗ ,” in Computer Aided Verification (CAV), 2015, pp. 30–48. [11] S. Agrawal and B. Bonakdarpour, “Runtime verification of k-safety hyperproperties in HyperLTL,” in IEEE Computer Security Foundations Symposium (CSF), 2016, pp. 239–252. [12] E. Ábrahám and B. Bonakdarpour, “HyperPCTL: A temporal logic for probabilistic hyperproperties,” in Quantitative Evaluation of Systems (QEST), 2018, pp. 20–35. [13] A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu, “Bounded model checking,” in Advances in Computers, 2003, vol. 58, pp. 117–148. [14] L. de Moura and N. Bjørner, “Z3: An efficient SMT solver,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008, pp. 337–340. [15] G. Barthe, P. R. D’Argenio, and T. Rezk, “Secure information flow by self-composition,” in IEEE Computer Security Foundations Workshop (CSFW), 2004, pp. 100–114. [16] F. Jia, T. Wu, X. Qin, and A. Squicciarini, “The Task Shield: Enforcing task alignment to defend against indirect prompt injection in LLM agents,” in Annual Meeting of the Association for Computational Linguistics (ACL), 2025, pp. 29 680–29 697. [17] P. Y. Zhong et al., “RTBAS: Defending LLM agents against prompt injection and privacy leakage,” arXiv:2502.08966, 2025. [18] E. Debenedetti et al., “Defeating prompt injections by design,” in IEEE Conference on Secure and Trustworthy Machine Learning (SaTML), 2026. [19] P. Li et al., “SAFEFLOW: A principled protocol for trustworthy and transactional autonomous agent systems,” arXiv:2506.07564, 2025. [20] LangChain AI, “LangGraph: Build resilient language agents as graphs,” GitHub repository, 2026, [Online]. Available: https://github. com/langchain-ai/langgraph. Accessed: Jun. 7, 2026. [21] M. C. Tschantz, A. Datta, and J. M. Wing, “Formalizing and enforcing purpose restrictions in privacy policies,” in IEEE Symposium on Security and Privacy (S&P), 2012, pp. 176–190. [22] M. A. Harrison, W. L. Ruzzo, and J. D. Ullman, “Protection in operating systems,” Communications of the ACM, vol. 19, no. 8, pp. 461–471, 1976. [23] K. Greshake, S. Abdelnabi, S. Mishra, C. Endres, T. Holz, and M. Fritz, “Not what you’ve signed up for: Compromising real-world LLMintegrated applications with indirect prompt injection,” in ACM Workshop on Artificial Intelligence and Security (AISec), 2023, pp. 79–90.

Related documents

• Local Allow, Global Deny: Why Per-Action Authorization Does Not Compose in LLM Agents#1403416
• AGATE: Provenance-Based Runtime Defense Against Compositional Attacks on LLM Agents#1105389
• AgentSecBench: Measuring Prompt Injection, Privacy Leakage, and Tool-Use Integrity in LLM Agents#229449
• Trust No Tool: Evaluating and Defending LLM Agents under Untrusted Tool Feedback#200400
• AgentProv: Auditing Agentic LLM API Providers via Tool-use Policy Probes#819536