用时序逻辑监控工具 Agent：MonPoly 标出 71.8% STAC 攻击链，但溯源检查被一行注入骗过 94%–99%

核心问题在于：现有面向工具调用智能体的护栏多为无状态或单次调用规则，难以声明式表达与审计跨步骤、依赖数据和时间的历史安全策略，且主流安全基准未能记录充足的执行与确认历史。

• 场景与重要性：大语言模型智能体已接入邮件、转账、文档修改与实体设备控制；在间接提示注入威胁下，攻击者可通过不可信文本诱导智能体执行一系列单独看似正常但组合起来有害的工具调用链。
• 现有防御不足：现有护栏（如 AgentSpec、Progent、GuardAgent 及启发式过滤器）大多属于无状态或基于单次调用的规则检查；对于多步数据依赖，只能通过命令式代码硬编码局部有限状态，缺乏通用、可审计且可复用的声明式时序语义。
• 核心观察与假设：运行时验证（Runtime Verification, RV）中的一阶度量时序逻辑（MFOTL）天然适合刻画包含数据量化与时间窗口的历史约束；然而在缺乏审批、时间戳的现有攻击基准上，时序规约会退化为危险动作类型检测，只有引入数据参数化溯源与完整轨迹上下文才能发挥鉴别力。
• 论文提出的方案：作者提出了基于 MFOTL 与标准监控器 MonPoly 的离线运行时验证评估方法，并在 AgentDojo、STAC 与 R-Judge 轨迹上评估了 5 条通用规约与参数化规约；针对轨迹自身可能被投毒的缺陷提出了查找绑定强化溯源机制，并给出了包含 12 个字段的执行就绪轨迹模式。
• 威胁模型：
  • 攻击者目标：通过不可信输入操控智能体，触发未授权转账、数据外发、恶意配置变更或破坏性删除等违背系统安全策略的动作链。
  • 攻击者知识与能力：处于黑盒或提示注入设定，能向环境注入不可信文本（如邮件、网页正文或伪造的工具返回值格式内容），试图诱导模型或伪造结构化条目污染监控器历史；但无法直接篡改智能体未发起的调用，也无法控制被查询的真实工具本身。
  • 受害系统：由大语言模型驱动并配备可调用外部 API 的智能体系统，其内部推理不可见，外部可观测行为体现为交互消息与工具调用日志。
  • 安全监控假定：监控器部署在工具执行层，仅读取输入输出轨迹中的结构化事件流；评估设定为事后离线重放检测。

作者将相关研究及本工作在维度上的定位归纳为以下几类：

基于规则与提示词的智能体护栏

• AgentSpec（Wang 等，2026）：提供可定制的运行时强制规范语言，具备形式化规则语义，作者指出其主要针对当前调用，对跨步骤历史依赖多依赖定制编码。
• Progent（Shi 等，2025）：提出基于特权控制的智能体保护，在单调用粒度评估权限断言。
• GuardAgent（Xiang 等，2024）与 Llama Guard（Inan 等，2023）：分别基于知识库推理或内容分类模型对当前调用与消息内容进行安全分类，缺乏对轨迹数据量化的时序推理机制。

带轨迹记录的智能体安全评测基准

• AgentDojo（Debenedetti 等，2024）：提供包含银行、工作区等套件的动态注入攻击环境，开源了包含攻击成功与效用标签的完整工具调用运行记录。
• STAC（Li 等，2025）：从 SHADE-Arena（Kutasov 等，2025）和 Agent-SafetyBench（Zhang 等，2024）衍生出 483 条多轮攻击链，通过隐藏最终有害步测试多步攻击。
• R-Judge（Yuan 等，2024）：提供涵盖物联网、手机等多领域的安全风险认知基准，包含真实的良性与不安全行为轨迹。
• 𝜏-bench（Yao 等，2025）：真实人机交互任务基准，其领域策略强制要求智能体在状态变更前取得用户确认，提供了多轮交互与高密度确认轨迹。

