PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Basavesh Ammanaghatta Shivakumar, Swarn Priya, Peng Gao

arXiv:2608.22868v1cs.CR

TL;DR

LLM-agent harms often arise when sensitive or untrusted data travels through otherwise plausible multi-step actions, a gap that isolated request authorization does not capture. AgentFlow addresses this with labeled flow and path policies, runtime mediation, and bounded SMT verification; preliminary evaluations report zero confirmed compromise on AgentDojo and AgentDyn under configured policies. The evidence remains scoped to modeled policy-visible behaviors, evaluated benchmarks, and the trusted enforcement interface.

  • Problem

    Agent systems need end-to-end control over how data origin, transformations, and later influence shape tool calls, response sinks, and delegation, beyond isolated request authorization.

  • Method

    AgentFlow combines a flow-centric policy language over labeled runtime edges and paths with a runtime reference monitor and bounded SMT verification for a structured policy fragment.

  • Results

    AgentFlow reduces confirmed compromise from 33.0% to 0.0% on 949 AgentDojo injected cases while raising aggregate utility from 46.7% to 63.3%.

  • Takeaways & Limitations

    The configured policies block the policy-visible attacker flows examined in the evaluated benchmarks while preserving useful task completion under those policies.

  • Takeaways & Limitations

    The results are scoped to policy-visible mediated behaviors, evaluated benchmarks, and a trusted correctly implemented runtime; overtainting can reduce utility in message-heavy workflows.

Abstract

from arXiv · show

LLM agents increasingly read untrusted content, invoke external tools, access private data, and delegate work to other agents. Harm often arises not from a single unsafe action but from the flow of sensitive data across a sequence of otherwise plausible steps. We present AgentFlow, a flow-centric policy language and runtime enforcement model for specifying where data may travel in agent systems. Policies are defined over labeled runtime edges and constrain 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 mediates agent actions, and a bounded SMT-based verifier checks safety properties for a structured policy fragment. We evaluate AgentFlow on multiple agent benchmarks. In our prototype, seven safety properties verify in under 0.5 seconds each, and the verifier catches all seeded unsafe policy variants in our study. On 949 AgentDojo injected 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 benchmark, 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 replays suggest that the configured policies block the benchmark-specified policy-visible attacker flows; in ASB's direct-prompt-injection harness, attack success is 0/1{,}200. These results are preliminary and scoped to the modeled policy-visible agent behaviors and evaluated benchmarks.

1 Introduction

AgentFlow frames agent security as controlling sensitive and untrusted data across labeled execution edges and multi-step histories, rather than authorizing isolated requests. It combines declarative policies, formal semantics, runtime mediation, and bounded verification, with preliminary benchmark evidence scoped to policy-visible behavior.

  • Agent failures can emerge across plausible sequences involving untrusted content, private data, tools, external services, and delegated agents.
  • Request-level authorization does not preserve data origin, transformations, or downstream influence across an agent execution.
  • AgentFlow uses flow rules for individual execution edges and path rules for multi-step histories over labeled executions.
  • Its formal model includes a multi-dimensional label lattice, provenance graph, execution traces, propagation functions, and small-step operational semantics.
  • The bounded SMT verifier checks properties including non-leakage, privilege-escalation resistance, delegation safety, trust-preserving flows, and taint monotonicity, or produces counterexample traces.
  • The prototype verifies seven safety properties in under 0.5 seconds each and reports preliminary evidence on AgentDojo, AgentDyn, and replay-based benchmarks.

2 Background and Motivation

