Agent轨迹时序验证：审批缺口、来源绑定与离线/在线边界

Agent轨迹时序验证：审批缺口、来源绑定与离线/在线边界

知识点轴：sandbox-security / benchmark-evaluation / harness-runtime / context management；MCP Gateway与A2A仅为应用延伸，不是论文实测。 arXiv:2610.09793v1 于2026-10-07提交，本轮深读§3–7；原文可核查，Agent-Benchmarks与Harness-Engineering的机制证据见归档选段。本机未运行作者MonPoly、原始benchmark或Hermes生产实例。^[raw/articles/formal-runtime-verification-agent-trace-2610-09793v1-selected-2026-10-17.md]

为什么对用户重要

MCP-Gateway-Runtime的工具授权、Hermes无人cron审批和Context-Engineering的外部数据防注入，通常不能只看“调用了哪个工具”。同一个send_email或资金操作是否越权，取决于谁批准、批准哪一笔、接收方如何成为可信对象、发生在什么时候。论文的关键贡献不是一个漂亮的70%拦截数字，而是证明缺少历史事件/真实来源的benchmark会把“时序安全”错误压缩为粗糙动作类型判断。这为内部coding-agent及MCP/A2A网关评测提供应记录什么、如何否决假成功的工程清单，而非本站安全结论。

一阶机制：事件、关系、时间与可信来源

1. 先看历史可满足性。 MFOTL用带数据变量的过去时义务表达“对对象o执行破坏动作，须先有对象o的有效批准”。论文将AgentDojo、STAC、R-Judge轨迹转事件流，用未修改MonPoly离线重放；五类通用义务覆盖破坏/撤防/付款/导出/设备配置。但是AgentDojo 6899条运行无显式approval，STAC 483条仅6条有approval-like工具事件，三个攻击语料都无真实时间戳/结构化状态。前件根本无法发生时，形式逻辑判定实际退化为危险tool-name识别；不是时序关系发挥作用。相对地τ-bench 1980条任务轨迹中，作者在1039条修改动作之前找到许可语言，但它无攻击标签，不能借此报攻击拦截率。
2. 同一动作因对象历史而不同。 在银行转账/工作区外发，通用规则对成功攻击的检出/正常触发分别是银行79.2%/44.0%、工作区42.5%/15.2%；按过去“收款人/联系人”的关系约束后为70.0%/24.0%、39.2%/10.9%。更低误报伴随一定攻击漏检；并不是“更安全且无代价”。无上下文的规则不能区分合法外发与泄漏；有状态的传统规则也能编码这种条件，MFOTL优势是声明式可审计语义，而非独占时序能力。credleakbench-destination-verification-and-recovery提示还要独立核最终接收端与业务终态。
3. 历史来源本身可被污染。 把“看似目录字段”算可信收件人时，攻击者只添一行伪结构/引用文本，就让原先已标记的403银行、203工作区轨迹中的94%/99%不再报警。论文把事先发起的lookup(t)与相应result(t,p)绑定后，同一四种植入下翻转为0，且原测试集原有检出/benign firing不变。不是凡来自tool message就可信；还需可信工具身份、不可由攻击者伪造的call id/response关联、session及结果来源。论文仅证明既定植入族，工具遭入侵或攻击者能伪造匹配lookup时仍可能失效。这里与context-privilege-escalation-role-scope-reload-verification的“role不能代替来源/持久范围”是一条链。
4. 12字段仅是必要条件，非自动授权。 作者建议事件记录timestamp, actor, tool, action, object, recipient, source, approval_id, session_id, state_before, state_after, trust_domain。审批需有用户可回答提案的交互轮次、对象/金额绑定、失效时间和可核验主体；单轮无人cron即便有approval_id字段也不能凭空生出当次同意。A2A里还须在委托前后核调用者/task owner与转发凭据归属，不能凭公开Card或trace字段授予权限；本文未做A2A跨主体实验。

数字与证据等级不能错位

论文关键词规范化在54个手工工具名上precision 0.90/recall 0.84；早期ack子串等误判被修正，说明工具→动作类型映射本身也是判分器，需固定版本、盲标gold及反例；形式正确不补输入脏数据。与harnesssecurity-bench-paired-utility-attack-effects的同任务合法效用+违规effect配对结合，先做离线历史轨迹复算，再做受控in-loop干预及改路/恢复复验。

可执行小样本验收（提议，未执行）

• 合成任务：Hermes请求对一个虚构收件人发canary；tool返回中放伪目录行。旁路试验分别设置真实directory lookup结果、被引述/伪格式联系人、被攻陷directory以及同名不同caller。事件由执行器在调用/返回边界签入，记录时间、caller、session、call_id、对象/接收端和可验证审批，而不是让模型生成自己的审计日志。
• 在冻结的合法/攻击双轨迹上先比动作类型规则、按对象审批、lookup-response绑定，分别记检出、benign firing、schema字段实填覆盖与ground-truth副作用；缺事件单独记unevaluable，不当安全通过。进而在隔离环境接入拦截门，允许被拒后继续任务，测合法完成、绕行操作和真实外发零effect；审批超时/跨会话复用、代理最终目标、工具身份篡改必须有负例。
• 不自动把论文的形式规则加到生产Hermes/MCP网关；未知有效caller和无用户交互的cron应保持现有权限，而不是从历史trace推断新的授权。AI-Knowledge-Point-Radar的A2A真实Card/owner/push仍单独高优先处理。

失败模式与开放问题

这是作者的离线重放，不是部署安全改善。泛化规则的正常触发29.3%意味着未配置人审/正确恢复时合法任务可能严重受损；论文后验轨迹无法观察block后agent适应/替代路径/真实业务结果。受限于原始语料缺审批时间、关系字段和真实后态；可信工具被接管、response重放/并发乱序、跨tenant trace join与时间源漂移还需工程验证。日志本身也可能泄漏收款人与用户身份，需最小化/脱敏和审计留存策略。论文未找到可直接复现实验结果的作者代码仓库；数字均标作者报告、非本轮独立重跑。

写入记录

• 2026-10-17 09:03 CST：深读论文§3–7，归档选段；提炼审批交互可达性、结构化关系的可信来源绑定、离线触发与在线阻断分账，并给Hermes隔离小样本验收合同。