Local pass, global reject: why per-action authorization cannot be composed in LLM Agents

Per-action authorization cannot compose into global authorization.

• Scenario: A single LLM agent calls tools within a bounded episode, and local predicates approve each call one at a time. The authors hold that the user authorizes the whole episode, not a sequence of separately approved steps.
• Insufficiency: The authors state that guardrails are single-trace execution monitors. A per-action monitor that never false-positives cannot detect relational purpose violations, regardless of the model or decision process; the authors view this as an expressiveness gap, not an engineering gap.
• Observation: A CAF is an execution, or a pair of executions, of local authorization that violates the global policy. Relational purpose violations have no point of attribution on a single trace. In the scheduling example, being approved to share the busy/free view does not equal disclosing the reason for being busy.
• Approach: Characterize eight subclasses along expressiveness and observability, and give the above undetectability. AL-SYNTH does not use language models and synthesizes minimal witnesses with SAT/SMT.
• Threat model:
  • Goal: A trace that passes all local checks yet violates Φ. No jailbroken or locally misbehaving agent is assumed.
  • Capability: An agent that looks benign and has legitimate purposes, whose compositional behavior conveys information or permissions not granted by its purpose. An adversary can influence it through task wording or injected content in tool results, without breaking local guardrails.
  • System: A single agent executes a bounded episode, actions come from a typed action set, and the environment state can change. Local authorization abstracts per-action guardrails, permission prompts, and tool-call monitors.
  • Policy: Φ conjoins intent, purpose, provenance, consent, and delegation. Four are single-trace properties, and the purpose conjunction requires comparing runs.

Hyperproperties and verification

• k-safety: Clarkson and Schneider (2010) define hyperproperties; a counterexample to k-safety is k finite traces. Noninterference is a typical 2-safety property.
• Verification tools: hyperproperty temporal logic (Clarkson et al., 2014), HyperLTL and HyperCTL* model checking (Finkbeiner et al., 2015), k-safety runtime verification (Agrawal and Bonakdarpour, 2016), and the probabilistic logic HyperPCTL (Ábrahám and Bonakdarpour, 2018).
• Usage: the authors state that they use this machinery rather than extend it.

Monitoring and composition

• Execution monitoring: Schneider (2000) defines what execution monitoring can enforce; Hamlen, Morrisett and Schneider (2006) give the computable classes of enforcement mechanisms. The authors state that the Locus theorem applies this bound to agent guardrails.
• Classical roots: McCullough (1988) notes that safety properties need not be composable; Goguen and Meseguer (1982) define noninterference; Harrison, Ruzzo and Ullman (1976) discuss access control safety problems.
• Multiple executions: Devriese and Piessens (2010) enforce noninterference using one execution per security level. The introduction states that these components are classical and that this paper does not count them as new contributions in themselves.

Declassification and purpose

• Declassification: Sabelfeld and Sands (2009) discuss dimensions and principles of declassification. The authors parameterize purpose with a declassification function.
• Planning semantics: Tschantz, Datta and Wing (2012) formalize purpose limitation using planning semantics. The authors consider this complementary to the information-flow view, and reconciliation remains open.

Agent security

• One side of a single trace: indirect prompt injection from Greshake et al. (2023) is called by the authors the explicit, single-trace side; the C1 experiments in this paper fall within that scope.
• Per-execution defenses: Task Shield (Jia et al., 2025) checks actions against the task; CaMeL (Debenedetti et al., 2026) uses capability isolation of data and control flow; Fides (Costa et al., 2025) performs information-flow taint tracking. The authors place them on the profile ladder.
• Difference from this paper: the authors state that none of these works compares different executions of the same purpose. Fides' own analysis states that it enforces explicit confidentiality but does not prevent implicit flows on control-flow decisions; the authors state that this residual is the relational purpose channel.

Baselines and tasks