Agent systems can turn individually legitimate database reads, summarization, delegation, and external writes into unsafe flows when untrusted or confidential data crosses their sequence. AgentFlow addresses this gap by tracking provenance and labels while enforcing constraints over tool calls, sinks, and execution histories.

  • Modern agents combine planning loops with tools that query databases, access files, retrieve web content, send email, execute code, and delegate work.
  • 2.1 Motivating Example: The example agent has user and transaction databases, corporate email and Slack, a third-party-capable summarizer, and a web-browsing research sub-agent.
  • 2.1 Motivating Example: Figure 1's architecture compiles and verifies policies before deployment, then mediates runtime tool calls and modeled response sinks with Allow, Deny, or Pause outcomes.
  • 2.1 Motivating Example: Trust laundering occurs when web content is treated as a verified internal policy update.
  • 2.2 Request-Level Authorization Is Not Enough: Request-level authorization decides individual principal-action-resource permissions but does not by itself enforce provenance- and history-sensitive constraints.
  • The motivating enterprise scenario treats separate database queries, summarization, and email as legitimate, but their chain can release confidential data without approved declassification.

3 Threat Model

AgentFlow models attacks that manipulate policy-visible mediated behavior while assuming a trusted, correctly implemented runtime and loaded policy. Its security goals cover constrained flows, delegation, trust labels, approved releases, and prohibited multi-step behaviors.

  • The model includes users, agents, tools, data sources, sinks, and optional sub-agents, with the runtime mediating tool invocations and modeled response sinks.
  • AgentFlow is a policy-enforcement layer rather than a general LLM alignment or program-verification system.
  • In-scope attackers include indirect prompt injectors, malicious tool providers, and compromised sub-agents influencing policy-visible behavior.
  • Jailbreaks, hallucinations, incorrect advice, covert channels, trusted-component compromises, and paths bypassing the reference monitor are outside the model unless they become modeled policy violations.
  • The runtime enforces flow and path constraints, authorized delegation sensitivity, persistent untrusted markings, approved external releases, and blocked prohibited paths.

4 AgentFlow Language Design

AgentFlow models agent security around labeled data flows, runtime provenance, and policy-controlled execution edges. Its language combines multidimensional labels, graph edges, agents, task scopes, flow rules, and path rules to constrain data movement and multi-step behavior.

  • AgentFlow organizes its language around a label system, flow graphs, flow rules, and path rules.
  • Label System: Labels classify data by sensitivity, category set, and trust, with ordering that restricts untrusted data from flowing into trusted destinations.Sensitivity controls confidentiality, categories support hierarchical field distinctions, and trust records source reliability.
  • Flow Graph Model: Runtime provenance is append-only: operations create trace events and fresh outputs linked to parent objects, enabling lineage- and session-scoped path evaluation.The static schema names policy-visible node and edge types but is not itself a control-flow graph.
  • Flow Graph Model: Nodes represent sources, sinks, and computation components, while edges specify permitted operations and label propagation semantics.Propagation can preserve labels, transform them for sanitization or controlled declassification, conservatively approximate opaque operations, or replace them with constants.
  • Agent and Task Scopes: Agents combine ownership, maximum sensitivity, authorized edges, delegation permissions, and parent relationships; task scopes add temporary least-privilege restrictions.Sub-agents can operate with independent clearance levels and restricted edge sets, while task scopes can explicitly permit or deny edges for a specific execution.

5 Formal Semantics