一阶与度量时序逻辑运行时验证

• MonPoly（Basin 等，2011）及其形式化验证内核 VeriMon（Basin 等，2022）：支持安全范围一阶度量时序逻辑（MFOTL）的数据流监控，具备严格的形式化语义。
• DejaVu（Havelund 等，2018）：基于 BDD 的一阶过去式时序逻辑监控器，用于对无度量时间属性进行交叉比对。
• Maris（Cui 等，2025）：在智能体内部运行时中调用 MonPoly 强制隐私策略，但在 3 个自行构建的应用（各 20 条合成查询）上评估；作者指出其未在社区公开的真实攻击轨迹语料上进行评估。

基线方法与对比基准

• 评测对比对象：AgentDojo 自带防护（工具过滤器、提示词聚焦等）、AgentSpec、Progent、GuardAgent 以及基于关键词的动作类型检测规则；评测基准涵盖 AgentDojo、STAC、R-Judge 及控制基准 𝜏-bench。

作者定位的区别 作者指出，现有系统要么是面向单调用的局部规则，要么是在合成小规模场景中嵌入逻辑；本文则是首次利用未修改的通用 RV 监控器，在社区现有的完整离线攻击轨迹语料上对声明式、参数化与度量时序规约进行一致基准评测。

作者提出将工具调用轨迹规范化为带类型的一阶事件流，并采用度量一阶时序逻辑（MFOTL）表达可复用的安全义务，利用现成的 MonPoly 监控器在离线重放下进行判定。

核心义务定义与形式化

作者定义了五类通用安全义务，核心语义统一为“发生特定类别的危险动作前，必须在轨迹历史中存在对应的许可/确认前置条件”：

• O1 破坏性操作：包括删除、清空、注销等；
• O2 防护降级：包括禁用防护、解锁、添加自动删除规则等；
• O3 财务提交：包括转账、支付、结算等；
• O4 外部导出：包括发送邮件、共享、公开发布等；
• O5 设备控制与配置：包括设置参数、终端执行、开关物理设备等。

形式化上，以破坏性动作为例，其违规监控形式定义为动作发生且过去从未被批准： destructive(a) \land \neg \blacklozenge approved(a) 其中 \blacklozenge 表示在过去某一时刻成立。

轨迹规范化与事件提取流程

1. 工具动作类型映射：根据预设的动词子字符串列表，将轨迹中助手的工具调用名称分类为对应的危险动作类型；带有只读前缀（如 get_、list_、read_、search_ 等）的调用明确排除，不作为动作或许可。
2. 前置条件与参数解析：解析用户输入与工具调用参数；将确认类动词（如 confirm、approve 等）识别为许可事件。
3. 事件流转换：对 AgentDojo 提取 {function, args} 序列；对 STAC 拼接历史调用与隐匿的最终步骤；每个包含谓词的时间点转化为 MonPoly 日志格式 @t predicate(...)，无动作的时间点予以剔除。

参数化关联规约设计

由于通用规约在无审批基准上会退化为动作检测，作者设计了结合轨迹数据上下文的一阶参数化规约：

• 收款人溯源规约（银行套件）：限制转账动作的收款人 p 必须曾作为结构化收发方出现在先前账户数据中：

\Box \forall p. (transfer(p) \land \neg \blacklozenge known\_payee(p))

• 联系人溯源规约（工作区套件）：限制外发邮件的收件人 r 必须曾出现在系统通讯录或目录查询的结构化响应键值中。

历史投毒防御与强化溯源机制

针对攻击者可通过注入文本伪造结构化目录条目的风险，作者提出了查找绑定（lookup-bound）强化溯源机制：

• 规定数据只有来自智能体实际发起的查询调用（lookup）所对应的紧邻返回结果（result）时，才被判定为可信来源；直接出现在未发起的伪造工具消息或普通文本中的字段不予采信。
• 该机制以严格的时序因果绑定切断了攻击者通过单行伪造注入污染监控器历史的路径。