• Surveyed systems: per-tool approval, Task Shield, RTBAS (Zhong et al., 2025), CaMeL, Fides, SAFEFLOW (Li et al., 2025). The authors assign them to profiles by their published design and do not run their implementations.
• Experimental controls: no guardrails, intent-closed guardrails, P5+ combined guardrails; on the reviewer side there is a benign no-leak control, an explicit single-trace C1 control, and a relational audit that sees two executions.
• Tasks: synthetic schedule relational witnesses, a cumulative-consent calendar task, a LangGraph schedule flow, and three types of offline audit with Claude Sonnet 4.6.

The authors state that what is new is the implication of these facts for agent authorization: the policy splits into a trace-safety part and a relational purpose part; under the stated non-collapse conditions, per-trace monitoring that never raises false alarms cannot detect the latter. All surveyed guardrails are on the trace-safety side.

The authors define the failure as compositional authorization failure (CAF), classify it by expressiveness and observability, and then synthesize minimal witnesses with AL-SYNTH, which does not use a language model.

Problem setting and global policy

• Transition system: a state assigns values to finitely many typed variables. Actions have guards and effects. Starting from the initial state, if the guard holds at each step, a finite trace is locally authorized.
• Projection: low is the declared purpose and other low inputs, hi is readable sensitive context, obs is outward disclosure.
• Five conjuncts: Φ conjoins intent C1, purpose C2D, provenance C3, consent C4, delegation C5. Lemma 1 states that C1, the path form of C3, C4 and C5 are single-trace safety properties. The explicit label flow C3lf is itself 2-safety, and P6 uses taint tracking as a conservative cover.
• Purpose: D is the context view of purpose authorization, α is the policy-relevant part of disclosure. Equation (1) in the main text is

C₂^D={S:∀ t,t′∈ S. low(t)=low(t′)∧ D(hi(t))=D(hi(t′))⇒α(obs(t))=α(obs(t′))}

that is: for two runs with the same low inputs and the same purpose-authorization view, the policy-relevant disclosures must be the same.

• Parameters: (D, α) are given by the policy. The authors state that Theorem 3 holds for every pair; a violation exists if and only if the pair remains non-degenerate (Definition 2, Theorem 1). A wrong choice only changes which disclosures are flagged and cannot make a nontrivial purpose conjunct visible to per-action guardrails that never raise false alarms. Residual disclosure freedom RDF-D means there exist finite traces with the same low and D(hi) but different α(obs); when the witness also lies in the locally authorized set A, it is denoted RDF-DA.

Two-axis characterization

• Expressiveness: witnesses for single-trace classes are finite bad prefixes; relational classes are k-safety hyperproperties. Intent, path provenance, consent and delegation are single-trace. C2D is relational.
• Profiles: P0 is pure black box. After it come, in order, intent approximation, information flow and purpose labeling, provenance graph, per-action consent, delegation re-verification, and cumulative summaries of intent and consent.
• Two ends: P6 adds cross-domain state transitions and is the strongest single-execution instrumentation the authors consider. P7 is the only profile that can compare different executions.
• Detection: it must both express the class and observe the state it depends on. Figure 2 places eight subclasses on the two axes; the bottom row's undetected count goes from 8 to 0 from P0 to P7 (including P5+).

Separation results

• Theorem 1: for any D and α, C2D is 2-safety; it is not induced by a trace property if and only if (D, α) remains non-degenerate; if it collapses, every system satisfies it.
• Singleton fact: equality is reflexive, so any single-trace set satisfies C2D. The two traces in a violating pair are each compliant; the fault lies only in their relation.
• Theorems 2 and 3: if a residual non-degenerate witness remains in A, then Φ=[A]∩C2D is not induced by a trace property. Theorem 3 states that per-trace monitoring that never raises false alarms for C2D cannot flag any trace and therefore cannot detect violations.
• Distribution and P7: Theorem 4 states that, under the stated single-run observables, no monitor can both soundly and completely decide, for all stochastic agents, that disclosure and undeclassified context are conditionally independent. Theorem 5 states that P≤6 can neither soundly and completely enforce Φ nor soundly detect C2D; for possibilistic properties, P7 can exhibit two-trace witnesses, and for distributional properties only statistical detection. Corollary 1 lists only three responses: tolerate false alarms, audit offline across contexts, or compare executions.

