AgentFlow：面向 LLM 智能体系统的流中心策略语言与运行时防护框架

如何把敏感或不可信数据在 LLM 智能体中的跨步流动写成可执行策略。

• 场景：作者认为危害常来自一串各自看似合法的动作，而不只是单次危险调用。读记录后把机密字段经摘要送到外部邮箱、把网页文本当成内部指令、或委托时带出过高数据，都是文中的失败形态。
• 现有不足：作者认为 Cedar 等请求级授权不提供端到端数据流状态。作者称近期防御提高了安全性，但策略所在位置和检查方式不同；操作者未必控制架构，工具还可动态注册。
• 本文做法：AgentFlow 用带标签运行时边上的流规则和路径规则描述约束，由引用监控器在执行时强制，并对结构化片段做有界 SMT 检查。作者称范围限于策略可见的中介行为。
• 威胁模型
  • 目标：造成违反已配置策略的 policy-visible 流，即中介工具调用、委托、数据释放或建模的响应汇输出。
  • 攻击者：间接提示注入者控制外部内容；恶意工具提供者控制工具元数据或输出；被攻陷子智能体试图提权、影响他方或外泄。不能改运行时、已加载策略、已审查工具，也不能绕过中介路径。
  • 系统：用户、智能体、工具、数据源、数据汇和可选子智能体。运行时被假定可信且正确实现。信任边界为 user–agent、agent–tool、agent–sub-agent、agent–external system 和 agent–tool registry。
  • 非目标：越狱、幻觉、错误建议和误导性回答不在范围内，除非造成中介违反或到达受保护汇。不判断已允许调用的任务语义。未表示为汇的隐蔽信道、可信组件缺陷和绕过监控器的路径不覆盖。给定可信运行时和正确策略，作者要强制 §3 的五项性质。

工具型智能体攻击

• 间接注入：Greshake et al. (2023) 提出针对 LLM 集成应用的间接提示注入。AgentDojo 与 InjecAgent 在工具型智能体中研究同一失败模式。
• 后续基准：BIPIA 关注最终回答操纵；AgentDyn 用动态生成任务；AgentHarm 研究有害工具请求；ASB 扩大任务和工具面；MCPTox 针对被投毒的 MCP 元数据。
• 其他入口：论文还写到工具选择、记忆、日志、网页内容和多智能体通信。作者称这些攻击促使跟踪不可信或敏感内容的后续使用，而不只过滤可疑提示。

智能体防御

• 栈上不同位置：Progent 控制工具权限；SEAgent 把强制访问控制用于委托；Conseca 生成任务策略；AgentArmor 分析运行时轨迹。论文还提到隔离或完整性护栏、守卫智能体、提示消毒和权限预测。作者称本文的补充是把谱系、标签和路径约束做成显式策略对象。
• 最近的强制系统：FORGE 在依赖图上用 Datalog；FIDES 把污点跟踪嵌进规划器；CaMeL 把特权规划与被隔离的数据处理分开；SAMOS 在 MCP 工作流外包一层信息流网关。作者称本文接口不同：带标签运行时边、路径规则、任务作用域能力和有界 SMT 片段。

授权与信息流

• 请求级授权：Cedar、XACML、Zanzibar 和基于 Datalog 的语言判断主体能否对资源动作；Zelkova 用 SMT 分析这类策略。作者称 AgentFlow 要记一步取得的内容如何影响后来的动作或汇。
• 经典信息流：Denning 的格、Myers 与 Liskov 的去中心化标签，以及 Jif、Flume、Asbestos、LIO，在常规程序里强制标签。降密与动态污点分析影响传播模型。作者称智能体暴露的是工具和模型调用，不是透明程序依赖，因此把调用当作被监控的数据流步骤，并增加路径规则。

验证与引用监控

• 部署前分析：验证器使用 Z3。Margrave 分析访问控制策略，FIREMAN 检查防火墙规则，云策略验证在部署前寻找错误配置。作者称把这种检查用于有界的标签传播、图可达性和路径模式。
• 执行监控：Schneider 刻画执行监控器可强制的策略；Ligatti 等研究 edit automata；SASI 做内联引用监控。作者称本文中介的是工具调用和建模的响应汇，推理对象是标签、来源、能力和路径，而不是底层系统调用。

