AgentFlow: A Flow-Centric Policy Language and Framework for Securing LLM Agent Systems

AgentFlow: A Flow-Centric Policy Language and Framework for Securing LLM Agent Systems Basavesh Ammanaghatta Shivakumar Virginia Tech

Swarn Priya Virginia Tech

Peng Gao Virginia Tech

arXiv:2608.22868v1 [cs.CR] 24 Aug 2026

August 25, 2026

Abstract LLM agents increasingly read untrusted content, invoke external tools, access private data, and delegate work to other agents. In these systems, harm often comes not only from obviously dangerous tool calls, but from how data moves through a sequence of otherwise plausible actions. A confidential record summarized by an LLM and then sent in an outgoing email can violate policy even if each step appears locally legitimate. In this technical report, we present AgentFlow, a flow-centric policy language and enforcement model for specifying where data may travel through an agent system. AgentFlow expresses policies over labeled runtime edges: which tools may receive sensitive fields, which sinks may receive released data, and what authority may cross delegation boundaries. The language supports flow and path rules, task-scoped capabilities, controlled release, and stateful taint semantics. A runtime reference monitor enforces these policies on mediated actions. We give a formal model for AgentFlow and a bounded SMT-based verifier for a structured policy fragment. In our prototype evaluation, the verifier catches all seeded unsafe policy variants in our study, and seven safety properties verify in under 0.5 seconds each. 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. These results are preliminary and are scoped to the modeled policy-visible agent behaviors and the evaluated benchmarks.

1

Introduction

LLM-based agent systems now routinely plan, invoke tools, and interact with external services on a user’s behalf [1, 2, 3]. This delegated authority makes agent failures qualitatively different from ordinary access-control mistakes: the dangerous behavior often emerges across a sequence of plausible steps [4]. Consider a customer-support agent with access to a user database and an email tool. Reading a customer’s record is legitimate. Sending email is legitimate. Reading a customer’s Social Security number and sending it to an external address is data exfiltration. Indirect prompt injection makes this pattern especially risky: an attacker-controlled web page, email, document, or tool output can instruct the agent to combine private reads with external writes that the user never intended [5, 6]. Similar failures arise when untrusted content is treated as an internal directive, when a high-privilege agent delegates sensitive context to a weaker sub-agent, or when reconnaissance is followed by targeted exfiltration [7, 6]. 1

Policy requirement. Request-level authorization languages such as Cedar [8] are well suited to deciding whether a principal may perform an action on a resource. Agent systems need that check, but also need to remember where data came from, how it was transformed, and which later actions it may influence. Request-level authorization does not provide this end-to-end data-flow state by itself. This paper introduces a policy layer for specifying when sensitive or untrusted content may influence later tool calls, response sinks, and delegation steps. Recent defenses address parts of this problem. Progent [9] controls tool privileges; SEAgent [7] studies privilege escalation through delegation; AgentArmor [10] analyzes runtime traces; and Conseca [11] generates contextual task policies. Concurrent systems such as FORGE [12], FIDES [13], CaMeL [14], and SAMOS [15] explore related enforcement designs. These systems improve agent safety, but they make different design choices about where policies live and how they are checked. The goal of this paper is not to claim that information-flow control or reference monitoring is new. Rather, AgentFlow asks how to make these ideas usable as an explicit policy layer for modern agent deployments, where the operator may not control the agent architecture, tools are registered dynamically, and security decisions must account for tool calls, delegated sub-agents, response sinks, and multi-step histories. This leads to a different interface from architecture-specific defenses: policies are written over labeled runtime edges and checked both during execution and, for a bounded fragment, before deployment. This report is intentionally scoped to policy-visible mediated agent behaviors: the reference monitor enforces the configured policy interface for tool calls, delegated actions, and modeled response sinks, and the bounded verifier checks safety properties for the structured policy fragment. It does not claim to solve every unsafe LLM behavior or every agentic failure mode. AgentFlow overview. We present AgentFlow, a flow-centric policy language and framework for securing LLM agent systems. AgentFlow enforces data-flow and path constraints over agent executions through a runtime monitor and pre-deployment checks. The framework is organized around three ideas: 1. Flow rules for agent actions. Several recurring agent security requirements can be stated as constraints on labeled execution edges: which tools may receive sensitive fields, which sinks may receive released data, and what authority may cross a delegation boundary. Unlike defenses tied to a specific agent architecture, AgentFlow exposes these checks as declarative rules over tool calls, response sinks, and delegation steps. 2. A multi-dimensional label lattice. Every data node is annotated with sensitivity, category, and trust metadata. The dimensions serve different purposes: sensitivity controls disclosure, category distinguishes fields such as email addresses from SSNs or credentials, and trust records whether content came from an untrusted source. This lets policies distinguish, for example, public-but-untrusted web text from trusted-but-confidential customer data. Labels are propagated through agent and tool operations using formally defined transfer functions. 3. Path rules for history-aware security. In addition to single-hop flow constraints, AgentFlow supports path rules that reason about multi-step behavior. Path rules can be evaluated over lineage-connected paths by default or over broader session-scoped histories when explicitly requested. This supports policies that require sanitization before external release, prevent reconnaissance-then-exfiltration patterns, or bound delegation depth, which are difficult to express with request-level tool permissions alone. Contributions: This paper makes the following contributions:

2

• We define a threat model for common agent attack surfaces: indirect prompt injection, malicious tool providers, and compromised sub-agents. We scope the model around policy-visible flows, which lets us state both the attacks AgentFlow targets and non-goals such as jailbreaks, hallucinations, covert channels, and unmediated tool bugs (§3). • We design AgentFlow, a policy language for LLM agents with tool calls, delegation, and response sinks. AgentFlow expresses security requirements using flow rules for individual execution edges and path rules for multi-step histories over labeled agent executions (§4). • We present a formal model of AgentFlow, including a multi-dimensional label lattice, an append-only provenance graph, execution traces, tool propagation functions, and a small-step operational semantics. We prove that the runtime preserves well-formedness and enforces the stated security goals for mediated traces (§5). • We develop an SMT-based verifier for the bounded, structured policy fragment used for predeployment checking. The verifier checks safety properties, including non-leakage, privilegeescalation resistance, trust-preserving flows, delegation safety, and taint monotonicity, or produces counterexample traces. • We implement an AgentFlow prototype consisting of a policy compiler, runtime engine, and verifier. We present preliminary evaluation evidence on AgentDojo [16] (949 injected cases across four task suites), AgentDyn [17] (200 dynamic Dailylife cases), and replay-based evaluations on ASB [18], InjecAgent [19], BIPIA [20], AgentHarm [21], and MCPTox [22]. Under the evaluated policies, AgentFlow reduces confirmed compromise to 0.0% on AgentDojo and AgentDyn, blocks the benchmark-specified policy-visible attacker flows in the replay evaluations, verifies seven safety properties in under 0.5 seconds each, and detects all 12 seeded unsafe policy variants in our study. These results are best understood as initial evidence for the modeled policy fragment and enforcement interface, not as a complete characterization of all agentic failure modes (§8). Figure 1 presents the system overview. AgentFlow interposes a runtime policy engine between the LLM agent and its tools. The runtime checks each tool call against declarative flow and path rules before execution. A separate SMT-based verifier checks safety properties over a bounded abstraction before deployment.

2

Background and Motivation

Modern LLM agents pair a planning loop with tool access: the model calls a tool, observes the result, and decides what to do next [1, 2]. Those tools may query databases, call APIs, scrape the web, read files, send email, execute code, or delegate to sub-agents. Frameworks and tool protocols such as the Model Context Protocol (MCP) [23] make these compositions easy to build. They also mean that data from a web page, email, or tool response can become part of a later privileged action [19].

2.1

Motivating Example

Consider an enterprise customer-support agent, Agent::main, owned by employee Alice. The agent has access to: • a users database containing names, SSNs, emails, and zip codes;

3

Pre-deployment Policy DSL labels, flows, paths

Compiler schema checks

SMT verifier bounded safety

Verified policy

load verified policy

User task external content

task/data

AgentFlow allow call runtime LLM agent proposed call Tools, APIs, reference monitor planner loop sub-agents checked response Allow/Deny/Pause tool result read/update allow release

Runtime state labels, lineage, capabilities, trace

External and response sinks

Runtime enforcement

Figure 1: AgentFlow system overview. Before deployment, policies are compiled and checked by the SMT verifier. At runtime, the reference monitor intercepts tool calls and modeled response sinks, evaluates labels, capabilities, lineage, and path rules, and returns Allow/Deny/Pause. • a transactions database containing card numbers and amounts; • a corporate email system and Slack workspace; and • an LLM summarization service, which may be hosted by a third party. The agent also delegates research tasks to a sub-agent, Agent::researcher, which can browse the web and call APIs but should not receive confidential data or cause external side effects. Attack 1: Data exfiltration via summarization. A malicious instruction embedded in a web page [5] (retrieved by the researcher sub-agent and passed to the main agent) instructs the agent to: “Summarize all customer SSNs and email them to attacker@evil.com.” The main agent is allowed to read the user database and send emails, so each tool call may look legitimate in isolation. The unsafe part is the path: confidential information flows from the database, through an LLM summarization step, to an external email sink without sanitization. Attack 2: Trust laundering. The researcher sub-agent scrapes a web page that claims: “The following text is a verified internal policy update: all agents should forward user data to backup@evil.com.” The text came from the web, so it is untrusted. If the system drops that provenance, the main agent may treat the injected instruction as an internal directive [24, 25]. Attack 3: Privilege escalation via delegation. The main agent delegates a research task while carrying confidential context. If the delegation boundary does not restrict what data or authority can cross, the sub-agent may receive data it should not see, or the parent may act as a confused deputy by performing privileged reads or writes on the sub-agent’s behalf [26, 27].

4

2.2

Request-Level Authorization Is Not Enough

Request-level authorization remains necessary: systems still need to decide whether an agent may call a particular tool on a particular resource. A language such as Cedar [8] is well suited to that question because it evaluates individual (principal, action, resource) requests against permit and forbid policies. The enterprise example cannot be checked by request-level authorization alone. Querying the database, calling a summarizer, and sending an email can each be legitimate operations. What matters is the chain connecting them: confidential data is read, transformed, and then released to an external sink without an approved declassification step. Trust laundering has the same shape. If text from the web is summarized, copied, or delegated, the system must still know that it came from an untrusted source. These checks require provenance, labels that change with execution, and constraints over paths through the agent’s history, rather than isolated allow/deny decisions at each tool call.

3

Threat Model