实验设置

• 被测模型：主实验评估 GPT-4o（gpt-4o-2024-05-13）；跨模型实验覆盖 AgentDojo 附带的全部 22 个无防御基础模型目录（涵盖 28 个含银行套件目录与 29 个含工作区套件目录）；𝜏-bench 上测试了 GPT-4o 与 Sonnet-3.5。
• 数据集与规模：AgentDojo 离线运行记录 6,680 次受攻击运行（排除 96 次空轨迹后）与 123 次良性运行；STAC 包含 483 条攻击链（来自 SHADE-Arena 与 Agent-SafetyBench）；R-Judge 包含 571 条记录（301 条不安全，270 条安全，含 30 条 IoT 子集）；控制基准 𝜏-bench 包含 1,980 条记录；合成日志 AgentTrace-T 包含 1,400 条轨迹。
• 指标定义：成功攻击检出率（Detection，在 security=true 运行上触发的比例）、良性触发率（BFR，良性运行上触发的比例，作为实用性代价代理指标）、阳性似然比（LR⁺ = Detection / BFR）、投毒翻转率（Poison Flip Rate）。区间均报告 95% Wilson 得分区间。
• 评测方式：基于离线日志运行未修改的 MonPoly 监控器，并使用 DejaVu 与 Isabelle/HOL 形式化验证内核 VeriMon 进行交叉校验（均得出完全相同的 347 次触发判定）。

主结果

下表呈现 GPT-4o（无防御）在 AgentDojo 各任务套件与通用规约下的主评测结果（据 Table 1、Table 9、Table 10）：

表格较宽，可左右滑动

评估对象 / 规约	ASR / 样本基数	成功攻击检出率 (%)	良性触发率 BFR (%)	唯一检出数	LR+
全体受攻击运行（通用并集）	1931/6680 (28.9%)	70.1	29.3	1354	2.40
O1 破坏性操作	1931 成功攻击	15.9	4.1	259	3.91
O2 防护降级	1931 成功攻击	0.0	0.0	0	-
O3 财务提交	1931 成功攻击	26.8	13.0	243	2.06
O4 外部导出	1931 成功攻击	27.9	10.6	491	2.64
O5 设备控制与配置	1931 成功攻击	16.2	6.5	38	2.49
银行套件（banking 并集）	ASR: 40.1%	97.4	79.2	未报告	1.23
工作区套件（workspace 并集）	ASR: 19.9%	62.9	21.7	未报告	2.90

• 作者指出，通用规约在 AgentDojo 上覆盖了 70.1% 的成功攻击，但良性触发率达 29.3%，在银行套件上良性触发率更高达 79.2%，说明通用层更适合作为人工会审的分流器而非自动拦截门控。
• 作者指出，由于基准缺乏审批事件，通用规约本质上退化为动作类型检测；检出贡献分布在多条规约中，其中导出规约贡献了最多的唯一检出（491次），而破坏性操作规约的区分度最高（LR⁺=3.91）。
• 在 STAC 基准上，通用规约在 483 条链中检出 347 条隐匿最终步（71.8%，95% CI [67.7, 75.7]），四款独立监控器判定完全一致。

预警提前量分析（Earliest Warning）

• 测了什么：统计监控器触发时间点相对于最终有害调用的位置。
• 结果：在 1931 次成功的 GPT-4o AgentDojo 攻击中，52.4%（1012次）在最终有害动作前实现预防性预警，17.7%（342次）在最终有害动作发生瞬间触发，29.9%（577次）从未触发；预防性预警的中位提前量为 1 次工具调用（均值 2.19，最大 13）。在 STAC 上，11.8% 为预防性，61.5% 为发生瞬间触发，26.7% 未触发。
• 作者解读：预警提前量表明该方法具备在危害发生前实施干预的时机窗口，而非仅作为事后残差。

参数化规约与溯源投毒防御实验