基线与基准：主基线是无防御系统，并复现 Progent 的公开手工策略路径。CaMeL 公开产物只作工件级比较，作者称不是安全排名。基准为 AgentDojo、AgentDyn、ASB、InjecAgent、BIPIA、AgentHarm 和 MCPTox。

作者称目标不是宣称信息流控制或引用监控是新的，而是在操作者未必控制架构、工具可动态注册时，把这些检查做成写在带标签运行时边上的显式策略层，并在执行时和部署前检查。

AgentFlow 把检查写成带标签执行边上的声明式规则：运行时引用监控器在工具调用和建模的响应汇上返回 Allow、Deny 或 Pause；部署前对有界结构化片段做 SMT 检查（Figure 1）。

标签、节点与智能体

• 三维标签：标签为 L=⟨s, C, t⟩，即敏感度、类别集和信任位。敏感度从 Public 到 TopSecret 共五级。类别是层次路径。信任为布尔值，网页抓取等不可信来源为 false。序为 ℓ₁ ⊑ ℓ₂ ⟺ s₁ ⪯_s s₂ ∧ C₁ ⊆ C₂ ∧ (t₁ ∨ ¬t₂)，作者用其中的信任约束阻止不可信数据流入可信目的地。连接取较高敏感度、类别并集和信任合取。
• 流图：模式只声明节点和边的类型，不是控制流图。允许的操作追加轨迹事件并分配新数据对象；谱系只追加、保持无环。节点带种类、标签、元数据和可选字段标签；边带传播模式。
• 传播：继承不改标签；变换可删类别、降敏感度或改信任，作者将其对应受控降密；不透明传播输出 ⟨high, ∅, false⟩，用于 LLMCall、CodeExecute 等黑盒；常量标签忽略输入。Figure 3 中 LLMCall 还会流向提供者汇。
• 主体与作用域：智能体有敏感度上限、可调用边、可委托对象和可选父智能体。Figure 4 中 main 上限为 Confidential，researcher 上限为 Internal 且不能再委托。任务作用域在单次任务上临时规定允许边和禁止边。

流规则与路径规则

• 单跳：流规则为 allow 或 deny。子句可约束源、目的、边、传播后标签、智能体和运行时上下文；allow 还可要求授权谓词为真。默认拒绝；两者同时匹配时 deny 优先，作者称遵循 Cedar 的冲突消解。
• 流规则例子：Figure 5 包括身份类数据不得进入外部汇、凭证不得离开、数据敏感度不得高于智能体上限，以及不可信且可能含指令的数据不得进入规划器。
• 多步：路径规则为 require 或 forbid，范围是 lineage 或 session。表达式包括单步匹配、顺序、最终跟随、紧邻且下一步不匹配、选择和有界重复。
• 路径例子：Figure 6 要求身份类数据到外部汇的路径含清洗、涂黑或加密；禁止信任提升后到达外部汇；禁止连续 Delegate 不少于 4 次；禁止机密查询最终跟外部写出，除非路径含清洗、涂黑或人工复核。

运行时语义

• 状态与请求：状态含污点映射、轨迹、谱系、当前任务作用域、已批准要求和活跃能力。请求含智能体、边、源、目的、输入数据标识、访问字段、释放上下文和可选能力。决策为 allow、deny 或 pause。
• 标签计算：整源读取用源标签；指定字段时只连接这些字段；谱系对象连接父标签。再按边的传播模式得到输出标签，构成候选步。
• 提交条件：allow 要求没有 deny 流子句匹配、所需流条件满足、扩展轨迹不匹配 forbid 路径、require 路径满足，且引用的要求与能力成功。deny 子句匹配则 deny；某授权要求为假则 pause。只有 allow 更新污点、谱系和轨迹。

部署前检查与定理

• 验证器：先做模式良构检查（附录 A）。验证器把策略和界 k 译成 Z3 约束，符号化边、节点、智能体、标签、谱系和路径匹配。SAT 则给出反例轨迹；UNSAT 表示该抽象下没有违反的有界轨迹。作者称这不是关于任意无界 LLM 行为的保证。每次检查从零重建编码。
• 定理：论文给出 Theorem 1–6：运行时保持良构；可达轨迹中的步只在 allow 之后追加，并满足适用的流与路径约束。委托安全、信任保持和外部披露都带策略假设，例如存在委托许可规则、没有显式信任再分类、去外部汇的敏感流除非获批否则被拒绝。证明部分的 Theorem 7 称，若策略含 forbid 路径，可达轨迹不满足该表达式。