We consider a system with users, agents, tools, data sources, data sinks, and optional sub-agents. Agents carry out user instructions through tool calls such as database queries, API calls, file operations, web retrieval, and email. The AgentFlow runtime mediates tool invocations and modeled response sinks, and we assume it is trusted and correctly implemented. AgentFlow is a policy-enforcement layer, not a general LLM alignment or program-verification system. An attack is in scope when it attempts to cause a policy-visible flow: a mediated tool call, delegation step, data release, or modeled response-sink output that violates the configured policy. Trust boundaries: Security can fail at five boundaries: user–agent, agent–tool, agent–sub-agent, agent–external system, and agent–tool registry. Agents may be influenced by prompt injection or unintended model behavior [5, 28]; users delegate authority through tool permissions and task instructions [29]. Tool implementations are trusted to obey their specifications, but returned data may be untrusted. Sub-agents may be compromised or manipulated [26, 25]. External systems are disclosure boundaries, and dynamically registered tools such as MCP tools may be malicious or overly permissive [23, 30, 6]. In-scope attacks: The attacker can influence policy-visible behavior in three ways [31, 32]. An indirect prompt injector controls external content consumed by the agent, such as web pages, emails, documents, or RAG entries [5, 24, 33]. A malicious tool provider controls tool metadata or outputs [30]. A compromised sub-agent tries to escalate privilege, influence other agents, or exfiltrate data. These attackers cannot modify the runtime, change the loaded policy, compromise vetted tools, or bypass mediated execution paths. AgentFlow blocks the resulting policy violations when they induce unauthorized tool calls, delegations, data releases, or protected response-sink flows. Section 8 evaluates enforcement on attacks drawn from AgentDojo, AgentHarm, ASB, InjecAgent, BIPIA, and related benchmarks. Non-goals: AgentFlow does not try to prevent every unsafe LLM behavior. Jailbreaks, hallucinations, incorrect advice, and misleading final answers are out of scope unless they cause a mediated policy violation or reach a modeled protected response sink. The runtime also does not judge whether an allowed tool call is semantically correct for the user’s task. Covert and side channels, including timing, token-length, and resource-usage channels, are outside the model unless represented as sinks. Bugs or compromises in trusted components, or any action path that bypasses the reference monitor, are not covered.

5

Security goals: Given a trusted runtime and a policy that correctly captures the intended security requirements for mediated tools and sinks, AgentFlow enforces five properties: data flows satisfy applicable flow and path constraints; delegated agents do not receive data exceeding their authorized sensitivity; untrusted data remains marked untrusted unless explicitly reclassified; sensitive data reaches external sinks only through policy-approved flows; and multi-step behaviors prohibited by path constraints are blocked.

4

AgentFlow Language Design

We now present the core language model of AgentFlow. The language makes policies over labeled runtime edges the common interface for expressing checks such as access control, information-flow restrictions, sandboxing, approval workflows, rate limits, and delegation safety in tool-using agents. The language is organized around four core concepts: label system, flow graphs, flow rules, and path rules.

4.1

Label System

AgentFlow label L is the fundamental mechanism for classifying data. Inspired by the lattice model of Denning [34] and the decentralized label model of Myers and Liskov [35], each label system is a triple drawn from a multi-dimensional lattice with three components: Sensitivity, Category set, and Trust. Label L is defined as ⟨s, C, t⟩ Sensitivity: A sensitivity s denotes the confidentiality level assigned to a data object. Sensitivity is partially ordered by the relation ≤, which specifies the permitted flow of information between security classes. s ∈ sensitivity ::=

Public | Internal | Confidential | Restricted | TopSecret

The order of sensitivities are defined using the relation ⪯s : Public ⪯s Internal ⪯s Confidential ⪯s Restricted ⪯s TopSecret

Categories: Categories are represented as tags drawn from a hierarchical taxonomy, enabling policies to reason about data at different levels of abstraction. Let A be a finite set of atomic category identifiers, where a ∈ A. A category is a hierarchical sequence of identifiers defined as: c ∈ Category ::= a | c.a. For example, the category: Personal.Identity.SSN denotes a path in the category hierarchy. A category set is a finite set of categories: C ⊆ Category. We define the ancestor relation ⪯c over categories. Intuitively, c1 ⪯c c2 means that c1 is equal to or more specific than c2 . The relation is defined by the following rules: c ⪯c c

c1 ⪯c c2 C-Step c1 .a ⪯c c2

C-Refl

c1 ⪯c c2 c2 ⪯c c3 C-Trans c1 ⪯c c3 For example, Personal.Identity.SSN ⪯c Personal.Identity. We define standard operations over category sets, including union (∪), intersection (∩), removal (\c ), and hierarchical matching (|=c ). Hierarchical matching is defined as: C |=c p ⇐⇒ ∃q ∈ C. q ⪯c p. For example, {Personal.Identity.SSN} |=c Personal.Identity. Removing all categories matching a category p is defined as: C \c p = { q ∈ C | ¬(q ⪯c p) }

6

Trust: A boolean indicating whether the data originates from a trusted source. Untrusted data (e.g., web scrapes, content from potentially poisoned vector stores) carries t: false and is subject to additional restrictions. Now we define the various relation over the label L, specifically over two labels ℓ1 and ℓ2 , where ℓ1 = ⟨s1 , C1 , t1 ⟩ and ℓ2 = ⟨s2 , C2 , t2 ⟩. The label ordering is defined by the relation ⊑: ℓ1 ⊑ ℓ2 ⇐⇒ s1 ⪯s s2 ∧ C1 ⊆ C2 ∧ (t1 ∨ ¬t2 ) The trust constraint (t1 ∨ ¬t2 ) ensures that untrusted data cannot flow into trusted destinations. Thus, trusted data may flow to either trusted or untrusted contexts, but untrusted data may only flow to untrusted contexts. If t1 is true (trusted source), the flow is allowed; otherwise the destination must be untrusted (¬t2 ). The join ⊔ of two labels is the least upper bound, defined as: ℓ1 ⊔ ℓ2 = ⟨max(s1 , s2 ), C1 ∪ C2 , t1 ∧ t2 ⟩. The meet relation ⊓ of two labels is the greatest lower bound, defined as: ℓ1 ⊓ ℓ2 = ⟨min(s1 , s2 ), C1 ∩ C2 , t1 ∨ t2 ⟩.

4.2

Flow Graph Model

AgentFlow separates the static policy schema from the runtime provenance model. The schema names node and edge types that policies may mention; it is not a control-flow graph. At runtime, each allowed operation appends a trace event, creates a fresh data object, and records provenance edges from earlier parent objects to the new output. Loops, retries, and memory updates therefore appear as additional events, while the provenance graph remains append-only and acyclic. Path rules are evaluated over lineage-connected subgraphs or over the ordered session trace. This follows the data-flow view used in dynamic taint analysis [36]. Figure 2 presents the AgentFlow syntax. Nodes: Nodes represent entities in the information-flow graph through which data may originate, propagate, transform, or terminate. A node may correspond to a data source (databases, APIs, file systems), an external sink (email systems, external APIs, logging), or an internal computation component (agent memory, sandboxes). Node is represented as name : ⟨k, L, (x, v), (f, L)⟩. name represents the node name as T :: i, where T is a node type name and i is an instance name. For example, Database::records. Each node is associated with a kind k, a security label L of the data associated with that node, along with optional metadata property map (x, v), and field-level labels for structured data (f, L). Metadata property map is used by policies to express semantic constraints over nodes, such as whether a node is external, third-party, financial, or agent-controlled. For example, a node Database::users of kind source may carry sensitivity Confidential, categories {Personal.Identity, Personal.Contact}, and trusted astrue, with per-field overrides (e.g., the ssn field at Restricted ). A sink such as EmailSystem::corporate is annotated with external = true and irreversible = true. Edges: Edges represent permitted data-flow operations between nodes in the flow graph. An edge defines how data propagates from a source node to a destination node, along with the transformation applied to the security label during propagation. Edge is represented as ename : ⟨n1 , n2 , ρ⟩, where ename is the name of the edge, n1 is the source node, n2 is the destination node, and ρ defines the label propagation semantics applied during the flow. The propagation mode ρ defines how security labels are propagated across an edge during data flow. Intuitively: •

◁f rom propagates labels from source node n without modification. Mainly used for data reads (SQLQuery, FileRead).

•

⇝ (r) applies a sequence of transformation rules r to the input label, such as category removal, sensitivity downgrading, or trust modification. This rule can be for sanitization (Anonymize, Encrypt). This corresponds to controlled declassification [37].

•

⊥ denotes opaque propagation, where internal propagation semantics are hidden or conservatively approximated inspired by language-based IFC [38]. This can be used for black-box 7

k ∈ kind ::= source | internal | sink ρ ∈ prop ::= ◁f rom | ⇝ (r) |⊥ |≡s

r ∈ rule ::= ⊖c |↓s | := s

source internal sink

remove downgrade set

name := T :: i

inherit transform opaque constant

f⊢ ∈ fperm ::= allow | deny π⊢ ∈ pperm ::= require | f orbid ϕreq : str → Bool

n ∈ Node ::= name : ⟨k, L, (x, v), (f, L)⟩ e ∈ Edge ::= ename : ⟨n1 , n2 , ρ⟩ a ∈ Agent ::= (aname, name) : ⟨s, e, a, b, ap ⟩ ts ∈ TaskScope ::= (tname, name) : ⟨e, e⟩ cl ∈ Clause ::= ⟨nsϕ , ndϕ , eϕ , Lϕ , aϕ , ϕ, ϕreq ⟩ f ∈ Flow ::= (f⊢ , f name) : cl em ∈ EdgeMatch ::= ename : ⟨nsϕ , ndϕ , Lϕ ⟩ πe ∈ PathExpr ::= em | (πe ) | πe →∗ πe | πe →! πe n {m,n} | i=1 πei | πe scope ∈ {lineage, session} π ∈ Path ::= (π⊢ , pname) : ⟨πe , e, πϕ , scope⟩ P ∈ Policy ::= ⟨f , π⟩

Figure 2: AgentFlow language syntax Edge

From → To

Propagation Semantics

SQLQuery

source → internal

◁from

Anonymize internal → internal ⇝ (r) LLMCall

internal → internal ⊥

propagates source labels unchanged removes identity categories and downgrades sensitivity conservatively propagates labels; also flows to provider sink

Figure 3: Representative edge definitions in AgentFlow. operations (LLMCall, CodeExecute) where the exact information flow is unknown. •

≡ s ignores the input label and replaces it with the constant label s. Mainly used for pure functions (GetTime, Calculate).

Figure 3 shows representative edge definitions.

4.3

Agent

Agents represent autonomous execution principals that perform operations over the information-flow graph. An agent defines the set of edges it is authorized to invoke, the maximum sensitivity level it may access, and optional delegation relationships to other agents. Formally, an agent is defined as (aname, name) : ⟨s, e, a, b, ap ⟩, where aname represents the agent name and name of the form T :: i represents the owner of the agent, s represents the maximum sensitivity level accessible to the agent, e represents the set of edges the agent is authorized to invoke, a represents the set of agents to which delegation is permitted, b represents the condition specifying whether the agent is a sub-agent or not, and last element ap represents the parent agent information (this field is optional). The owner

8

represented by name specifies who controls the agent, while the parent (a) specifies which other agent the agent operates under. Figure 4 shows two representative agent definitions. Agent

Max Sens. Permitted Edges

main (owner: alice)

Confidential SQLQuery, FileRead researcher, VectorSearch, LLMCall data_analyst SendEmail, SlackPost Anonymize, Redact, Calculate, GetTime

researcher (sub-agent of main)

Internal

WebScrape, APIGet, Calculate, GetTime

Delegates

—

Figure 4: Agent definitions. Each agent has an owner, maximum sensitivity clearance, and an edge whitelist implementing least privilege. Sub-agents inherit their parent’s owner but have independent clearance levels and restricted edge sets. Task scopes: Task scopes define temporary least-privilege restrictions applied to an agent during the execution of a specific task. A task scope constrains which edges an agent is permitted or forbidden to invoke within that execution context. It is formally represented as (tname, name) : ⟨e, e⟩. For example, a task scope summarize_emails for agent main permits only {ReadEmail, LLMCall} and explicitly denies {SendEmail, HTTPPost, SQLWrite}.