• 测了什么：在银行与工作区评估参数化规约对误报的削减，并测试攻击者注入伪造目录行对监控器的欺骗及强化防范效果。
• 结果：在银行任务中，参数化收款人规约将 BFR 从 44.0% 降至 24.0%，检出率仅从 79.2% 变为 70.0%（LR⁺ 从 1.80 升至 2.92）；在工作区中，BFR 从 15.2% 降至 10.9%，检出率从 42.5% 变为 39.2%（LR⁺ 从 2.79 升至 3.61）。两项削减在 McNemar 检验下均具备统计显著性（银行 p=5.3× 10⁻²³，工作区 p=1.5× 10⁻¹¹）。
• 投毒与强化：在朴素溯源下，单行结构化或引用转发投毒导致银行 94.0%（379/403）和工作区 99.0%（201/203）的违规标记被翻转为合规；采用调用-响应绑定的强化溯源后，两者的翻转率均降为 0.0%（Table 3），且检出率与良性触发率均无任何变化。

基准就绪度与确认事件审查（Census）

• 测了什么：对 AgentDojo、STAC、R-Judge 及 𝜏-bench 统计审批、收发人、对象、时间戳等字段的可用性。
• 结果：AgentDojo 包含显式审批的比例为 0%（0/6899），STAC 为 1.2%（6/483），R-Judge 为 0.4%（2/571）；三者均不包含真实时间戳与结构化状态（Table 4）。在多轮交互的 𝜏-bench 上，状态变更前包含显式用户确认的轨迹比例达 52.5%（1039/1980）（Table 5）。
• 作者解读：作者认为审批缺失并非智能体轨迹的固有属性，而是攻击基准单轮交互协议导致的工具链设计缺漏。

其他消融与分析

• 工具映射敏感性：保守映射下 AgentDojo 检出率为 69.0%、BFR 为 26.0%；扩展映射下检出率为 79.9%、BFR 为 43.9%（Table 12）。
• 54 个手工标注工具的关键词分类准确率：微平均精确率 0.90，召回率 0.84，F1 值为 0.87，主类别完全匹配率为 87.0%（Table 11）。
• 轨迹字段消融：仅动作（R0）LR⁺ 为 1.80；加入接收者身份（R1）LR⁺ 升至 2.92；加入防投毒溯源（R2）保持该数值但在攻击下翻转率从 94% 降为 0%（Table 6）。
• 运行吞吐率与内存：MonPoly 在 1× STAC 日志上的吞吐率为 52k–179k 事件/秒，50× 复制下达 429k 事件/秒，内存峰值常驻保持在 8–14 MB（Table 13）。
• 跨模型参数化效果一致性：在 22 个模型目录下，参数化收款人规约在 20 个目录下降低了良性触发率，2 个保持不变，0 个增加，双侧符号检验 p=1.9× 10⁻⁶。

负面结果与例外

• 在 R-Judge 上通用规约对不安全记录的检出率仅为 23.6%（71/301），安全记录误报率为 16.3%（44/270）；作者解释称这是由于 R-Judge 绝大多数案例属于纯文本语义风险（隐私泄露、错误建议），缺乏结构化轨迹特征。
• STAC 中约 29% 的失败案例属于文本语义模式，且有 136 条链终止于五类通用规约之外的动作（如日历修改、编辑垃圾邮件规则等），监控器未能覆盖。
• 旅行套件（travel）在通用规约下检出率仅 16.5%，良性触发率为 11.1%，作者指出其原因在于该套件极少涉及金钱转账或数据外发动作。

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

