Agenra: A Language and Verified Core for Stateful LLM Agent Authorization

The gist: AgentFlow presents a flow-centric policy language and enforcement model for specifying where data may travel through an agent system, which reduces confirmed compromise from 33.0% to 0.0% on AgentDojo and improves aggregate utility from 46.7% to 63.3%

AgentFlow Overview

AgentFlow is a flow-centric policy language and framework for securing LLM agent systems that enforces data-flow and path constraints over agent executions through a runtime monitor and pre-deployment checks The framework is organized around three ideas: Flow rules for agent actions, A multi-dimensional label lattice, and Path rules for history-aware security Flow rules state constraints on labeled execution edges such as which tools may receive sensitive fields, which sinks may receive released data, and what authority may cross a delegation boundary The multi-dimensional label lattice annotates every data node with sensitivity, category, and trust metadata to distinguish public-but-untrusted web text from trusted-but-confidential customer data Path rules support reasoning about multi-step behavior by evaluating constraints over lineage-connected paths or broader session histories

Policy Language Design

The AgentFlow language is organized around four core concepts: label system, flow graphs, flow rules, and path rules The label system defines a label L as a triple ⟨s, C, t⟩ where Sensitivity controls disclosure levels (Public to TopSecret), Categories distinguish fields such as email addresses from SSNs or credentials, and Trust indicates whether content came from an untrusted source The trust constraint ensures that untrusted data can only flow to untrusted contexts, defined by the relation ⊑ where l1 ⊑ l2 means s1 ≤ s2 and C1 ⊆ C2 and (t1∨¬t2) Flow rules define policy constraints over information flows in the graph, where a flow rule either permits or denies a flow when a collection of predicates over nodes, edges, labels, agents, and runtime state are satisfied Path rules constrain multi-step data flow by matching temporal patterns over execution traces using expressions like πe which describes how information-flow events are expected to occur over time within a trace

Formal Semantics and Enforcement

The runtime execution evolves over mutable runtime states that maintain taint information, execution traces, lineage relations, active task scopes, requirements, and capabilities The operational semantics define how runtime execution evolves by intercepting requests, computing propagated labels according to edge propagation semantics (e.g., ◁from or ⇝ (r)), evaluating flow and path policies against candidate steps, and updating the runtime state accordingly A policy decision is computed by evaluating flow clauses and path clauses against the candidate step, where a candidate step is allowed when it satisfies all required conditions including matching no deny-flow clause or not violating any forbidden path expression The runtime transition semantics define the behavior of AgentFlow by combining label resolution, propagation semantics, policy evaluation, and runtime state evolution

Static Verification

Beyond runtime enforcement, AgentFlow checks bounded policy properties by reducing them to satisfiability modulo theories (SMT), following the approach pioneered by AWS Zelkova The SMT verifier translates a policy set and a bound k into Z3 constraints and checks the safety properties summarized below The verifier checks seven safety properties, including non-leakage, privilege escalation resistance, trust-preserving flows, delegation safety, and taint monotonicity The prototype rebuilds the SMT encoding from scratch for each verification run; in preliminary evaluation, these full reruns complete in under 0.5 seconds per checked property

Evaluation Results

On 949 AgentDojo injected test cases across four suites, AgentFlow reduces confirmed compromise from 33.0% to 0.0% while improving aggregate utility from 46.7% to 63.3% On a 200-case AgentDyn Dailylife stress test, it reduces confirmed compromise from 73.5% to 0.0% while preserving near-baseline utility (44.5% to 43.5%) Breadth checks across ASB, InjecAgent, BIPIA, AgentHarm, and MCPTox-style replays suggest that the configured policies block the benchmark-specified policy-visible attacker flows; in ASB’s upstream direct-prompt-injection harness, attack success is 0/1,200 The results are preliminary and scoped to modeled policy-visible agent behaviors and evaluated benchmarks

Comparison with Related Defenses

AgentFlow differs from related defenses like FIDES, CaMeL, FORGE, and SAMOS by exposing a standalone policy layer over labeled edges and histories, together with bounded checks for the supported policy fragment The runtime overhead for core policy decision-making is negligible at an average per-intercept latency of 6.4 µs The SMT verifier verifies properties in under 0.5 seconds, which is comparable to other policy-facing mechanisms like FIDES and CaMeL

Limitations