4.4

Flow Rules

Flow rules define policy constraints over information flows in the graph. A flow rule either permits or denies a flow when a collection of predicates over nodes, edges, labels, agents, and runtime state are satisfied. Flow is representes as (f⊢ , f name) : cl where f⊢ denotes the flow permission and cl is the clause. Clause consist of following: nsϕ denotes an optional predicate over source nodes, ndϕ denotes an optional predicate over destination nodes, eϕ denotes an optional predicate over edges, Lϕ denotes an optional predicate over propagated labels, aϕ denotes an optional predicate over agents, ϕ denotes an optional predicate over the runtime flow context, and ϕreq denotes an optional authorization requirement predicate that must evaluate to true before a matching allow rule can authorize the flow. Figure 5 shows four representative deny rules. Rule Name

Effect Condition

no_pii_external

deny

credentials_never_leave clearance_cap untrusted_to_control

carrying Personal.Identity.*; to external sink deny carrying Credential.*; to any deny data.sensitivity > agent.sensitivity deny from untrusted node; to AgentPlanner; data may contain instructions

Figure 5: Representative flow rules. AgentFlow follows a default-deny policy consistent with the principle of least privilege [39]: any flow not explicitly permitted by an allow rule is rejected. If both allow and deny rules match a flow, deny rules take precedence, following the conflict-resolution model used by Cedar [8].

9

4.5

Path Rules

Path rules constrain multi-step data flow, not just individual hops. σ defines a single step-event consisting of ⟨ns , e, nd , L, a⟩, where ns represents the source node, e represents the edge, nd represents the destination node, L represents the label, and a represents the executing agent. A single step observe one flow action; hence we defined flow-rules to inspect one step. There are certain security properties that needs to be assured for the sequence of actions. For example, Data must be anonymized before sending it out. requires not only checking the edge SENDEMAIL, but also needs guarantees about edge before SENDEMAIL. Hence, we introduce notion of trace τ . To check for assurance for a set of properties we define a notion of edge match. An edge match em defines a single-step trace pattern, where ename denotes the matched edge name, nsϕ denotes a predicate over source nodes, ndϕ denotes a predicate over destination nodes, and Lϕ denotes a predicate over propagated labels. We have a notion of path expression represented as πe , which defines the temporal patterns over execution traces. A path expression describes how information-flow events are expected to occur over time within a trace. The expression πe matches a consecutive ordered sequence of path expressions in a trace. The expression πe1 →∗ πe2 matches a trace in which a match for πe1 is eventually followed by a later match for πe2 , with zero or more intermediate steps between them. The expression πe1 →! πe2 matches a trace in which a match for πe1 is immediately followed by a step n that does not match πe2 . The expression i=1 πei matches any one of the alternative path expressions {m,n}

in πe , while πe matches between m and n consecutive repetitions of the path expression πe . Path rules π define temporal constraints over execution traces that cannot be expressed using individual flow rules alone. A path rule constrains how information-flow events may occur over time within a trace. A path rule is represented as (π⊢ , pname) : ⟨πe , e, πϕ , scope⟩, where the rule requires or forbids a matching trace pattern, and pname denotes the name of the path rule. The component πe denotes the temporal path expression matched against execution traces. The set e denotes an optional set of edge names that must appear in a matched trace fragment. The predicate πϕ denotes an optional predicate over matched trace fragments, allowing additional constraints over execution history. Finally, scope ∈ {lineage, session} specifies whether the rule is evaluated over lineage traces or complete session traces. Figure 6 presents representative path rules.

4.6

Policy

A policy P defines the security constraints enforced by the system and is composed of a set of flow rules and a set of path rules. Flow rules govern individual information-flow steps, while path rules constrain temporal patterns over execution traces.

5

Formal Semantics

The static policy language defines the structure of permitted information flows, but enforcement in AgentFlow occurs dynamically during execution. At runtime, the system intercepts each tool invocation, computes propagated labels, evaluates flow and path policies, and updates execution lineage. Rather than reasoning only over static node types, AgentFlow tracks information flow per concrete runtime data object. This enables causal taint tracking, lineage-aware propagation, and path-sensitive policy enforcement across multi-step agent executions. To formalize runtime behavior, we introduce runtime data identifiers, execution steps, traces, runtime states, runtime decisions, and intercepted requests. Runtime data objects are identified by data identifiers d ∈ DataId , each of which names a concrete value produced during execution. 10

Rule

Kind

Semantics

require Paths carrying Personal.Identity.* data to external sinks must include Anonymize, Redact, or Encrypt. no_trust_laundering forbid Forbid paths where untrusted data reaches an external sink after trust elevation. limit_delegation_depthforbid Forbid paths containing ≥ 4 consecutive Delegate edges. no_recon_then_exfil forbid Forbid paths where SQLQuery over Confidential data is eventually followed by HTTPPost or SendEmail to an external sink unless the path includes Redact, or Anonymize, HumanReview. pii_must_sanitize

Figure 6: Representative path rules. require rules enforce the presence of specific edges in matching traces, while forbid rules prohibit matching temporal trace patterns. Execution proceeds through runtime steps. A step records a single causally connected informationflow event, including the participating nodes and edge, propagated labels, executing agent, produced data object, and its lineage dependencies. σ ∈ Step ::= ⟨ns , e, nd , Lin , Lout , a, d, dp ⟩ A trace records the sequence of runtime execution steps produced during policy enforcement. This trace may contain repeated invocations of the same edge, retries, and memory updates. Acyclicity applies only to the derived lineage/provenance relation over runtime data identifiers: each allowed step allocates a fresh output identifier whose parents are earlier identifiers. τ ∈ Trace ::= σ Runtime execution evolves over mutable runtime states that maintain taint information, execution traces, lineage relations, active task scopes, approved requirements, and active capabilities. str ∈ RuntimeState ::= ⟨M, τ, Lin, ts, Req, Cap⟩ where: •

M : DataId ⇀ L is the taint map. It records the current label associated with each runtime data object.

•

τ is the execution trace. It records all runtime steps that have been allowed during execution.

•

Lin : DataId ⇀ DataId is the lineage map. If Lin(d) = dp , then the data object d was derived from the parent data objects dp .

•

ts is the currently active task scope. It restricts which edges may be used during the current task execution. 11

•

Req is the set of approved runtime requirements that may be checked during policy evaluation.

•

Cap is the set of active capabilities currently granted to the runtime.

Each intercepted runtime request evaluates to a policy decision determining whether execution may proceed. D ∈ Decision ::= allow | deny | pause Runtime requests model intercepted tool invocations together with the execution context required for policy evaluation. req ∈ Request ::= ⟨a, e, ns , nd , d, f , ctx, cap⟩ •

a is the agent issuing the tool invocation.

•

e is the edge, or tool/action, being invoked.

•

ns is the source node from which the data is read.

•

nd is the destination node to which the result flows.

•

d is the input runtime data identifier. It identifies the data object whose taint and lineage should be used for this request.

•

f is the set of fields accessed by the request. When present, the input label is computed from the labels of these fields rather than from the whole source node.

•

ctx is the release context used by policies that depend on the runtime context of the request.

•

cap is an optional capability required to perform the request. The request may proceed only if the runtime state grants this capability.

The operational semantics define how runtime execution evolves under schema Γ and policy set P . Execution proceeds by intercepting runtime requests, computing propagated labels, constructing candidate execution steps, evaluating flow and path policies, and updating the runtime state accordingly.

5.1

Label Propagation Semantics

During execution, each edge propagates labels according to its propagation annotation ρ. We write ρ ⊢ Lin ⇓ Lout to mean that applying propagation mode ρ to input label Lin produces output label Lout . We also define the meaning of individual transformation rules. We write r ⊢ L ⇓ L′ to mean that applying rule r to label L produces label L′ . Let L = ⟨s, C, t⟩. ⊖c ⊢ ⟨s, C, t⟩ ⇓ ⟨s, C \c {c}, t⟩ 12

R-RemoveCat

s′ ≤ s R-Downgrade ↓ s′ ⊢ ⟨s, C, t⟩ ⇓ ⟨s′ , C, t⟩ := s′ ⊢ ⟨s, C, t⟩ ⇓ ⟨s′ , C, t⟩

R-Set

The propagation annotation of an edge lifts these rule-level transformations to runtime label propagation. ◁f rom ⊢ L ⇓ L

P-Inherit

≡ s′ ⊢ ⟨s, C, t⟩ ⇓ ⟨s′ , C, t⟩ ⊥ ⊢ L ⇓ ⟨high, ∅, false⟩

P-Const

P-Opaque

r1 ⊢ L0 ⇓ L1 · · · rn ⊢ Ln−1 ⇓ Ln P-Transform ⇝ (r1 , . . . , rn ) ⊢ L0 ⇓ Ln

5.2

Input Label Resolution

Before evaluating propagation policies, the runtime computes the input label associated with a request. Input labels are resolved using the source node, referenced fields, and lineage-connected runtime data objects. We write str , req ⊢ Lin to mean that, under runtime state str , the request req resolves to input label Lin . Source reads inherit the label directly from the source node when no field-level access is specified. ns = name : ⟨source, L, A, F ⟩ IL-Source str , ⟨a, e, ns , nd , d, ∅, ctx, cap⟩ ⊢ L Field-sensitive accesses compute the input label by joining the labels of the referenced fields. ∀(fi , Li ) ∈ F fi ∈ f IL-Field F str , ⟨a, e, ns , nd , d, f , ctx, cap⟩ ⊢ i Li Runtime lineage propagates taint labels across derived runtime data objects. Lin(d) = dp M (di ) = Li IL-Lineage F s d str , ⟨a, e, n , n , d, f , ctx, cap⟩ ⊢ i Li

5.3

Candidate-Step Construction

For each intercepted runtime request, the runtime constructs a candidate execution step by resolving the input label, applying edge propagation, and recording the resulting runtime flow event. We write str , req ⇓ σ to mean that, under runtime state str , the request req constructs candidate runtime step σ. Candidate-step construction combines input-label resolution and edge propagation semantics. str , req ⊢ Lin

ρ ⊢ Lin ⇓ Lout s d str , ⟨a, e, n , n , d, f , ctx, cap⟩ ⇓ ⟨ns , e, nd , Lin , Lout , a, d, dp ⟩ 13

CS-Build

where ρ is the propagation annotation associated with edge e. The runtime first resolves the input label associated with the request, then propagates the label according to the edge propagation semantics, and finally records the resulting runtime flow event as a candidate execution step.

5.4

Path Matching Semantics

Path expressions are evaluated over runtime execution traces. We write τ |= πe to mean that execution trace τ satisfies path expression πe . An edge-match expression matches a singleton trace when the runtime step satisfies the predicates associated with the edge matcher. em |= σ PM-Edge [σ] |= em Sequential composition matches when the trace can be decomposed into subtraces satisfying the component path expressions. τ1 |= πe1 τ2 |= πe2 PM-Seq τ1 · τ2 |= πe1 →∗ πe2 Strict sequential composition additionally requires the matching subtraces to be adjacent in the execution trace. τ1 |= πe1 τ2 |= πe2 adjacent(τ1 , τ2 ) PM-Strict ! τ1 · τ2 |= πe1 → πe2 Choice expressions match when at least one branch matches the trace. τ |= πej