AgentFlow formalizes runtime information flow as taint- and lineage-aware execution steps, then evaluates flow and temporal path policies before committing each step to the trace.

  • Runtime Enforcement: Runtime enforcement intercepts each tool invocation, computes propagated labels, evaluates flow and path policies, and updates execution lineage.Each intercepted request yields a policy decision determining whether execution may proceed.
  • Runtime Data and Lineage: Concrete runtime data objects receive identifiers, enabling causal taint tracking, lineage-aware propagation, and path-sensitive enforcement across multi-step executions.Execution steps record nodes, edges, labels, agents, produced data, and lineage dependencies.
  • Runtime State: Runtime states maintain taint maps, execution traces, lineage relations, active task scopes, approved requirements, and active capabilities.Capabilities can be required for a request to proceed, while task scopes restrict usable edges.
  • Label Propagation Semantics: Input labels are resolved from source nodes, selected fields, and lineage-connected data objects before edge-specific propagation computes output labels.Field-sensitive access joins only referenced field labels rather than using the entire source node.
  • Path Matching Semantics: Path expressions match execution traces using edge matching, sequential composition, adjacency constraints, choice, and bounded repetition.Require rules demand matching edges, whereas forbid rules prohibit matching temporal trace patterns.
  • Policy Evaluation Semantics: Policy evaluation allows a candidate step only when flow clauses, path constraints, runtime requirements, and referenced capabilities all succeed.Otherwise, the step receives a deny or pause decision depending on the failing condition.
  • Runtime Transition Semantics: Allowed execution proceeds by intercepting requests, constructing candidate steps, evaluating policies, and updating runtime state.The resulting trace records the sequence of allowed steps, including retries and memory updates, while provenance remains acyclic.

6 Static Verification and Analysis

AgentFlow combines schema well-formedness checks with bounded SMT verification and runtime theorems covering policy enforcement, delegation, trust, and external disclosure.

  • Static Verification: The verifier reduces bounded AgentFlow policy properties to SMT constraints over symbolic steps, labels, lineage links, capabilities, and path rules.SAT models are decoded as counterexample traces; UNSAT means no violating bounded abstract trace exists.
  • Schema Well-Formedness: Static well-formedness checks ensure declared references, labels, propagation functions, node connections, capabilities, delegation targets, and policy entities are valid.These checks establish assumptions required by both operational semantics and static verification.
  • Verification and Runtime Guarantees: The verifier checks bounded instances of the same safety goals enforced by the runtime, while separate theorems establish guarantees for mediated traces.The runtime results include preservation and policy-enforcement soundness claims.
  • Security Guarantees: Delegation safety ensures that, under an appropriate clearance rule, no delegated agent receives data above its authorized sensitivity level.The result holds for every reachable trace under the stated assumption.
  • Security Guarantees: Without explicit trust reclassification, data originating from an untrusted source remains untrusted in the taint map through derived runtime objects.This is the stated trust-preservation condition.
  • Security Guarantees: Sensitive data reaches external sinks only through authorized flows when policies deny unapproved disclosures and no deny or path rule blocks the authorized flow.The guarantee is conditional on the configured policy and runtime assumptions.

7 Implementation

The prototype compiles AgentFlow policies, validates them, and mediates tool calls through capability, label, flow, path, and state-update checks.

  • Prototype Architecture: The prototype is a Python policy engine containing a compiler, runtime monitor, and SMT verifier.The compiler translates policy files into an internal runtime representation.
  • Validation: Compilation rejects malformed syntax, invalid sensitivity or flow/path effects, unknown propagation operators, and unresolved provider side-channel references.Runtime-dependent references are deferred to interception-time checks.
  • Runtime Mediation: The runtime identifies the source, destination, and edge, then checks active task scopes, required capabilities, and runtime requirements before execution.Unknown runtime entities deny rather than silently allowing the call.
  • Label Tracking: Label computation combines propagation functions, selected-field labels, release contexts, and optional scanners to determine the output label.Field-level tracking can reduce overtainting, while scanners can upgrade labels when sensitive patterns appear in LLM output.
  • Decision and State Update: Flow, side-channel, and path rules are evaluated before the runtime returns ALLOW, DENY, or PAUSE.On ALLOW, the engine updates taint, lineage, and trace state.
  • Framework Integration: Middleware integrates AgentFlow with agent frameworks by mapping tool calls to policy edges and executing the original tool only after an allow decision.The integration preserves the framework’s tool interface while inserting the runtime check.

8 Evaluation