The main limitation is overtainting in message-heavy workflows when an LLM processes a tainted tool result, as the runtime may conservatively propagate that taint because it cannot recover exact token-level dependencies Task classes that require care include those that intentionally forward untrusted web content to an external sink or combine private records with attacker-controlled instructions, which require explicit release contexts AgentFlow’s SMT verifier gives a priori guarantees for the verifier’s bounded, structured abstraction, not for arbitrary LLM behavior outside the modeled tool and response-sink interface The guarantee scope is useful in practice because the verifier checks policy properties before deployment while the runtime monitor enforces those policies on mediated actions

Related Work

The paper focuses on work shaping AgentFlow, including attacks on tool-using agents, agent defenses, authorization and IFC, and policy analysis It draws from prompt injection and tool misuse studies like AgentDojo [16] and InjecAgent [19], as well as defenses such as Progent [9], SEAgent [7], AgentArmor [10], and Conseca [11] It also draws on authorization systems like Cedar, XACML, Zanzibar, and Datalog-based authorization to track how content obtained in one step may influence a later agent action or sink It also draws on classical IFC from Denning and Myers and Liskov to inform the propagation model It applies SMT and symbolic techniques, similar to those used by Zelkova, Margrave, FIREMAN, and cloud-policy verification to analyze authorization policies The runtime enforcement follows the reference-monitor tradition characterized by Schneider

Conclusion

AgentFlow presents a policy language and runtime monitor for controlling how data moves through tool-using LLM agents By tracking labels, provenance, and execution history across tool calls, AgentFlow lets operators express constraints that request-level checks miss, including multihop exfiltration, trust laundering, unsafe delegation, and temporal attack patterns In the current prototype and evaluation, runtime enforcement with bounded SMT checks blocks the policy-visible attacks examined in our benchmarks while preserving useful task completion under the configured policies This report provides a concrete technical and formal foundation for this design, along with preliminary evaluation evidence that motivates further application-specific development and validation

References

[1] S.

1. Improve data flow control by implementing AgentFlow to enforce policies over labeled runtime edges, which allows specifying which tools may receive sensitive fields and which sinks may receive released data. This enables prevention of harm like data exfiltration, even when individual steps appear legitimate, by tracking taint through the system.

2. Enhance delegation safety by using AgentFlow's path rules to constrain multi-step behavior, specifically preventing patterns like reconnaissance-then-exfiltration, which is difficult to express with request-level permissions alone. This prevents unauthorized data flow across delegation boundaries where sub-agents might receive data they should not see.

3. Implement a bounded SMT verifier for pre-deployment checks to ensure policy correctness, as the paper states it checks safety properties, including non-leakage, privilege escalation resistance, trust-preserving flows, delegation safety, and taint monotonicity. This provides a formal guarantee that the structured policy fragment is sound before deployment.

4. Strengthen trust preservation by utilizing the label system where trust records whether content came from an untrusted source, ensuring that untrusted data may only flow to untrusted contexts as defined by the relation l1 ⊑ l2. This prevents trust laundering by blocking untrusted data from reaching trusted destinations without explicit reclassification.

5. Enforce task-scoped least privilege by using task scopes, which can constrain which edges an agent is permitted or forbidden to invoke within a specific execution context. This addresses the need for policies that require sanitization before external release by dynamically adjusting permissions based on the current task, as seen in AgentDyn stress tests.

6. Develop a runtime reference monitor that intercepts tool calls and modeled response sinks to evaluate flow and path rules, returning a decision of ALLOW, DENY, or PAUSE. This provides real-time enforcement by checking policies against the current execution trace to ensure every step satisfies the constraints before committing it.

Applications that deploy LLM agents keep revising the permissions their agents use. When authority is consumable, even widening a permission can break a legitimate workflow, because an early call may use up a grant that a later call needs. Checking individual requests, or watching one run succeed, misses this. We present Agenra, a policy language with a Lean enforcement core that tracks the values each call uses, resources discovered at run time, and authority consumed by earlier calls. Agenra treats safety and workflow preservation as separate properties. Our key idea is to certify a revision with a simulation between the old and new permission ledgers. Quota increases, appended grants and independent reorderings admit such simulations by construction, and Lean checks proposed simulations for other finite-quota revisions. The proofs use the deployed matching predicates and extend through the full monitor, covering discovered resources, payloads that are never enumerated, failed calls and approvals. They assume serialized calls and identical service results under both policies, and they trust the Python translation layer. On 51 authored revisions, the checks certify all 21 that preserve their clients and none of the 30 that do not, and every lost workflow is confirmed by replay. They also certify a real quota increase from an open-source agent application. In a report-delivery application, raising the send quota preserves every client yet permits a second approved send, so preservation does not imply safety.