1≤j≤n PM-Choice

n π i=1 ei

τ |=

Bounded repetition matches when the trace satisfies the path expression between m and n times. m≤k≤n

∀i ∈ [1, k]. τi |= πe {m,n}

τ1 · · · τk |= πe

PM-Repeat

Parenthesized expressions preserve the semantics of the enclosed path expression. τ |= πe PM-Group τ |= (πe ) The path matching semantics define how runtime execution traces satisfy path constraints used during policy evaluation.

5.5

Policy Evaluation Semantics

Policy evaluation determines whether a candidate runtime step may be committed to the execution trace. We write P, str ⊢ σ ⇓ D to mean that policy P , under runtime state str , evaluates candidate step σ to decision D. A policy decision is computed by evaluating flow clauses and path clauses against the candidate step and the current execution trace. Flow policies check whether the current step is permitted, while path policies check whether adding the candidate step would satisfy or violate a trace-level path constraint. A candidate step is allowed when: 14

•

no deny-flow clause matches the candidate step,

•

all required flow conditions are satisfied,

•

no forbidden path expression is matched by the extended trace,

•

all required path constraints are satisfied, and

•

all runtime requirements and capabilities referenced by the policy evaluate successfully.

Otherwise, the candidate step evaluates to either deny or pause depending on the failing policy condition. Let τ · σ denote the trace obtained by appending candidate step σ to the current execution trace τ. ∃(allow, f name) : cl ∈ f . cl |= σ ∀(deny, f name) : cl ∈ f . cl ̸|= σ ∀(require, pname) : ⟨πe , e, πϕ , scope⟩ ∈ π. τ · σ |= πe ∀(f orbid, pname) : ⟨πe , e, πϕ , scope⟩ ∈ π. τ · σ ̸|= πe P, ⟨M, τ, Lin, ts, Req, Cap⟩ ⊢ σ ⇓ allow

PEA

∃(deny, f name) : cl ∈ f . cl |= σ PED P, str ⊢ σ ⇓ deny ∃ϕreq . ϕreq (str ) = false PEP P, str ⊢ σ ⇓ pause where cl |= σ denotes that candidate step σ satisfies the predicates associated with clause cl.

5.6

Runtime Transition Semantics

Runtime execution proceeds by intercepting requests, constructing candidate execution steps, evaluating policies, and updating the runtime state accordingly. We write Γ, P ⊢ ⟨str , req⟩ → ⟨st′r , D⟩ to mean that, under schema Γ and policy set P , executing request req in runtime state str produces decision D and updated runtime state st′r . An allowed execution appends the candidate step to the runtime trace and updates the taint and lineage maps associated with the produced runtime data object. str , req ⇓ σ

P, str ⊢ σ ⇓ allow

σ = ⟨ns , e, nd , Lin , Lout , a, d, dp ⟩ st′r = ⟨M [d 7→ Lout ], τ · σ, Lin[d 7→ dp ], ts, Req, Cap⟩ RTA Γ, P ⊢ ⟨str , req⟩ → ⟨st′r , allow ⟩ A denied execution leaves the runtime state unchanged. str , req ⇓ σ P, str ⊢ σ ⇓ deny RTD Γ, P ⊢ ⟨str , req⟩ → ⟨str , deny⟩ 15

A paused execution similarly leaves the runtime state unchanged while awaiting additional approval or capability resolution. str , req ⇓ σ P, str ⊢ σ ⇓ pause RTP Γ, P ⊢ ⟨str , req⟩ → ⟨str , pause⟩ The runtime transition semantics define the behavior of AgentFlow by combining label resolution, propagation semantics, policy evaluation, and runtime state evolution.

6

Static Verification and Analysis

Beyond runtime enforcement, AgentFlow checks bounded policy properties by reducing them to satisfiability modulo theories (SMT), following the approach pioneered by AWS Zelkova [40] and extended to large-scale policy verification. The verifier covers a structured fragment of AgentFlow and uses a bounded abstraction of the runtime’s lineage semantics. It represents an execution of length at most k as symbolic steps with symbolic edge choices, labels, lineage links, capabilities, and path-rule matches, then asks whether any such trace can violate a target property.

6.1

Static Well-Formedness of the Schema

Before verification or execution, AgentFlow performs a collection of static consistency checks over the schema Γ = ⟨N , E, A, T , Σ, Σf ⟩, where N , E, A, and T denote the declared nodes, edges, agents, and task scopes, respectively, while Σ and Σf define the attribute and field typing environments. The well-formedness analysis ensures that all references are declared, labels and propagation functions are well typed, edges connect compatible nodes, agents reference only existing capabilities and delegation targets, and policy clauses refer only to entities present in the schema. These checks eliminate malformed configurations before execution and establish the assumptions required by both the operational semantics and the static verifier. The complete well-formedness judgments for schemas, nodes, edges, agents, policies, and runtime states are presented in Appendix A.

6.2

SMT Verifier

The SMT verifier translates a policy set and a bound k into Z3 [41] constraints and checks the safety properties summarized below. Each symbolic step chooses an edge, source and destination nodes, an agent, input and output labels, and lineage dependencies. Flow rules, release rules, and path rules are encoded as constraints over those steps. If the formula is SAT, the model is decoded into a counterexample trace; if it is UNSAT, no violating bounded abstract trace exists. This is a bounded guarantee under the verifier’s abstraction, not a claim about arbitrary unbounded LLM behavior. The prototype rebuilds the SMT encoding from scratch for each verification run; in our preliminary evaluation, these full reruns complete in under 0.5 seconds per checked property.

6.3

Runtime Enforcement Guarantees

The verifier checks bounded instances of the same safety goals enforced by the runtime, under the verifier’s abstraction. Separately, we prove that the AgentFlow runtime preserves well-formedness and enforces the security goals defined in Section 3 for mediated traces. The theorems below summarize these runtime guarantees; complete proofs are deferred to Appendix A. 16

Theorem 1 (Runtime Preservation). Assume Γ ⊢ P and Γ ⊢ str . If Γ, P ⊢ ⟨str , req⟩ → ⟨st′r , D⟩, then Γ ⊢ st′r . Theorem 2 (Policy Enforcement Soundness). Let str = ⟨M, τ, Lin, ts, Req, Cap⟩ be reachable under Γ and P . For every step σ ∈ τ , σ was appended only after policy evaluation returned allow . Therefore, σ matches an applicable allow rule, violates no matching deny-flow clause, satisfies all runtime requirements, and does not make the trace violate any forbid path rule in P . Theorem 3 (G1: Flow Policy Enforcement). Let str = ⟨M, τ, Lin, ts, Req, Cap⟩ be reachable under Γ and P . For every step σ ∈ τ , the flow represented by σ satisfies all applicable flow and path constraints in P . Theorem 4 (G2: Delegation Safety). Assume P contains a delegation clearance rule that denies any delegation step sending data with output label Lout to a delegated agent a′ whenever Lout .s ̸⪯s a′ .smax . Then no delegated agent receives data exceeding its authorized sensitivity level in any reachable trace. Theorem 5 (G3: Trust Preservation). Assume no explicit trust-reclassification transformation is applied. If data originates from an untrusted source, then every runtime data object derived from it remains untrusted in the taint map M . Theorem 6 (G4: External Disclosure Control). Assume P denies sensitive data flows to external sinks unless an applicable allow or release rule authorizes the flow and no matching deny or path rule blocks it. Then sensitive data may reach an external sink only through such an authorized flow.

7

Implementation

Our prototype is a Python policy engine with a compiler, runtime monitor, and SMT verifier.

7.1

Policy Compiler

The policy compiler parses AgentFlow policy files (labels, nodes, edges, agents, flow rules, release rules, and path rules) into an internal representation. The compiler performs syntax and schema checks before the policy is loaded: • Policy construction: Declared nodes, edges, agents, labels, task scopes, requirements, release rules, and path rules are parsed into the runtime policy representation. • Local validation: The compiler rejects malformed syntax, invalid sensitivity levels, invalid flow/path effects, unknown propagation operators, and unresolvable provider side-channel references such as also_flows_to. • Fail-closed handoff: References that depend on runtime task state, selected fields, or dynamically constructed tool calls are checked by the monitor at interception time; unknown agents, edges, nodes, capabilities, or task scopes deny rather than silently allowing the call.

17

7.2

Runtime Engine

The runtime engine intercepts tool calls and modeled response sinks in the agent loop and evaluates the policy: 1. Edge construction: Identifies the source node, destination node, and edge from the intercepted operation. 2. Scope and capability checks: Applies active task scopes, required capabilities, and runtime requirements before the operation is allowed to proceed. 3. Label computation: Applies the tool’s propagation function, selected-field labels, release contexts, and optional runtime scanners to compute the output label. 4. Flow and side-channel evaluation: Evaluates matching deny and allow rules, including implicit provider flows modeled with also_flows_to. 5. Path rule evaluation: Checks the updated lineage or session trace against configured path rules. 6. Decision: Returns ALLOW, DENY, or PAUSE. 7. State update: On ALLOW, updates the taint map, lineage map, and trace. The engine integrates with agent frameworks via middleware that wraps tool call functions, following the inline reference monitor approach [42]. In the LangChain integration, for example, tool wrappers preserve the original tool interface but call the AgentFlow runtime before execution. The wrapper maps the framework’s tool name and arguments to an AgentFlow edge, source node, destination node, selected fields, and optional capability context. If the decision is allow, the wrapper executes the tool and records the produced data identifier, output label, parent data identifiers, and trace entry; if the decision is deny or pause, the tool is not invoked. The AgentDojo and AgentDyn adapters use the same runtime interface, with suite-specific mappings from benchmark tools to policy nodes and edges. The runtime also supports field-level label tracking: when a tool reads specific fields from a source node (e.g., SELECT name, email rather than SELECT *), the input label is computed as the join of only those fields’ labels rather than the conservative node-level label, reducing overtainting. Additionally, edges with runtime_scan categories can invoke an optional callback to detect sensitive data in LLM output (e.g., scanning for SSN patterns), upgrading the output label accordingly. These scanners are conservative label upgraders, not semantic safety classifiers; false negatives are outside the formal guarantee unless the corresponding sink or release is modeled by the policy.

8

Evaluation

Our preliminary evaluation asks five questions: whether runtime enforcement blocks policy-visible attacks while preserving task completion; whether the same mechanisms transfer beyond AgentDojo [16]; whether the policies cover attack surfaces from additional benchmarks; whether the SMT verifier catches realistic policy mistakes; and whether mediation adds meaningful latency. We also compare with related defenses when public artifacts make the comparison meaningful. The results below are best interpreted as initial prototype evidence for the policy layer and its enforcement model, rather than as a comprehensive characterization of all agent security behaviors.

18

Table 1: Policy structure for the main agent evaluations. Policies are written once per suite, not per task or attack instance. Suite

Sensitive / Untrusted Inputs

Protected Sinks

Representative Rules

Banking

Accounts, balances, cards; injected messages Reservations, calendar, payments; web results Docs, email, contacts; external mail/web text Channels, DMs, web pages; attacker messages

Transfers, external messages

Personal data, files, finance, calendar; web/tool results

Email, files, finance, calendar mutations