原型

• 组件：Python 策略引擎，含编译器、运行时监控器和 SMT 验证器。编译器做语法与模式检查；未知智能体、边、节点、能力或任务作用域在拦截时拒绝。实现与验证器还处理释放规则；Figure 2 的策略对象由流规则和路径规则组成。
• 接入：中间件包住工具函数。LangChain 包装器保持原接口，执行前把工具名和参数映射到边、源、目的、字段和能力。deny 或 pause 时不调用工具。AgentDojo 与 AgentDyn 适配器做套件专用映射。
• 字段与扫描：指定字段时，输入标签是这些字段的连接，而不是整节点标签。带 runtime_scan 的边可用回调提升输出标签。作者称扫描器是保守的标签升级器，不是语义安全分类器；假阴性不在形式保证内，除非对应汇或释放已被策略建模。

实验设置

• 模型配置：冻结的 AgentDojo、AgentDyn，以及分母对齐的 Progent 比较，使用固定 frontier LLM，论文未给出型号。ASB 上游 DPI 使用该工件的模型配置。其余广度检查是确定性回放。
• 规模：AgentDojo 有 949 例注入用例，每例把良性任务与注入攻击配对：Banking 144、Travel 140、Workspace 560、Slack 105。AgentDyn 的 Dailylife 为 200 例。ASB 有 10 个场景、51 个良性任务、20 个正常工具和 400 个攻击者工具。
• 基线：主基线是无防御系统。Progent 走公开手工策略路径，且为同一模型族。CaMeL 的公开产物只作工件级效用比较。
• 指标：utility 是注入用例上的良性任务完成率；confirmed compromise 只计确认攻击成功。作者不用 AgentDojo 原始 security 位，而用四类后处理：compromise_confirmed、blocked_terminal、benign_failure_or_task_drop、ambiguous。
• 策略：每个套件写一份，不按任务或攻击实例特化。Table 1 概括敏感或不可信输入、受保护汇和代表性规则，例如资金流动作用域、任务作用域的预订能力、分类型释放，以及把频道、私信和网页汇分开。
• 判定与重复：分类由工件中的分类脚本完成。论文未说明该脚本是否为 LLM，未报告与人工的一致性，也未报告重复次数。验证器用 Z3，界 k=10。

主结果

据 Table 2。列为 Util.% 与 Comp.%。论文未点名 frontier LLM。

Swipe horizontally to read the table

套件	基线效用	基线妥协	AgentFlow效用	AgentFlow妥协
Banking	75.7%	66.0%	81.9%	0.0%
Travel	44.3%	25.7%	60.7%	0.0%
Workspace	36.1%	16.6%	57.3%	0.0%
Slack	66.7%	84.8%	73.3%	0.0%
合计	46.7%	33.0%	63.3%	0.0%

• 作者解读：作者称四套件的确认妥协均为表中的零，并认为部分阻断使智能体不再跟随注入干扰。作者把效用代价归于旅行门控、Slack 消息与网页限制、银行资金控制和 Workspace 外部邮件控制。
• Progent：作者称在分母对齐的公开手工策略比较中，Slack 对照为效用 55.2%、妥协 5.7%，Banking 对照为 72.2% 与 0.0%，并称 AgentFlow 高于该对照。Travel 与 Workspace 的 Progent 工作负载更小，正文未给数字。
• 读表条件：效用是注入用例上的任务完成，不是单独的无攻击效用。妥协列不含仅被阻断、任务失败或无法评估的情形。

机制消融

Table 3 是最新代码上的 12 例诊断切片，不是 Table 2 的冻结全量。A0 为无防御，A2 仅流规则，A3 加路径，A4 再加谱系，A6 为含任务作用域能力和释放上下文的完整配置。

Swipe horizontally to read the table