The evaluation studies security, utility, transfer, breadth, verification, and latency questions using frozen AgentDojo and AgentDyn runs plus replay-based benchmark checks.

  • Policy Structure: Policies are written once per suite and model sensitive sources, untrusted inputs, protected sinks, and task-scoped releases.Sensitivity, category, and trust labels serve distinct policy roles.
  • Evaluation Setup: AgentDojo contains 949 injected cases across Banking, Travel, Workspace, and Slack, evaluated with utility and confirmed-compromise outcomes.The study also includes a 200-case AgentDyn Dailylife run and five breadth checks.
  • AgentDojo Results: 63.3% utility versus 46.7% and 0.0% confirmed compromise versus 33.0% are reported for AgentFlow versus the baseline across 949 AgentDojo cases.The compromise column counts confirmed attack success rather than blocked, failed, or ambiguous cases.
  • Mechanism Ablation: A6 raises Travel utility from 3/12 to 11/12 and Banking utility from 3/12 to 8/12 while retaining zero confirmed compromise on the diagnostic slices.The full configuration adds scoped capabilities and release contexts after earlier structural defenses proved too conservative.
  • Breadth Checks: The breadth checks report blocked or prevented unsafe flows, while deterministic replay benign-side counts are policy-gate pass counts rather than final-answer utility.ASB is separately qualified because its reported task success differs from benign policy-gate pass rate.
  • AgentDyn Stress Test: AgentDyn 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 run includes 138 terminal policy blocks, mostly associated with missing scoped capabilities for dynamic task families.

8.5 Breadth and Replay Checks

Breadth replays test whether configured policies block benchmark-specified attacker flows, while verifier and overhead measurements assess pre-deployment checking and runtime cost. The comparisons are scoped to policy-facing mechanisms and preliminary prototype evidence.

  • Breadth and replay checks: Policy-gate replays block modeled attacker flows across tool-registry, prompt-injection, response-sink, harmful-sequence, and poisoned-MCP scenarios.These checks assess policy-gate coverage rather than end-to-end agent utility.
  • Verifier checks: 12/12 seeded unsafe policy variants are caught by the verifier.The study includes overbroad releases, PII and credential leaks, third-party sharing, trust laundering, overpermission, and selected-field leaks.
  • Verifier checks: All properties verify (UNSAT) with k=10, and the largest checked-in policy remains within sub-second solving.The largest policy has 28 edges, 17 nodes, and 30 flow/path/release rules.
  • Runtime overhead: 6.4 µs average per-intercept latency is negligible relative to 1–10 seconds of LLM inference.Measured P50, P95, and P99 latencies are 6.0, 8.7, and 9.7 µs, respectively.
  • Comparison with related defenses: AgentFlow reaches 63.3% utility versus 60.1% for the reproduced CaMeL artifact, an artifact-level comparison rather than a security ranking.The comparison uses a denominator-aligned reproduction on the AgentDojo configuration.
  • Limitations and discussion: Overtainting can block benign tasks when workflows mix trusted and untrusted content or lack explicit release contexts.The verifier's guarantees also apply only to its bounded, structured abstraction.

9 Related Work

AgentFlow builds on research in agent defenses, authorization, information-flow control, symbolic verification, and reference monitoring. Its distinguishing interface applies labeled flow and path policies to runtime agent operations rather than embedding enforcement in one architecture.

  • Agent defenses: Prior agent defenses address tool privileges, delegation, runtime traces, task policies, isolation, guard agents, sanitization, and permission prediction.The cited systems make different choices about where policies live and how they are checked.
  • Closest related systems: FORGE, FIDES, CaMeL, and SAMOS use dependency-graph policies, planner taint tracking, privileged/quarantined planning, or MCP IFC gateways.AgentFlow instead uses labeled runtime edges, path rules, task-scoped capabilities, and bounded SMT checks.
  • Authorization and information flow: Traditional authorization decides whether a principal may act on a resource, whereas AgentFlow tracks how content from one step may influence later actions or sinks.This extends the request-level view with data-flow state.
  • Information-flow control: AgentFlow adapts classical lattice labels, declassification, and dynamic taint analysis to monitored tool and model calls.LLM agents expose calls rather than transparent program dependencies.
  • Policy verification: The verifier applies SMT-style pre-deployment checking to bounded agent properties involving label propagation, graph reachability, and path patterns.This connects AgentFlow to established symbolic policy-analysis techniques.
  • Runtime enforcement: The runtime follows reference-monitor traditions while reasoning over labels, provenance, capabilities, and paths instead of low-level system calls.It mediates agent tool calls and modeled response sinks.