Scope money movement; deny card/credential release Require task-scoped booking and calendar capabilities Allow typed releases; deny sensitive external sends Separate channel/DM/web sinks; block untrusted-to-privileged flows Reuse flow/path checks; scoped capabilities for dynamic tasks

Travel Workspace Slack

AgentDyn

8.1

Booking APIs, calendar updates External email, document sharing DMs, channels, final responses

Experimental Setup

Benchmarks: We use AgentDojo [16], which provides 949 injected test cases across Banking (144), Travel (140), Workspace (560), and Slack (105). Each case pairs a benign task with an injection attack. Rather than using AgentDojo’s raw security bit, we post-process traces with a four-way outcome taxonomy and report utility (benign task completion under the injected case) and confirmed compromise (observed attack success). The artifact includes case-level traces and the classifier script. We additionally run AgentDyn’s 200-case Dailylife stress test and five breadth checks. ASB [18] provides 10 scenarios, 51 benign tasks, 20 normal tools, and 400 attacker tools; we evaluate both its deterministic task/tool matrix and its upstream AIOS planner with AgentFlow inserted at the tool-call gate. We also replay InjecAgent [19], BIPIA response-sink splits [20], AgentHarm tool-target behaviors [21], and MCPTox poisoned MCP metadata [22] as deterministic authorization checks. Agent configuration: We use a fixed frontier LLM configuration for the frozen AgentDojo and AgentDyn runs and for denominator-aligned Progent comparisons. The upstream ASB DPI harness uses the model configuration from that artifact; the remaining breadth checks are deterministic replays. For each benchmark suite, we write one AgentFlow policy over the suite’s tools and data sources; policies are not specialized to individual tasks or attack instances. Baselines: Our primary baseline is the undefended system. We also reproduce the closest public programmable-policy baseline, Progent [9], using the same model family and public manualpolicy path. Slack and Banking are denominator-aligned with our frozen tables; Travel and Workspace use smaller Progent-bundled workloads, so we keep them supplemental. Policy structure: Table 1 summarizes the suite-level policies used in the main agent evaluations. This is not a separate policy-authoring study; the goal is to show what security state the policies model. Across suites, the policies mark sensitive sources, untrusted inputs, protected sinks, and task-scoped releases. The label dimensions serve different roles: sensitivity identifies data that should not leave freely, category separates fields such as email addresses from credentials or payment data, and trust prevents web or attacker-controlled content from authorizing privileged actions.

8.2

Runtime Security Enforcement

Table 2 presents the frozen results across all four AgentDojo suites. Interpreting the compromise metric. AgentDojo’s native security field can conflate blocked prerequisite calls with attack failure, task failure, or unevaluable cases. We therefore classify each 19

Table 2: Frozen AgentDojo results under a fixed frontier LLM configuration. Utility = benign task completion rate on injected cases (higher is better). Compromise = confirmed attack success rate (lower is better). Baseline Suite

AgentFlow

Util.%

Comp.%

Util.%

Comp.%

Banking Travel Workspace Slack

75.7 44.3 36.1 66.7

66.0 25.7 16.6 84.8

81.9 60.7 57.3 73.3

0.0 0.0 0.0 0.0

Total

46.7

33.0

63.3

0.0

Table 3: Main-paper AgentDojo ablation slices on the latest code. Utility is benign task completion; compromise is confirmed attack success. Suite

Metric

Travel Travel Slack Slack Banking Banking

Utility Compromise Utility Compromise Utility Compromise

A0

A2

A3

A4

A6

4/12 7/12 11/12 11/12 9/12 12/12

3/12 0/12 3/12 3/12 3/12 0/12

3/12 0/12 3/12 4/12 3/12 0/12

3/12 0/12 3/12 4/12 3/12 0/12

11/12 0/12 11/12 0/12 8/12 0/12

trace as compromise_confirmed, blocked_terminal, benign_failure_or_task_drop, or ambiguous. The “Comp.” column reports only confirmed compromise, separating attacks that genuinely succeed from attacks prevented by policy but possibly at utility cost. In these 949 injected cases, AgentFlow raises utility from 46.7% to 63.3% and reduces confirmed compromise from 33.0% to 0.0%. Trace inspection suggests that some policy blocks keep the agent from following injected distractions; the remaining utility costs come from travel gates, Slack message/webpage restrictions, banking money-movement controls, and Workspace external-email controls. On count-aligned public Progent runs, AgentFlow also exceeds Progent on Slack (73.3% utility and 0.0% compromise vs. 55.2% and 5.7%) and Banking (81.9% and 0.0% vs. 72.2% and 0.0%).

8.3

Mechanism Ablation

To diagnose mechanism value, we rerun frozen 12-case diagnostic slices from Travel, Slack, and Banking. Table 3 compares the undefended baseline (A0), flow-only enforcement (A2), flow plus path constraints (A3), flow plus path and lineage tracking (A4), and the full configuration with task-scoped capabilities and release contexts (A6). Early structural defenses reduce compromise but are too conservative for utility; A6 recovers benign task completion while retaining zero confirmed compromise on these slices. A2–A4 prevent all confirmed compromise on Travel and Banking, but often terminate benign workflows because they cannot distinguish attacker-induced side effects from task-authorized effects. A6 adds scoped capabilities and release contexts, raising Travel utility from 3/12 to 11/12 and Banking from 3/12 to 8/12. On Slack, the full policy closes channel, DM, webpage, and finalresponse sink gaps while matching the baseline’s 11/12 utility on the slice. 20

Table 4: Breadth checks across additional benchmarks. “Blocked/prevented” counts attacker or unsafe flows denied by AgentFlow. For deterministic replays, “Benign side” is the benign policy-gate pass count. Benchmark

Mode

Cases

Blocked/prevented

Benign side

ASB task/tool matrix ASB upstream DPI InjecAgent BIPIA AgentHarm MCPTox

deterministic gate planner + gate JSON case replay response-sink replay tool-target replay metadata-flow replay

2,142 1,200 2,108 41,250 416 485

2,040/2,040 1,200/1,200 2,108/2,108 41,250/41,250 208/208 485/485

102/102 2/1,200† 2,108/2,108 41,250/41,250 208/208 485/485

†

8.4

ASB reports original-task success under attacked prompts, not benign policy-gate pass rate.

Dynamic AgentDyn Stress Test

To test generalization beyond AgentDojo’s static tasks, we run the supported Dailylife suite from AgentDyn [17]. This 200-case run exposes a security-utility tradeoff: AgentFlow reduces confirmed compromise from 147/200 (73.5%) to 0/200 (0.0%), while utility changes from 89/200 (44.5%) to 87/200 (43.5%). The outcome taxonomy explains the tradeoff: AgentFlow blocks 319 tool calls across 143 cases, including 138 terminal policy blocks, mostly from missing scoped capabilities for dynamic task families such as inbox reads, web fetches, financial transfers, calendar changes, and graph/file mutations. The result suggests the mechanisms transfer to a more open-ended task distribution, while the first-pass Dailylife policy still needs additional release contexts and capability grants for legitimate dynamic-task families.

8.5

Breadth and Replay Checks

We also run breadth checks across ASB [18], InjecAgent [19], BIPIA [20], AgentHarm [21], and MCPTox [22] (Table 4). Except for the ASB upstream DPI run, these are deterministic policy-gate replays, so the benign-side column is not clean final-answer utility. The replays ask whether the policy layer blocks the benchmark-specified unsafe tool, sink, or metadata transition independent of model stochasticity. These replay checks test policy-gate coverage, not end-to-end agent utility. Within that scope, the policies block the modeled attacker flows across tool-registry attacks, indirect prompt-injection tool calls, response-sink flows, harmful tool-target sequences, and poisoned MCP metadata.

8.6

SMT Verification Value and Performance

We evaluate whether the SMT verifier catches realistic policy-authoring mistakes and how long the checked properties take to verify. Seeded verifier-bug study. We seed twelve plausible unsafe policy variants, including overbroad releases, missing PII guards, credential escape/exfiltration, third-party sharing, trust laundering, overpermission, and selected-field leaks. The verifier catches all 12/12 bugs: five structurally through the overbroad-release checker and seven through semantic properties for PII leakage, credential escape, credential exfiltration sequences, trust laundering, and third-party sharing. For the six bugs with externally actionable traces, we also generate replayable runtime witnesses showing the violation that would be reachable if verification were bypassed. Verification performance. Table 5 reports verification times for seven safety properties, each verified with bound k = 10 over the verifier’s bounded abstract traces. All seven properties verify in 21

Table 5: SMT verification results. All properties verified (UNSAT) with k=10 using Z3 [41]. Times are wall-clock on a single core. Property

Result

Time (s)

non_leakage_pii no_credential_escape no_privilege_escalation no_sensitive_to_third_party no_credential_exfil_sequence no_trust_laundering taint_monotonicity

UNSAT UNSAT UNSAT UNSAT UNSAT UNSAT UNSAT

<0.5 <0.5 <0.5 <0.5 <0.5 <0.5 <0.5

Table 6: Comparison with related agent defenses. The table compares policy-facing mechanisms, not overall security strength. ✓ means the feature is first-class in the paper or public artifact; Partial means the system provides a related mechanism with a narrower or different interface. Feature Runtime enforcement IFC/taint/provenance tracking Standalone declarative policy layer Explicit path/history constraints Task/capability scoping Bounded SMT policy checks

AgentFlow

FIDES

CaMeL

FORGE

SAMOS

✓ ✓ ✓ ✓ ✓ ✓

✓ ✓ – – Partial –

✓ Partial – – ✓ –

✓ ✓ ✓ Partial Partial –

✓ ✓ – – Partial –

under 0.5 seconds. The largest checked-in AgentDojo/AgentDyn policy has 28 edges, 17 nodes, and 30 flow/path/release rules; with k = 10, the resulting quantifier-free formulas remain small enough for sub-second solving. Thus policies can be checked before deployment for the verified properties within the verifier’s bounded abstraction.

8.7

Runtime Overhead

We measure the policy evaluation path (label lookup, rule matching, path checking, and taint propagation) on the benchmark schema used by our scenario tests. Average per-intercept latency is 6.4 µs (P50: 6.0 µs, P95: 8.7 µs, P99: 9.7 µs), negligible relative to LLM inference (∼1–10 seconds). Wrapper, logging, and scanner costs vary by integration, but the core policy decision is not a bottleneck in our measurements.

8.8

Comparison with Related Defenses

Table 6 compares AgentFlow with the closest related defenses. “Partial” denotes a related mechanism with a narrower or different interface. The table compares policy-facing mechanisms, not overall security strength. AgentFlow differs mainly in exposing a standalone policy layer over labeled edges and histories, together with bounded checks for the supported policy fragment. FIDES [13] and CaMeL [14] embed security into the agent architecture. FORGE [12] is closest as a declarative policy system, using Datalog over dependency graphs; AgentFlow instead emphasizes labeled flow/path rules and bounded SMT checks. SAMOS [15] applies IFC ideas to MCP workflows. These systems are not simply baselines for the same interface: they make different assumptions about where enforcement lives. We also ran a denominator-aligned reproduction of CaMeL’s public +camel artifact on our AgentDojo configuration; it completed all 949 cases with 60.1% utility. AgentFlow

22

reaches 63.3% utility in our frozen package. We treat this as an artifact-level comparison, not as a head-to-head security ranking.

8.9

Limitations and Discussion