AL-SYNTH

• Goal: given a model and a target class, output a minimal witness that is locally authorized at each step and globally unauthorized; for a specified profile, it must also evade the checks that profile can express and observe. The engine is symbolic and does not use a language model.
• Dual semantics: the same transition system has a reference semantics and an SMT encoding. The solver performs bounded model checking, and the oracle enumerates. The two should induce the same CAF; consistency is tested, not assumed.
• Solving: at bound n, encode the initial state, variable ranges, transitions and stepwise local authorization, then conjoin the final-state violation. Minimal witnesses are found by increasing the bound, with one satisfiability query per bound. all-SAT is used only for completeness checks.
• Relational witnesses: self-compose two copies of the system and assert that low and D(hi) are equal and α(obs) is not, i.e. the negation implied by Equation (1). The existence query is SAT. To evade profile P, the negations of P's individual safety checks are placed in the same query rather than filtered afterward. The validation criteria are T1 soundness, T2 bounded completeness, T3 minimality; results are in the experiments.

Experimental setup

• Models under test: The reviewers are 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, and local Qwen3-30B. The offline audit agent is Claude Sonnet 4.6. The live tool-calling agents are Qwen3-30B and Gemma-4.
• Tasks: The shared trace of the scheduling model is collect, aggregate, report; world a provides slot 10, world b provides slot 11. The live task is the cumulative-consent calendar task. The LangGraph graph is read, aggregate, propose. The three offline types are Injected-doc forward (C1), Narrow-scope share (C4), and Scheduling audit (C2r).
• Reviewer protocol: Temperature 0, generation budget 4000 tokens. Ten scenarios vary the slot pair, the hidden reason, the task wording, and the A/B order, each repeated 3 times, for 30 scenario repetitions in total; repetitions measure stability rather than coverage. Hosted models go through OpenRouter's default routing, with the provider not fixed; local models go through vLLM. The appendix states the access time as June 2026.
• Live protocol: Temperature 0.7, 60 independent rollouts per cell, execution errors 0. The guardrails are no guardrail (P0), intent closure, and P5+, which rejects once cumulative disclosure exceeds the consent bound.
• Offline protocol: Claude Sonnet 4.6 acts as the tool-calling agent at a fixed temperature; the main text does not give the value of that temperature. C2r keeps the busy/free view fixed, the two conditions differ only in the hidden reason, and a high share rate is used as a gate so that an empty result reflects disclosure rather than refusal. The upper bounds are exact one-sided 95% Clopper–Pearson.
• Other: The six guardrails do not run implementations and are placed in the strongest profile according to their published designs. The synthesizer is Z3, checked against an exhaustive oracle. The cells of Table V are the number of times at least one action was blocked out of 30 scenario repetitions.

Main results

Swipe horizontally to read the table

According to Table V. Qwen3.7-max is omitted; its four cells are 0/30, 0/30, 30/30, 30/30, the same as Claude Opus 4.8. Llama-4-Maverick, the lowest in the relational audit column, is included.

• The authors state that Kimi-K2.6's blocks are at the same level as benign blocks, being single-step conservatism rather than relational detection, because per-action review cannot see the second execution. Its single-step counts are 3/180 for witnesses and 1/180 for benign, and DeepSeek's benign is 2/180, with a definition different from the table above.
• The authors state that all nine models block the explicit single-trace C1, so it is not a blanket allow. The same models recover detection after seeing two executions; the authors state that Llama-4-Maverick separates the relational observability of P7 from relational detection, which remains a model capability.
• The authors state that this table is a separation of observation and model, not nine independent vulnerabilities. By Theorem 3, the per-action blind spot does not depend on the single-execution decision process.