切片	指标	A0	A2	A3	A4	A6
Travel	效用	4/12	3/12	3/12	3/12	11/12
Travel	妥协	7/12	0/12	0/12	0/12	0/12
Slack	效用	11/12	3/12	3/12	3/12	11/12
Slack	妥协	11/12	3/12	4/12	4/12	0/12
Banking	效用	9/12	3/12	3/12	3/12	8/12
Banking	妥协	12/12	0/12	0/12	0/12	0/12

• 作者解读：作者称早期结构防御能降低妥协，但对效用过保守；A2–A4 分不清攻击者引起的副作用和任务授权的副作用。A6 在这些切片上恢复良性完成，并保持确认妥协为零。
• 例外：作者未解释 Slack 妥协列中 A3、A4 相对 A2 的变化。作者称完整策略补上了频道、私信、网页和最终回答汇的缺口，并使该切片效用与 A0 相同。

AgentDyn 与广度回放

• 动态任务：AgentDyn 的 200 例 Dailylife 上，确认妥协从 147/200（73.5%）到 0/200（0.0%），效用从 89/200（44.5%）到 87/200（43.5%）。运行时阻断 319 次工具调用，涉及 143 例，其中 138 次为终止性策略阻断。作者认为机制转到了更开放的任务分布，同时初版策略仍缺动态任务族的释放上下文和能力授予。
• 广度：除 ASB 上游 DPI 外为确定性策略门回放。作者称这测的是策略门覆盖，不是端到端效用；良性侧是策略门通过数。ASB 的 2/1,200 是受攻击提示下的原任务成功，不是良性策略门通过率。摘要称该 harness 的攻击成功为 0/1,200。

Swipe horizontally to read the table

基准	模式	用例	阻断	良性侧
ASB 矩阵	确定性门	2,142	2,040/2,040	102/102
ASB 上游 DPI	规划器加门	1,200	1,200/1,200	2/1,200
InjecAgent	JSON 回放	2,108	2,108/2,108	2,108/2,108
BIPIA	响应汇回放	41,250	41,250/41,250	41,250/41,250
AgentHarm	工具目标回放	416	208/208	208/208
MCPTox	元数据流回放	485	485/485	485/485

• 作者解读：作者称所配置策略阻断了这些基准指定的、策略可见的攻击者流，包括工具注册、间接注入工具调用、响应汇、有害工具目标序列和被投毒的 MCP 元数据。

验证器、开销与对照

• 播种错误：12 个不安全策略变体全部被发现。5 个由过宽释放检查器做结构化发现，7 个由语义性质发现，覆盖过宽释放、缺失身份守卫、凭证逃逸或外泄序列、第三方共享、信任洗白、过授权和字段级泄漏。其中 6 个有可在绕过验证时重放的运行时见证。
• 验证时间：Table 5 的七项性质在 k=10、单核墙上时间下均为 UNSAT，每项 <0.5 秒：non_leakage_pii、no_credential_escape、no_privilege_escalation、no_sensitive_to_third_party、no_credential_exfil_sequence、no_trust_laundering、taint_monotonicity。
• 开销与 CaMeL：场景测试所用模式上，策略评估路径平均每次拦截 6.4 µs（P50 6.0、P95 8.7、P99 9.7）。作者称相对约 1–10 秒的 LLM 推理可忽略，并称核心决策在其测量中不是瓶颈。CaMeL 公开产物在同一 AgentDojo 配置上跑完 949 例，效用 60.1%；作者称这只是工件级效用比较，不是正面安全排名。论文未报告该次 CaMeL 的确认妥协。

其他消融与分析

• 已检入的最大 AgentDojo/AgentDyn 策略：28 条边、17 个节点、30 条流/路径/释放规则；k=10（§8.6）。
• 验证原型每次从零重建 SMT 编码；作者称这些完整重跑在所查性质上不到 0.5 秒（§6.2、§8.6）。
• AgentDyn 终止性拒绝的来源，作者点名为收件箱读取、网页抓取、资金转账、日历更改和图或文件变更等动态任务族缺作用域能力（§8.4）。
• Table 6 比较的是策略侧机制是否一等，作者称不是总体安全强度；AgentFlow 被标成独立声明式策略层、显式路径约束和有界 SMT 检查均为一等。
• 包装器、日志和扫描器成本随集成变化；论文未给出这些外围成本的数字（§8.7）。
• 字段级标签和可选扫描器没有单独的效用或漏报数字（§7.2）。