Overtainting and utility: The main limitation is overtainting in message-heavy workflows. When an LLM processes a tainted tool result, the runtime may conservatively propagate that taint because it cannot recover exact token-level dependencies. Per-task reset helps when tasks have clear boundaries, but tasks that mix trusted and untrusted content still require careful release rules. This is why we report both utility and confirmed compromise. Task classes that require care: AgentFlow enforces the configured policy; it does not infer which releases the application owner intended. Tasks that intentionally forward untrusted web content to an external sink, combine private records with attacker-controlled instructions, or share sensitive fields with a third party require explicit release contexts. Without those contexts, the runtime may block a benign task. AgentDyn exposes this tradeoff: the first-pass Dailylife policy blocks all confirmed compromises in our run, but missing scoped capabilities account for many terminal denials. Guarantee scope: 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. This scope is still useful in practice: the verifier checks policy properties before deployment, while the runtime monitor enforces those policies on mediated actions.

9

Related Work

We focus on work that shapes AgentFlow: attacks on tool-using agents, agent defenses, authorization and IFC, and policy analysis.

9.1

LLM Agent Security

Prompt injection and tool misuse show that agent security cannot stop at input filtering. Greshake et al. [5] introduced indirect prompt injection against LLM-integrated applications. AgentDojo [16] and InjecAgent [19] study the same failure mode in tool-using agents. BIPIA focuses on final-response manipulation [20]; AgentDyn adds dynamically generated tasks [17]; AgentHarm studies harmful tool-use requests [21]; ASB broadens the task and tool surface [18]; and MCPTox targets poisoned MCP metadata [22]. Other attacks enter through tool selection [30, 43], memory [33], logs [6], web content [44, 45], or multi-agent communication [25]. These attacks motivate tracking later uses of untrusted or sensitive content, not only suspicious prompts. Recent defenses protect different parts of the stack. Progent controls tool privileges [9]. SEAgent applies mandatory-access-control ideas to delegation [7]. Conseca generates task-specific policies [11], while AgentArmor analyzes runtime traces [10]. Other defenses rely on isolation or integrity guardrails [27], guard agents [46], prompt sanitization [47], or permission prediction [29]. AgentFlow complements these systems by making lineage, labels, and path constraints explicit policy objects. The closest related systems are FORGE [12], FIDES [13], CaMeL [14], and SAMOS [15]. FORGE uses Datalog over dependency graphs. FIDES embeds taint tracking in an agent planner. CaMeL separates privileged planning from quarantined data processing. SAMOS places an IFC gateway around MCP workflows. AgentFlow uses a different interface: policies over labeled runtime edges, path rules, task-scoped capabilities, and a bounded SMT-checked fragment. 23

9.2

Authorization and Information Flow

Traditional authorization systems decide whether a principal may act on a resource. Cedar [8, 48], XACML [49], Zanzibar [50], and Datalog-based authorization [51] are examples of this request-level view. Zelkova uses SMT solving to analyze authorization policies [40]. AgentFlow instead tracks how content obtained in one step may influence a later agent action or sink. AgentFlow also draws on classical IFC. Denning introduced lattice-based information flow [34], and Myers and Liskov developed decentralized labels [35]. Jif [52], Flume [53], Asbestos [54], and LIO [55] enforce labels in conventional programs. Work on declassification [37] and dynamic taint analysis [56, 36] informs our propagation model. LLM agents expose tool and model calls rather than transparent program dependencies; AgentFlow treats those calls as monitored data-flow steps and adds path rules.

9.3

Verification and Runtime Monitoring

SMT and symbolic techniques are common in policy analysis. Our verifier uses Z3 [41]. Margrave analyzes access-control policies [57]; FIREMAN checks firewall rules [58]; and cloud-policy verification finds misconfigurations before deployment [59]. AgentFlow applies this style of pre-deployment checking to bounded agent properties: label propagation, graph reachability, and path patterns. At runtime, AgentFlow follows the reference-monitor tradition. Schneider characterizes policies enforceable by execution monitors [60]. Ligatti et al. study edit automata [61, 62], and SASI demonstrates inline reference monitoring [42]. AgentFlow mediates agent tool calls and modeled response sinks, but reasons over labels, provenance, capabilities, and paths rather than low-level system calls. Work on multi-agent security [26] and MCP security [23] further motivates this placement: delegation and tool registration introduce data-flow boundaries that ordinary tool permissions do not capture.

10

Conclusion

We presented AgentFlow, 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. Yao, J. Zhao, D. Yu, N. Du, I. Shafran, K. Narasimhan, and Y. Cao, “React: Synergizing reasoning and acting in language models,” arXiv preprint arXiv:2210.03629, 2022. [2] T. Schick, J. Dwivedi-Yu, R. Dessì, R. Raileanu, M. Lomeli, E. Hambro, L. Zettlemoyer, N. Cancedda, and T. Scialom, “Toolformer: Language models can teach themselves to use tools,” Advances in neural information processing systems, vol. 36, pp. 68 539–68 551, 2023.

24

[3] Z. Xi, W. Chen, X. Guo, W. He, Y. Ding, B. Hong, M. Zhang, J. Wang, S. Jin, E. Zhou et al., “The rise and potential of large language model based agents: A survey,” Science China Information Sciences, vol. 68, no. 2, p. 121101, 2025. [4] M. Yu, F. Meng, X. Zhou, S. Wang, J. Mao, L. Pan, T. Chen, K. Wang, X. Li, Y. Zhang et al., “A survey on trustworthy llm agents: Threats and countermeasures,” in Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining V. 2, 2025, pp. 6216–6226. [5] K. Greshake, S. Abdelnabi, S. Mishra, C. Endres, T. Holz, and M. Fritz, “Not what you’ve signed up for: Compromising real-world llm-integrated applications with indirect prompt injection,” in Proceedings of the 16th ACM workshop on artificial intelligence and security, 2023, pp. 79–90. [6] Y. Hu, C. Fan, S. Samyoun, and J. Du, “Log-to-leak: Prompt injection attacks on tool-using llm agents via model context protocol,” 2026. [7] Z. Ji, D. Wu, W. Jiang, P. Ma, Z. Li, Y. Gao, S. Wang, and Y. Li, “Taming various privilege escalation in llm-based agent systems: A mandatory access control framework,” arXiv preprint arXiv:2601.11893, 2026. [8] J. W. Cutler, C. Disselkoen, A. Eline, S. He, K. Headley, M. Hicks, K. Hietala, E. Ioannidis, J. Kastner, A. Mamat et al., “Cedar: A new language for expressive, fast, safe, and analyzable authorization,” Proceedings of the ACM on Programming Languages, vol. 8, no. OOPSLA1, pp. 670–697, 2024. [9] T. Shi, J. He, Z. Wang, H. Li, L. Wu, W. Guo, and D. Song, “Progent: Programmable privilege control for llm agents,” arXiv preprint arXiv:2504.11703, 2025. [10] P. Wang, Y. Liu, Y. Lu, Y. Cai, H. Chen, Q. Yang, J. Zhang, J. Hong, and Y. Wu, “Agentarmor: Enforcing program analysis on agent runtime trace to defend against prompt injection,” arXiv preprint arXiv:2508.01249, 2025. [11] L. Tsai and E. Bagdasarian, “Contextual agent security: A policy for every purpose,” in Proceedings of the 2025 Workshop on Hot Topics in Operating Systems, 2025, pp. 8–17. [12] N. Palumbo, S. Choudhary, J. Choi, G. Amir, P. Chalasani, and S. Jha, “Formal policy enforcement for real-world agentic systems,” arXiv preprint arXiv:2602.16708, 2026. [13] M. Costa, B. Köpf, A. Kolluri, A. Paverd, M. Russinovich, A. Salem, S. Tople, L. Wutschitz, and S. Zanella-Béguelin, “Securing ai agents with information-flow control,” arXiv preprint arXiv:2505.23643, 2025. [14] E. Debenedetti, I. Shumailov, T. Fan, J. Hayes, N. Carlini, D. Fabian, C. Kern, C. Shi, A. Terzis, and F. Tramèr, “Defeating prompt injections by design,” arXiv preprint arXiv:2503.18813, 2025. [15] G. Ntousakis, J. J. Stephen, M. V. Le, S. S. L. Chukkapalli, T. Taylor, I. M. Molloy, and F. Araujo, “Securing mcp-based agent workflows,” in Proceedings of the 4th Workshop on Practical Adoption Challenges of ML for Systems, 2025, pp. 50–55. [16] E. Debenedetti, J. Zhang, M. Balunovic, L. Beurer-Kellner, M. Fischer, and F. Tramèr, “Agentdojo: A dynamic environment to evaluate prompt injection attacks and defenses for llm agents,” Advances in Neural Information Processing Systems, vol. 37, pp. 82 895–82 920, 2024. 25

[17] H. Li, R. Wen, S. Shi, N. Zhang, and C. Xiao, “Agentdyn: A dynamic open-ended benchmark for evaluating prompt injection attacks of real-world agent security system,” arXiv preprint arXiv:2602.03117, 2026. [18] H. Zhang, J. Huang, K. Mei, Y. Yao, Z. Wang, C. Zhan, H. Wang, and Y. Zhang, “Agent security bench (asb): Formalizing and benchmarking attacks and defenses in llm-based agents,” in International Conference on Learning Representations, vol. 2025, 2025, pp. 35 331–35 366. [19] Q. Zhan, Z. Liang, Z. Ying, and D. Kang, “Injecagent: Benchmarking indirect prompt injections in tool-integrated large language model agents,” in Findings of the Association for Computational Linguistics: ACL 2024, 2024, pp. 10 471–10 506. [20] J. Yi, Y. Xie, B. Zhu, E. Kiciman, G. Sun, X. Xie, and F. Wu, “Benchmarking and defending against indirect prompt injection attacks on large language models,” in Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining V. 1, 2025, pp. 1809–1820. [21] M. Andriushchenko, A. Souly, M. Dziemian, D. Duenas, M. Lin, J. Wang, D. Hendrycks, A. Zou, Z. Kolter, M. Fredrikson et al., “Agentharm: A benchmark for measuring harmfulness of llm agents,” in International Conference on Learning Representations, vol. 2025, 2025, pp. 79 185–79 220. [22] Z. Wang, Y. Gao, Y. Wang, S. Liu, H. Sun, H. Cheng, G. Shi, H. Du, and X. Li, “Mcptox: A benchmark for tool poisoning on real-world mcp servers,” in Proceedings of the AAAI Conference on Artificial Intelligence, vol. 40, no. 42, 2026, pp. 35 811–35 819. [23] X. Hou, Y. Zhao, S. Wang, and H. Wang, “Model context protocol (mcp): Landscape, security threats, and future research directions,” ACM Transactions on Software Engineering and Methodology, 2025. [24] Y. Liu, Y. Jia, R. Geng, J. Jia, and N. Z. Gong, “Formalizing and benchmarking prompt injection attacks and defenses,” in 33rd USENIX Security Symposium (USENIX Security 24), 2024, pp. 1831–1847. [25] D. Lee, M. Tiwari, and B. Miranda, “Prompt infection: Llm-to-llm prompt injection within multi-agent systems,” in European Symposium on Research in Computer Security. Springer, 2025, pp. 511–520. [26] C. S. de Witt, K. Krawiecka, I. Krawczuk, B. Hagag, W. L. Anderson, P. Belcak, B. Bucknall, X. Cai, A. Chopra, D. Cohen et al., “Open challenges in multi-agent security: Towards secure systems of interacting ai agents,” arXiv preprint arXiv:2505.02077, 2025. [27] J. Kim, W. Choi, and B. Lee, “Prompt flow integrity to prevent privilege escalation in llm agents,” arXiv preprint arXiv:2503.15547, 2025. [28] T. Geng, Z. Xu, Y. Qu, and W. E. Wong, “Prompt injection attacks on large language models: A survey of attack methods, root causes, and defense strategies,” Computers, Materials, & Continua, vol. 87, no. 1, 2026. [29] Y. Wu, K. Yang, F. Roesner, T. Kohno, N. Zhang, and U. Iqbal, “Towards automating data access permissions in ai agents,” arXiv preprint arXiv:2511.17959, 2025. [30] J. Shi, Z. Yuan, G. Tie, P. Zhou, N. Z. Gong, and L. Sun, “Prompt injection attack to tool selection in llm agents,” arXiv preprint arXiv:2504.19793, 2025. 26