Coverage curve and defense matrix

• What was measured: For each profile × each subclass, the solver either synthesizes a witness that the profile cannot see, or determines that none exists within the bound. The solver and the oracle agree on all 9×8 cells (Table I).
• Curve: The number of undetected cases from P0 to P7 is 8, 7, 6, 5, 4, 3, 2, 1, 0. Up to P6, the remainder is exactly the relational purpose class. Explicitly marked flows are conservatively covered at P6 and above. After removing purpose markers the curve is [8, 7, 7, 6, 5, 4, 3, 2, 1], and it returns to the original curve after restoration.
• Design upper bounds: The authors did not run the six implementations. In Table III, per-tool approval covers none of the eight classes, RTBAS three classes, CaMeL five classes, and Fides and SAFEFLOW seven classes (six exact, explicitly marked flows conservative). The relational purpose column is uncovered for all six, and only the P7 relational audit covers it. The authors state that running the implementations cannot raise that column without comparing executions or accepting false positives.

Live consent composition

• What was measured: Qwen3-30B and Gemma-4 on the cumulative-consent task, 60 rollouts each, with three guardrail sets (Table VI). This class is consent composition, closed at P5+, not the relational purpose class of Theorem 3.
• Numbers: With no guardrail, Qwen3-30B is 22/60 (37%, Wilson 95% CI [26, 49]), and both the clean-intent and benign controls are 0/60. Intent closure is 20/60, 3.3 percentage points lower than no guardrail (Newcombe 95% CI [-13.4, 19.8], Fisher exact test p=0.85). P5+ is 0/60, 33.3 percentage points lower than intent closure (CI [21.1, 45.9], p<10^{-6}), and both benign and clean-intent blocks are 0/60; the one-sided 95% upper bound for each control is 4.9%. All three cells for Gemma-4 are 0/60.
• Authors' interpretation: The authors state that the disclosure is invisible in any single-step purpose, so the difference under intent closure falls in an interval containing 0; P5+ removes all violating traces. The authors read this as the profile achieving the intended capability, not as a separate causal finding. The blind spot is structural, and whether it appears depends on the model.

Offline audit and LangGraph

• Sonnet: Table IV, fixed temperature. C1 and C4 are both n=10, CAF=0, upper bound ≤26%. C2r is n=80, with CAF=0 under the policy-relevant abstraction α, upper bound ≤3.7%.
• Retracted positive example: The authors state that the initial analysis reported a covert signal stable across seeds; inspection of the raw output found that the two conditions provided the same set of slots, and the signal came from the feature extractor counting a differently worded word. Under α of Eq. (1), the channel is clean. The authors keep this episode because the safety result holds only under the abstraction that tracks the policy.
• LangGraph: The per-action guardrail includes tool permissions, purpose markers, provenance, and per-action consent. The two worlds share the authorized busy/free view and differ only in the hidden reason. The guardrail returns allow, allow, allow in both worlds, with different action parameters; the provided slots are 10 and 11 respectively. The AL-SYNTH relational audit flags C2D. The authors state that they do not claim LangGraph has a vulnerability.

Other ablations and analyses

• Minimal witness synthesis on the cumulative-consent model (11 actions, Z3 4.16) takes about 0.02 to 0.07 s up to depth 12; all-SAT at depths 3 to 7 goes from 1 to 29,337 witnesses and from 0.02 s to 118 s, and the main text states a difference of about 2,770× at depth 7. Figure 5 also labels 2,781 and ∼2,770×. The authors state that the timings are illustrative, not a benchmark.
• T1, T2, and T3 pass for every class, including the relational class; the minimal pairs of self-synthesized witnesses and the oracle agree (§VII).
• Oracle agreement only checks two encodings, and the authors state that it does not show that the semantics correctly characterizes a deployment (§VII).