10 Conclusion

AgentFlow is presented as a policy language and runtime monitor for controlling data movement through tool-using LLM agents. The prototype combines runtime enforcement and bounded SMT checks, with preliminary evidence of blocking modeled benchmark attacks while retaining useful task completion.

  • Conclusion: AgentFlow controls data movement through tool-using LLM agents by tracking labels, provenance, and execution history.This supports constraints that request-level checks miss, including multihop exfiltration, trust laundering, unsafe delegation, and temporal attack patterns.
  • Conclusion: Runtime enforcement with bounded SMT checks blocks the policy-visible attacks examined in the benchmarks while preserving useful task completion under configured policies.The authors characterize this as preliminary evaluation evidence motivating application-specific development and validation.

Proofs for the security properties

The proofs establish that allowed runtime transitions preserve well-formedness and enforce applicable flow, path, delegation, trust, and external-disclosure policies. Each guarantee depends on the trusted runtime, policy assumptions, and the semantics of allow, deny, and pause transitions.

  • Runtime preservation: Allowed transitions update labels, traces, and lineage while preserving runtime-state well-formedness; denied and paused transitions leave the state unchanged.This is the Runtime Preservation result for reachable states under schema Γ and policy P.
  • Policy enforcement soundness: Every committed trace step was appended only after policy evaluation returned allow, so it violates no matching deny-flow clause or forbid path rule.This is the Policy Enforcement Soundness theorem.
  • Flow and path enforcement: Every reachable step satisfies applicable flow and path constraints under the policy.The result follows from soundness and the allow condition in policy evaluation.
  • Delegation safety: A delegation clearance rule denying excessive sensitivity implies that no delegated agent receives data above its authorized sensitivity level.The guarantee is conditional on the policy containing the stated delegation rule.
  • Trust preservation: Without explicit trust reclassification, data originating from an untrusted source remains untrusted through lineage-connected propagation.The proof relies on trust joining by conjunction and propagation preserving untrustedness.
  • External disclosure control: Sensitive data reaches an external sink only through a policy-approved flow when policies deny unapproved sensitive disclosures.This guarantee is conditional on the relevant external-disclosure policies.
  • Path safety: A forbid path rule ensures that no reachable trace satisfies its prohibited multi-step path expression.Policy evaluation rejects the transition that would complete the forbidden path.

A Appendix

The appendix defines well-formedness conditions for AgentFlow’s schema objects, policy declarations, and path expressions. These checks validate names, references, types, permissions, scopes, and allowable edge structures.

  • Core schema objects: Categories and labels are well-formed when category grammar, sensitivity, trust, and category-set requirements are satisfied.
  • Core schema objects: Nodes and edges require valid kinds or names, declared endpoints, well-formed labels or propagation specifications, and correctly typed attributes and fields.
  • Agent and task declarations: Agents and task scopes must reference declared nodes and edges while satisfying valid names, sensitivity bounds, and declared delegation relationships.
  • Policy declarations: Clauses, flows, and edge matches are valid when predicates are typed, permissions and names are valid, and referenced runtime structures are well-formed.
  • Path declarations: Path expressions and paths require well-formed edge matches and compositions, valid bounded repetition, declared edges, trace-typed predicates, permissions, names, and scopes.
  • Policy structure: Policies are well-formed when every flow and path declaration they contain is well-formed, and the schema permits source, internal, and sink edge combinations.
Loading 2608.22868v1…