[31] Y. Tang, Y. Liu, J. Lan, Z. Yan, and E. Gelenbe, “Security of llm-based agents regarding attacks, defenses, and applications: A comprehensive survey,” Information Fusion, p. 103941, 2025. [32] J. Kim, X. Liu, Z. Wang, S. Qiu, B. Li, W. Guo, and D. Song, “The attack and defense landscape of agentic ai: A comprehensive survey,” arXiv preprint arXiv:2603.11088, 2026. [33] Z. Chen, Z. Xiang, C. Xiao, D. Song, and B. Li, “Agentpoison: Red-teaming llm agents via poisoning memory or knowledge bases,” Advances in Neural Information Processing Systems, vol. 37, pp. 130 185–130 213, 2024. [34] D. E. Denning, “A lattice model of secure information flow,” Communications of the ACM, vol. 19, no. 5, pp. 236–243, 1976. [35] A. C. Myers and B. Liskov, “Protecting privacy using the decentralized label model,” ACM Transactions on Software Engineering and Methodology (TOSEM), vol. 9, no. 4, pp. 410–442, 2000. [36] E. J. Schwartz, T. Avgerinos, and D. Brumley, “All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask),” in 2010 IEEE symposium on Security and privacy. IEEE, 2010, pp. 317–331. [37] A. Sabelfeld and D. Sands, “Declassification: Dimensions and principles,” Journal of Computer Security, vol. 17, no. 5, pp. 517–548, 2009. [38] A. Sabelfeld and A. C. Myers, “Language-based information-flow security,” IEEE Journal on selected areas in communications, vol. 21, no. 1, pp. 5–19, 2003. [39] B. W. Lampson, “Protection,” ACM SIGOPS Operating Systems Review, vol. 8, no. 1, pp. 18–24, 1974. [40] J. Backes, P. Bolignano, B. Cook, C. Dodge, A. Gacek, K. Luckow, N. Rungta, O. Tkachuk, and C. Varming, “Semantic-based automated reasoning for aws access policies using smt,” in 2018 Formal Methods in Computer Aided Design (FMCAD). IEEE, 2018, pp. 1–9. [41] L. De Moura and N. Bjørner, “Z3: An efficient smt solver,” in International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2008, pp. 337–340. [42] U. Erlingsson and F. B. Schneider, “Sasi enforcement of security policies: A retrospective,” in Proceedings of the 1999 workshop on New security paradigms, 1999, pp. 87–95. [43] J. Ye, S. Li, G. Li, C. Huang, S. Gao, Y. Wu, Q. Zhang, T. Gui, and X.-J. Huang, “Toolsword: Unveiling safety issues of large language models in tool learning across three stages,” in Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), 2024, pp. 2181–2211. [44] I. Evtimov, A. Zharmagambetov, A. Grattafiori, C. Guo, and K. Chaudhuri, “Wasp: Benchmarking web agent security against prompt injection attacks,” Advances in Neural Information Processing Systems, vol. 38, 2026. [45] R. Wang, Y. Jia, and N. Z. Gong, “Obliinjection: Order-oblivious prompt injection attack to llm agents with multi-source data,” arXiv preprint arXiv:2512.09321, 2025.

27

[46] Z. Xiang, L. Zheng, Y. Li, J. Hong, Q. Li, H. Xie, J. Zhang, Z. Xiong, C. Xie, C. Yang et al., “Guardagent: Safeguard llm agents by a guard agent via knowledge-enabled reasoning,” arXiv preprint arXiv:2406.09187, 2024. [47] T. Shi, K. Zhu, Z. Wang, Y. Jia, W. Cai, W. Liang, H. Wang, H. Alzahrani, J. Lu, K. Kawaguchi et al., “Promptarmor: Simple yet effective prompt injection defenses,” arXiv preprint arXiv:2507.15219, 2025. [48] C. Disselkoen, A. Eline, S. He, K. Headley, M. Hicks, K. Hietala, J. Kastner, A. Mamat, M. McCutchen, N. Rungta et al., “How we built cedar: A verification-guided approach,” in Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, 2024, pp. 351–357. [49] O. Standard, “extensible access control markup language (xacml) version 3.0,” A:(22 January 2013). URl: http://docs. oasis-open. org/xacml/3.0/xacml-3.0-core-spec-os-en. html, 2013. [50] R. Pang, R. Caceres, M. Burrows, Z. Chen, P. Dave, N. Germer, A. Golynski, K. Graney, N. Kang, L. Kissner et al., “Zanzibar:{Google’s} consistent, global authorization system,” in 2019 USENIX Annual Technical Conference (USENIX ATC 19), 2019, pp. 33–46. [51] N. Li and J. C. Mitchell, “Datalog with constraints: A foundation for trust management languages,” in International Symposium on Practical Aspects of Declarative Languages. Springer, 2002, pp. 58–73. [52] A. C. Myers, “Jflow: Practical mostly-static information flow control,” in Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1999, pp. 228–241. [53] M. Krohn, A. Yip, M. Brodsky, N. Cliffer, M. F. Kaashoek, E. Kohler, and R. Morris, “Information flow control for standard os abstractions,” ACM SIGOPS Operating Systems Review, vol. 41, no. 6, pp. 321–334, 2007. [54] P. Efstathopoulos, M. Krohn, S. VanDeBogart, C. Frey, D. Ziegler, E. Kohler, D. Mazieres, F. Kaashoek, and R. Morris, “Labels and event processes in the asbestos operating system,” ACM SIGOPS Operating Systems Review, vol. 39, no. 5, pp. 17–30, 2005. [55] D. Stefan, A. Russo, J. C. Mitchell, and D. Mazières, “Flexible dynamic information flow control in haskell,” in Proceedings of the 4th ACM Symposium on Haskell, 2011, pp. 95–106. [56] J. Newsome, D. X. Song et al., “Dynamic taint analysis for automatic detection, analysis, and signaturegeneration of exploits on commodity software.” in NDSS, vol. 5, 2005, pp. 3–4. [57] K. Fisler, S. Krishnamurthi, L. A. Meyerovich, and M. C. Tschantz, “Verification and changeimpact analysis of access-control policies,” in Proceedings of the 27th international conference on Software engineering, 2005, pp. 196–205. [58] L. Yuan, H. Chen, J. Mai, C.-N. Chuah, Z. Su, and P. Mohapatra, “Fireman: A toolkit for firewall modeling and analysis,” in 2006 IEEE Symposium on Security and Privacy (S&P’06). IEEE, 2006, pp. 15–pp. [59] M. Bouchet, B. Cook, B. Cutler, A. Druzkina, A. Gacek, L. Hadarean, R. Jhala, B. Marshall, D. Peebles, N. Rungta et al., “Block public access: trust safety verification of access control 28

policies,” in Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2020, pp. 281–291. [60] F. B. Schneider, “Enforceable security policies,” ACM Transactions on Information and System Security (TISSEC), vol. 3, no. 1, pp. 30–50, 2000. [61] J. Ligatti, L. Bauer, and D. Walker, “Edit automata: Enforcement mechanisms for run-time security policies,” International Journal of Information Security, vol. 4, no. 1, pp. 2–16, 2005. [62] ——, “Run-time enforcement of nonsafety policies,” ACM Transactions on Information and System Security (TISSEC), vol. 12, no. 3, pp. 1–41, 2009.

Proofs for the security properties We now state the security properties guaranteed by the runtime semantics. We show that the runtime semantics enforces the security goals defined in Section 3. Intuitively, a trace is valid if it is obtained by starting from an initial runtime state and repeatedly applying runtime transitions. Only transitions that return allow append a step to the trace; transitions that return deny or pause leave the trace unchanged. We start by defining some properties related to the trace. Definition 1 (Reachable Runtime State). A runtime state str k is reachable under schema Γ and policy P if it is obtained from an initial runtime state st0r by a finite sequence of runtime transitions: Γ, P ⊢ ⟨st0r , req1 ⟩ → . . . ⟨stkr , Dk ⟩. If stkr = ⟨M, τ, Lin, ts, Req, Cap⟩, then τ is a valid trace under Γ and P . Theorem 1 (Runtime Preservation). Assume Γ ⊢ P and Γ ⊢ str . If Γ, P ⊢ ⟨str , req⟩ → ⟨st′r , D⟩, then Γ ⊢ st′r . Proof. By case analysis on the runtime transition rule. •

RTA case: The transition is an allowed execution. By rule RTA, there exists a candidate step σ = ⟨ns , e, nd , Lin , Lout , a, d, dp ⟩ such that str , req ⇓ σ and P, str ⊢ σ ⇓ allow . The updated runtime state is st′r = ⟨M [d 7→ Lout ], τ · σ, Lin[d 7→ dp ], ts, Req, Cap⟩. Since Γ ⊢ str , the taint map M , trace τ , lineage map Lin, task scope ts, requirements Req, and capabilities Cap are well-formed under Γ. By candidate-step construction, Lout is produced by label propagation from a well-formed input label; therefore Γ ⊢ Lout . The step σ contains declared nodes, a declared edge, a declared agent, and well-formed labels, so Γ ⊢ σ. Updating M with a well-formed label, appending a well-formed step to a well-formed trace, and updating Lin with parent identifiers from the candidate step preserve well-formedness. All other components of the runtime state are unchanged. Hence Γ ⊢ st′r .

•

RTD case: The transition is denied. By rule RTD, the runtime state is unchanged:st′r = str . Since Γ ⊢ str by assumption, we immediately have Γ ⊢ st′r .

•

RTP case: The transition is paused. By rule RTP, the runtime state is unchanged: st′r = str . Since Γ ⊢ str by assumption, we immediately have Γ ⊢ st′r . 29

Therefore every runtime transition preserves well-formedness of the runtime state. Theorem 2 (Policy Enforcement Soundness). Let str = ⟨M, τ, Lin, ts, Req, Cap⟩ be reachable under Γ and P . For every step σ ∈ τ , σ was appended only after policy evaluation returned allow . Therefore, σ violates no matching deny-flow clause, satisfies all runtime requirements, and does not make the trace violate any forbid path rule in P . Proof. By induction on the length of the trace τ . •

Base case: τ = ϵ means the trace contains no steps; hence proved.

•