• 评估基于离线重放而非在环拦截：实验衡量的是规约在离线记录轨迹上的触发率，未测试在环防御屏障拦截后智能体的自适应与重规划行为（Section 1 Scope、Section 7 Limitations）。
• 良性触发率仅为效用代价的代理：良性触发率仅统计了被规约标记的良性运行比例，由于被阻断的任务未重新执行，未能直接测量实际的任务失败率（Section 4、Section 7 Limitations）。
• 粗粒度关键词映射与纯文本语义盲区：工具分类采用子字符串匹配较为粗糙；STAC 中约 29% 的用例及 R-Judge 的多数用例仅体现在有害文本内容上，纯结构化时序验证无法对此类语义风险作出判定（Section 7 Limitations）。
• 参数化与跨模型覆盖范围受限：参数化规约精细化仅在银行和工作区两个套件上评估；跨模型分析仅覆盖了 AgentDojo 附带的模型（Section 7 Limitations）。
• 度量时序算子未在真实攻击语料中验证：由于现有攻击基准不包含时间戳，度量时序逻辑的滑动窗口与速率限制仅在人工构造的 CPS/IoT 日志上进行表达性验证，未反映真实攻击中的实际违规频率（Section 6.2、Section 7 Limitations）。
• 强化溯源仅验证特定攻击族：查找绑定的强化溯源规约仅针对测试的伪造返回值注入攻击有效，若攻击者能够伪造匹配的查询调用或直接破坏被查询的工具本身，则超出该机制防护范围（Section 5.2、Section 7 Limitations）。

实验覆盖范围

• 被测模型范围：主实验重点分析 GPT-4o（gpt-4o-2024-05-13），跨模型分析覆盖 AgentDojo 附带的 22 个无防御模型目录，控制基准包含 Sonnet-3.5，共计涉及这 23 款模型目录。
• 基准与任务套件：实验覆盖 AgentDojo（banking、slack、travel、workspace 4 个套件）、STAC（483 条链）、R-Judge（571 条记录，含 30 条 IoT 记录）及 𝜏-bench（airline 与 retail 领域共 1,980 条记录）。
• 规约覆盖范围：正式定义并评估了 5 条通用一阶时序规约（O1–O5）、2 条针对特定套件的参数化数据溯源规约，以及 3 条用于度量时间测试的人工规则。
• 实验未报告的维度：论文未报告在环拦截下模型的任务重试成功率、执行延迟开销，亦未报告大语言模型评判员与人工标注的一致性统计。

这篇论文对工具调用大语言模型智能体的安全监控进行了形式化时序验证研究。

• 核心定位与问题：针对现有智能体护栏多为无状态单调用规则、无法声明式表达跨步骤数据依赖安全策略，且主流安全基准缺乏时间与审批记录的问题，评估了一阶度量时序逻辑（MFOTL）在离线重放下的监控效能。
• 核心方法：提出离线运行时验证评估框架，将轨迹映射为类型化事件流，由未修改的 MonPoly 监控器判定 5 类通用操作规约；针对误报设计了基于历史数据的参数化溯源规约，并提出查找绑定机制抵御针对监控器历史的投毒攻击。
• 关键定量结果：
  1. 在 AgentDojo（GPT-4o，无防御）上，通用规约检出 70.1% 的成功攻击，良性触发率为 29.3%（Table 1）；在 STAC 上检出 71.8% 的隐匿有害步骤（Section 4.1）。
  2. 在成功攻击中，52.4% 的检测早于最终有害调用触发，提供干预时机（Section 4.1）。
  3. 参数化溯源将银行套件良性触发率从 44.0% 降至 24.0%（p=5.3× 10⁻²³），工作区从 15.2% 降至 10.9%（p=1.5× 10⁻¹¹）（Table 2）。
  4. 面对注入投毒，朴素溯源产生 94%–99% 的规约翻转，而强化溯源完全消除翻转至 0.0% 且不牺牲检出（Table 3）。
  5. 现存攻击基准审批字段极度稀缺（AgentDojo 为 0%，STAC 仅 0.6% 在有害步前），但多轮交互基准 𝜏-bench 显式确认率达 52.5%（Table 5）。
• 结论与启示：作者认为形式化时序监控的价值取决于轨迹是否承载可信历史；当前攻击基准因交互协议缺陷导致规约退化为动作检测，未来基准需采用支持用户确认的多轮交互协议并记录包含时间戳与溯源的十二字段规范。