作者指出的局限与后续方向

• 过度污染：§8.9 称主要局限是消息密集型工作流中的过度污染。LLM 处理带污点的工具结果时，运行时可能保守传播污点，因为无法恢复精确的 token 级依赖。任务边界清晰时，按任务重置有帮助；混合可信与不可信内容的任务仍需要仔细的释放规则。
• 不推断意图：§8.9 称系统强制的是已配置策略，不推断应用所有者想放行哪些释放。有意把不可信网页转到外部汇、把私人记录与攻击者控制的指令组合，或与第三方共享敏感字段，都需要显式释放上下文，否则可能阻断良性任务。
• 动态任务的能力缺口：§8.9 称 AgentDyn 上初版 Dailylife 策略阻断了该次运行的全部确认妥协，但缺失的作用域能力解释了许多终止性拒绝。
• 验证范围：§8.9 称 SMT 给出的是验证器有界、结构化抽象上的先验保证，不是建模的工具与响应汇接口之外的任意 LLM 行为。
• 后续工作：§10 称当前结果是初步评测证据，并称这促使进一步做面向应用的开发与验证。

实验覆盖范围

• 基准规模：§8.1 的智能体运行包括 AgentDojo 949 例注入用例（四套件分别为 144、140、560、105）和 AgentDyn Dailylife 200 例。ASB 含 10 个场景、51 个良性任务、20 个正常工具、400 个攻击者工具，以及上游 DPI 1,200 例。
• 模型写法：§8.1 对 AgentDojo、AgentDyn 和分母对齐的 Progent 比较写的是固定 frontier LLM，未给出型号；ASB 上游 DPI 使用该工件的模型配置。每个套件一份策略，不按任务或攻击实例特化。
• 判定协议：§8.2 的效用和确认妥协来自四类轨迹分类和分类脚本。论文未报告该分类与人工判定的一致性，也未报告重复次数。
• 回放与对照：§8.5 除 ASB 上游 DPI 外是确定性策略门回放，良性侧不是最终回答效用。§8.2 的 Progent 正文数字限于 Slack 与 Banking；Travel 与 Workspace 为更小的补充负载，正文未给数字。§8.8 的 CaMeL 比较报告了 949 例效用，未报告确认妥协。
• 验证设置：§8.6 以 k=10 检查七项性质，并播种 12 个不安全策略变体。§8.7 的延迟测的是场景测试所用模式上的策略评估路径。

AgentFlow 是面向工具型 LLM 智能体的流中心策略语言和运行时监控器。它处理的问题是：机密或不可信数据可以沿一串各自合法的读取、变换、委托和外部写出流动，而只看单次主体–动作–资源的授权记不住这条链。

• 机制：数据带敏感度、类别和信任。边上的传播可以继承、变换、不透明近似或换成常量。流规则管单跳，默认拒绝且拒绝优先；路径规则在谱系或会话历史上要求清洗、限制委托或禁止指定的多步模式。引用监控器在工具执行前给出允许、拒绝或暂停。部署前，Z3 在长度至多 k 的符号化轨迹上检查结构化片段。论文给出运行时良构性与中介轨迹强制的定理，并写明若干目标依赖策略中已有相应规则。
• AgentDojo：未点名的固定 frontier LLM 上，949 例注入用例的确认妥协从 33.0% 到 0.0%，合计效用从 46.7% 到 63.3%（Table 2）。效用按注入用例上的良性任务完成计算。
• 其他运行：AgentDyn 200 例 Dailylife 上，确认妥协从 73.5% 到 0.0%，效用从 44.5% 到 43.5%。ASB 上游直接提示注入 harness 的攻击成功为 0/1,200；同一次原任务成功为 2/1,200。七项性质在 k=10 时均于 0.5 秒内为 UNSAT，12 个播种的不安全策略变体全部被发现。
• 作者结论：作者称在所配置策略下，运行时强制加有界检查阻断了所考察基准中的策略可见攻击，并保留了可用的任务完成。作者同时把结果限定在建模的中介接口和已评基准上，并指出过度污染、未写出的释放上下文，以及有界抽象之外的 LLM 行为，仍不在该保证内。