Limitations and future directions noted by the authors

• Differential testing: The authors state that the validation is differential testing on small models, not a proof of correctness, nor a scalability study (§IX, pointing to §VII).
• Synthetic tasks: The symbolic model is clean and the tasks are synthetic, which constrains the empirical claims but not the theorems; noisier tools only add traces, and the single-instance facts remain (§IX).
• Supply scope: The symbolic model only supplies the synthesizer, whose witnesses are replayed on the agent framework (§IX).
• Model roles: The agent behavior experiments cover two model families; the nine-model activity evaluation assesses reviewers, not autonomous tool-using agents (§IX).
• Design upper bounds: The guardrail matrix is derived from design and is a directional bound; the direction is explained in §VIII (§IX).
• Purpose semantics and next steps: Purpose is modeled in a declassification style rather than planning semantics; the authors view the two as complementary. Measuring the relational class on real multi-tool workloads is a natural next step (§IX).

Experimental coverage

• Reviewers: The nine models of Table V, temperature 0, 3 runs each for ten templates, budget 4000 tokens; hosted models go through OpenRouter's default routing, and the paper states that the provider was not fixed (§VIII, Appendix C).
• Live: The tool-calling agents are Qwen3-30B and Gemma-4, cumulative-consent task, temperature 0.7, 60 rollouts per cell, execution errors 0; the guardrails are no guardrail, intent closure, and P5+ (Table VI).
• Offline: The sample sizes for Claude Sonnet 4.6 on the three task types are 10, 10, and 80 respectively; the main text only states a fixed temperature and does not give the value (Table IV).
• Guardrail placement: The six mechanisms are assigned to profiles according to their published designs; the authors did not run their code; the cross-execution column is No for all (Table II, Appendix B). The relational audit is P7 of AL-SYNTH.
• Synthesis: The solver and the exhaustive oracle agree on 9 profiles × 8 subclasses; the timings come from an 11-action cumulative-consent model, Z3 4.16, and the authors state it is not a benchmark (Table I, Figure 5). The LangGraph section does not report the number of repetitions.

• Positioning: The authors analyze why per-action authorization for LLM agents does not yield global authorization for a whole episode, and call such witnesses compositional authorization failures (CAF).
• Problem: The global policy conjoins intent, purpose, provenance, consent, and delegation. The purpose conjunction is a 2-safety hyperproperty: two runs can have the same low inputs and purpose-authorization view and still differ in disclosure, and no single trace is attributable.
• Result form: The monitoring profile ranges from pure black-box P0 to P7, which can compare executions. The authors give: a per-trace monitor that never false-positives on the purpose class cannot detect that class, regardless of the underlying model or decision process. To constrain it, one must compare executions or accept false positives. AL-SYNTH uses Z3 and self-synthesis to generate minimal witnesses, not language models, and checks against an exhaustive oracle.
• Reviewers: Apart from Kimi-K2.6's 3/30, the eight reviewers in Table V have 0/30 per-action blocks on synthesized relational witnesses; after seeing two executions, eight are 30/30 and Llama-4-Maverick is 17/30. All nine models are 30/30 on the explicit single-trace C1.
• Live and audit: Qwen3-30B exhibits consent-composition CAF in 22/60 runs with no guardrail, and 0/60 with P5+; Gemma-4 is 0/60 (Table VI). Claude Sonnet 4.6 has CAF 0 on the three tested types, with an upper bound ≤3.7% for C2r at n=80 (Table IV). The published designs of the six investigated guardrails do not compare two executions.
• Authors' conclusion: The authors state that per-action authorization is structurally insufficient for relational conjunctions that cannot be reduced to single-trace safety. Safety in the experiments comes from model behavior; a verifiable single-execution monitor is blind to the relational class, so deployment depends on properties that vary by model and cannot be verified by that monitor.