Inductive case: Suppose τ = τ ′ · σ for some previous trace τ ′ and last step σ. By the induction hypothesis, every step in τ ′ satisfies the property. It remains to show that the newly appended step σ also satisfies the property. Since σ appears as the last step of a reachable trace, it must have been appended by an allowed runtime transition. Therefore, by rule RTA, there exists a previous runtime state st′r = ⟨M ′ , τ ′ , Lin′ , ts′ , Req ′ , Cap′ ⟩ and a request req such that st′r , req ⇓ σ

and

P, st′r ⊢ σ ⇓ allow .

By rule PEA, policy evaluation can return allow only if σ matches no deny-flow clause, satisfies the relevant runtime requirements, and does not make the extended trace τ ′ · σ violate any forbid path rule in P . Thus σ satisfies the desired property. Since all steps in τ ′ satisfy the property by the induction hypothesis, all steps in τ = τ ′ · σ satisfy the property. Therefore the theorem holds.

Theorem 3 (G1: Flow Policy Enforcement). Let str = ⟨M, τ, Lin, ts, Req, Cap⟩ be reachable under Γ and P . For every step σ ∈ τ , the flow represented by σ satisfies all applicable flow and path constraints in P . Proof. Let σ ∈ τ be arbitrary. Since str is reachable, τ is a valid trace. By Policy Enforcement Soundness2 theorem, σ was appended to the trace only after policy evaluation returned allow . By rule PEA, policy evaluation returns allow only if the candidate step matches no deny-flow clause, satisfies the applicable runtime requirements, and does not make the extended trace violate any forbid path rule in P . Therefore, σ satisfies all applicable flow and path constraints in P . Since σ was arbitrary, every step in τ satisfies all applicable flow and path constraints. Theorem 4 (G2: Delegation Safety). Assume P contains a delegation clearance rule that denies any delegation step sending data with output label Lout to a delegated agent a′ whenever Lout .s ̸⪯s a′ .smax . Then no delegated agent receives data exceeding its authorized sensitivity level in any reachable trace.

30

Proof. Assume, for contradiction, that some delegated agent a′ receives data exceeding its authorized sensitivity level. Then there exists a step σ = ⟨ns , e, nd , Lin , Lout , a, d, dp ⟩ ∈ τ such that e is a delegation edge to a′ and Lout .s ̸⪯s a′ .smax . By the delegation clearance rule, this step matches a deny-flow clause in P . However, by G1, every step in a reachable trace satisfies all applicable flow constraints. In particular, no committed step can match a deny-flow clause. This is a contradiction. Therefore, no delegated agent receives data exceeding its authorized sensitivity level. Theorem 5 (G3: Trust Preservation). Assume no explicit trust-reclassification transformation is applied. If data originates from an untrusted source, then every runtime data object derived from it remains untrusted in the taint map M . Proof. By induction on the lineage recorded in Lin. •

Base case: If a runtime data object d originates from an untrusted source, then input-label resolution assigns it a label L such that L.t = false. When the producing step is allowed, rule RTA records this label in the taint map M .

•

Inductive case: Suppose d is produced from parent objects dp , and some parent di ∈ dp is untrusted: M (di ).t = false. By input-label resolution, the input label Lin is computed from theVlabels of the lineageconnected parent objects. Since trust joins using conjunction, tin = i ti , and at least one parent satisfies ti = false, it follows that tin = false. Hence Lin .t = false. Because no explicit trust-reclassification transformation is applied, label propagation preserves untrustedness: ρ ⊢ Lin ⇓ Lout ⇒ Lout .t = false. Finally, rule RTA updates the taint map with M [d 7→ Lout ]. Thus M (d).t = false.

Therefore, data originating from untrusted sources retains its trust designation unless explicitly reclassified. Theorem 6 (G4: External Disclosure Control). Assume P contains policies that deny sensitive data flows to external sinks unless the flow is explicitly policy-approved. Then sensitive data may reach an external sink only through a policy-approved flow.

31

Proof. Assume, for contradiction, that sensitive data reaches an external sink through a flow that is not policy-approved. Then there exists a step σ = ⟨ns , e, nd , Lin , Lout , a, d, dp ⟩ ∈ τ such that nd is an external sink, Lout is sensitive, and the flow is not approved by P . Since the flow is not policy-approved, either a deny-flow clause matches σ, or an applicable path requirement for external release is not satisfied. In either case, policy evaluation could not return allow by rule PEA. However, since σ ∈ τ , the step was appended to the trace by rule RTA, which requires P, st′r ⊢ σ ⇓ allow for some previous runtime state st′r . This is a contradiction. Therefore, sensitive data may reach external sinks only through policyapproved flows. Theorem 7 (G5: Path Safety). If P contains a forbid path rule with path expression πe , then no reachable trace τ satisfies πe : τ ̸|= πe . Proof. Assume, for contradiction, that there exists a reachable trace τ such that τ |= πe . Then the forbidden multi-step behavior described by πe appears in the trace. Let σ be the last step whose addition makes the trace satisfy πe , and write τ = τ ′ · σ. Since σ ∈ τ , the step was appended by rule RTA. Thus, for some previous runtime state st′r , P, st′r ⊢ σ ⇓ allow . However, by rule PEA, policy evaluation can return allow only if the extended trace does not match any forbid path expression in P . Since τ ′ · σ |= πe , the step could not have been allowed. This is a contradiction. Therefore, no reachable trace satisfies πe .

A

Appendix

Definition 2 (Category Well-Formedness). A category c is well-formed, written ⊢ c if it is generated by the category grammar defined in Figure 2, where each atomic identifier a belongs to the set of atomic categories A. a∈A CAtom ⊢a

⊢c

a∈A CPath ⊢ c.a

Definition 3 (Label Well-Formedness). A label L = ⟨s, C, t⟩ is well-formed under schema Γ, written Γ ⊢ L label, if the sensitivity and trust component are valid, and every category in the category set is well-formed. s ∈ sensitivity ∀c ∈ C. ⊢ c t ∈ {true, f alse} WFL Γ ⊢ ⟨s, C, t⟩; Definition 4 (Node Well-Formedness). A node n = name : ⟨k, L, (x, v), (f, Lf )⟩ is well-formed under schema Γ, written Γ ⊢ n, if the node has a valid kind, its node label is well-formed, its attributes are well-formed, and its field labels are well-formed. 32

k ∈ kind

Γ⊢L

∃T, i. name = T :: i

∀(x, v) ∈ (x, v). x ∈ dom(Σ) ∀(x, v) ∈ (x, v). Γ ⊢ v : Σ(x) ∀(f, Lf ) ∈ (f, Lf ). f ∈ dom(Σf ) ∀(f, Lf ) ∈ (f, Lf ). Γ ⊢ Lf unique(x)

unique(f ) WFN

Γ ⊢ name : ⟨k, L, (x, v), (f, Lf )⟩ Definition 5 (Edge Well-Formedness). An edge e = ename : ⟨n1 , n2 , ρ⟩

is well-formed under schema Γ, written Γ ⊢ e, if the edge name is valid, both endpoint nodes are declared in the schema, and the propagation specification is well-formed. n1 = name1 : ⟨k1 , L1 , (x1 , v1 ), (f1 , Lf1 )⟩ ∈ N n2 = name2 : ⟨k2 , L2 , (x2 , v2 ), (f2 , Lf2 )⟩ ∈ N ( ) (source, internal), (source, sink), (k1 , k2 ) ∈ (internal, internal), (internal, sink) ρ ∈ prop ρ =⇝ (r) ⇒ ∀r ∈ r. r ∈ rule ρ =≡ s ⇒ s ∈ sensitivity Γ ⊢ n1 Γ ⊢ ename : ⟨n1 , n2 , ρ⟩

Γ ⊢ n2

WFE

Definition 6 (Agent Well-Formedness). An agent a = (aname, name) : ⟨s, e, a, b, ap ⟩ is well-formed under schema Γ, written Γ ⊢ a, if the agent name is valid, the referenced node exists, the sensitivity bound is valid, referenced edges are declared and respect the sensitivity bound, and delegated agents are declared. ∃T ′ , i′ . name = T ′ :: i′

s ∈ sensitivity

b ∈ {true, false} ∀e′ ∈ e. e′ = ename : ⟨n1 , n2 , ρ⟩ ∈ E ∀e′ ∈ e. e′ = ename : ⟨n1 , n2 , ρ⟩ ∈ E sens(n1 ) ≤ s

sens(n2 ) ≤ s

∀e ∈ e, Γ ⊢ e

∀a′ ∈ a. a′ ∈ A ∀ap ∈ ap . ap ∈ A Γ ⊢ (aname, name) : ⟨s, e, a, b, ap ⟩

WFA

Definition 7 (Task-Scope Well-Formedness). A task scope ts = (tname, name) : ⟨ein , eout ⟩ is well-formed under schema Γ, written Γ ⊢ ts, if the task name is valid, the referenced node is declared, and all input and output edges are declared in the schema. 33

∃T, i. tname = T :: i

∃T ′ , i′ . name = T ′ :: i′

name ∈ N ∀e ∈ ein . e ∈ E ∀e ∈ eout . e ∈ E Γ ⊢ (tname, name) : ⟨ein , eout ⟩

WFTS

Definition 8 (Clause Well-Formedness). A clause cl = ⟨nsϕ , ndϕ , eϕ , Lϕ , aϕ , ϕ, ϕreq ⟩ is well-formed under schema Γ, written Γ ⊢ cl, if all predicate components are well-typed over their corresponding runtime objects. Definition 9 (Flow Well-Formedness). A flow declaration f = (f⊢ , f name) : cl is well-formed under schema Γ, written Γ ⊢ f , if the flow permission is valid, the flow name is valid, and the clause is well-formed. f⊢ ∈ fperm

∃T, i. f name = T :: i Γ ⊢ (f⊢ , f name) : cl

Γ ⊢ cl WFF

Definition 10 (Edge-Match Well-Formedness). An edge match em = ename : ⟨nsϕ , ndϕ , Lϕ ⟩ is well-formed under schema Γ, written Γ ⊢ em , if the edge name has the form T :: i and all predicate components are well-typed over their corresponding runtime objects. Definition 11 (Path-Expression Well-Formedness). A path expression πe is well-formed under schema Γ, written Γ ⊢ πe , if every edge match appearing in πe is well-formed, every composed {m,n} subexpression is well-formed, and every bounded repetition πe satisfies 0 ≤ m ≤ n. Definition 12 (Path Well-Formedness). A path π = (π⊢ , pname) : ⟨πe , e, πϕ , scope⟩ is well-formed under schema Γ, written Γ ⊢ π, if the path permission is valid, the path name has the form T :: i, the path expression is well-formed, all referenced edges are declared, the path predicate is typed over traces, and the scope is valid. Definition 13 (Policy Well-Formedness). A policy P = ⟨f , π⟩ is well-formed under schema Γ, written Γ ⊢ P , if every flow and path declaration appearing in the policy is well-formed.

34

Related documents

• LLM-Based Agents for Software and Systems Security: Approaches, Applications, and Assessment#618499
• AgentRedBench: Dynamic Redteaming and Integration-Aware Defense for LLM Agents over SaaS Integrations#246421
• Understanding and Mitigating Prompt Leaking Attacks in Real-World LLM-Based Applications#287061
• AGATE: Provenance-Based Runtime Defense Against Compositional Attacks on LLM Agents#1105389
• LatentSift: Policy-State Filtering for Token-Efficient Verification of Software Engineering Agents#1131213