CaMeLoT：用 CTL 时序逻辑在执行前静态验证 Agent 计划

工具调用智能体的安全是整段执行的性质，而 CaMeL 的策略在单次工具调用时检查，既表达不了活性，也会把本可在规划阶段发现的违规留到运行时。

• 场景：作者称 LLM 智能体代用户规划并调用外部工具，可能接触私有数据、改持久状态或触发超出对话的后果。OWASP 把提示注入列为这类应用最主要的风险。若计划被提示注入、恶意指令或被污染的上下文操纵，智能体可能自主外传信息、滥用权限或造成破坏性变更。
• 现有方法的不足：CaMeL（Debenedetti et al., 2025）用 Willison (2023) 的双 LLM 架构约束控制流，用能力（capabilities）跟踪数据来源与读者，并在工具调用时用 Python 函数做允许或拒绝。作者称其策略模型是过程式且时间上局部的：解释器虽维护数据流图，却没有覆盖整段执行的全局规范语言，活性无法自然表达。运行时才检查还会执行失败点之前的 LLM 调用；规划阶段也不能利用违规去重规划。原 CaMeL 论文把缺乏形式性列为未来工作。
• 核心观察：计划本身是包含工具调用、控制流和数据依赖的关键产物。一部分性质必须在运行时检查，另一部分可以从计划的时序结构在规划阶段静态检查。
• 威胁模型：
  • 目标与受害系统：防御针对工具调用型 LLM 智能体中的提示注入；安全策略约束可观察动作，而不只依赖模型抵抗对抗指令。
  • 知识与信任：CaMeLoT 使用与 CaMeL 相同的威胁模型：输入提示词、用户提示词和系统提示词，以及一部分（并非全部）工具的输出是可信的。
  • 能力划分：P-LLM 根据可信用户查询生成受限 Python 计划；无工具的 Q-LLM 只把不可信内容抽成带能力标签的结构化值。到达 Q-LLM 的注入不能向 P-LLM 下指令，只能改变变量的值。
  • 检查位置：CaMeLoT 在任何外部工具调用之前静态拒绝违反时序性质的计划；依赖具体值或读者集合的检查仍留给 CaMeL 运行时。
• 提出的方法：作者提出 CaMeLoT，作为 CaMeL 的保守、互补扩展：把计划译成有限状态机，用 CTL 与 nuXmv 在规划阶段验证，失败时用反例驱动修复，并可从自然语言可选地抽出时序规范。

• CaMeL 与双 LLM、能力系统
  • CaMeL（Debenedetti et al., 2025）——把 Willison (2023) 的双 LLM 隔离与基于来源、读者的能力跟踪结合起来，在工具调用时执行 Python 策略。作者称原论文把缺乏形式性列为未来工作，本文针对这一缺口。
  • 信息流基础——Denning and Denning (1977)、Goguen and Meseguer (1982)、Abadi et al. (2009) 被用来说明能力与信息流；作者只把它们作为 CaMeL 所依据的传统概念，没有另作对比。
• 静态与动态结合、时序与运行时执行
  • Meijer (2026)——论证智能体工作流应结合静态与动态检查，并同样关注提示注入。作者称区别在于本文使用时序逻辑、带计划修复的模型检验、任务性质抽取，并建立在已有的 CaMeL 上。
  • TraceFix（Xia et al., 2026）——用 TLA+ 的 TLC 检验 LLM 合成的协议，按反例修复，再在运行时监视器下执行。作者称其关注互斥与无死锁，验证后的协议只被编译进提示词；CaMeLoT 验证的是随后会被执行的计划，对象是提示注入下的安全与任务性质。
  • 运行时或轨迹上的时序约束——TemporalGuard（Cohen et al., 2026）用过去时间时序逻辑约束到当前时刻为止的对话；Agent-C（Kamath et al., 2025）、AgentSpec（Wang et al., 2025）、MARIS（Cui et al., 2026）、Doshi et al. (2026)、VeriGuard（Miculicich et al., 2025）、Progent（Shi et al., 2025）在运行时约束工具使用或数据流。Ramani et al. (2025) 用 LLM 把计划变成 Kripke 结构与 LTL，再用 NuSMV 检验。Sentinel（Zhan et al., 2025）用时序逻辑分析已收集的具身智能体轨迹。作者称这些工作偏离本文之处是侧重运行时验证或事后轨迹，而不是执行前静态验证生成的计划。Hong et al. (2026) 被引为：相当一部分写清的策略可用符号机制执行，时序性质是关键一类。
• 信息流形式模型、隔离与模型级防御
  • LLMbda（Garby et al., 2026）、f-secure（Wu et al., 2024）、RTBAS（Zhong et al., 2025）给出信息流的形式模型，作者称它们不支持时序逻辑或正确性验证。DRIFT（Li et al., 2026）用动态权限隔离提示注入，作者称没有本文所包含的形式性。IsolateGPT（Wu et al., 2025）通过隔离工具环境减轻跨应用流动风险。
  • 护栏与指令层级——Inan et al. (2023)、Li et al. (2025) 在主模型前对输入或输出做安全分类。作者称这类防御仍是概率性的，不能给出确定性保证，且 LLM-as-a-judge 会受到优化攻击（Shi et al., 2024）。StruQ（Chen et al., 2025）与 SecAlign（Chen et al., 2024）通过微调让模型区分或忽略不可信区域中的指令。作者称 CaMeLoT 与这些模型级防御互补：它验证生成的计划，而不是依赖模型抵抗恶意指令。Greengard (2026b,a)、Cohen et al. (2026) 与 Amazon Bedrock 的推理护栏（Bayless et al., 2025）被用来对照“用逻辑保证输出正确”；作者称本文的做法是把时序逻辑用于智能体工作流中的用户需求。Dogwood 近期加入了时序策略，作者称其在推理护栏中的用法仍不清楚。
• 基线与基准：基线是 CaMeL 及其在实验 2 中只跟踪污点的简化命名空间；基准是 AgentDojo 的 Slack、Banking、Travel、Workspace（Debenedetti et al., 2024），即原 CaMeL 评测所用套件，另加作者构造的 SOC 工作流。作者称 SOC 示例的实际相关性来自该领域增多的智能体用法，并认为以后需要更专门的 SOC 策略基准。

作者把本文定位为：补上 CaMeL 的形式性缺口，在保留其运行时能力检查的同时，用 CTL 模型检验、反例修复和任务性质抽取做执行前验证。

CaMeLoT 在 P-LLM 生成计划之后、任何外部工具调用之前插入验证阶段。能从计划时序结构读出的要求写成 CTL，用 nuXmv 检验；依赖具体值或读者集合的要求仍由 CaMeL 在运行时处理。Figure 1 中蓝色为原 CaMeL，黄色为新增的任务性质抽取、安全性质、模型检验与反例修复。

问题设定与 CTL

• 两类性质：一是写成时序逻辑公式的安全策略；二是从用户提示词抽出并译成时序逻辑的任务性质。
• CTL：路径量词 A 表示所有路径，E 表示某条路径；本文用到的模态是 X（下一状态）、F（最终）、G（始终）、U（直到）。AG φ 表示每条路径的每个状态都有 φ；AF φ 表示每条路径最终有 φ；A[φ U ψ] 表示每条路径上 φ 一直成立直到 ψ。作者称文中例子用线性时序逻辑也够，但分支逻辑的推广无害。
• 策略形态：策略按领域筛选，只检查计划里出现的工具和动作所对应的子集。每条策略带受 Sigma 规则启发的轻量元数据（名称、状态、级别等）。Listing 1 的内部表示把公式、描述和级别放在一起。常见模式包括参数溯源、污点阻止、时序顺序和终止（例如 AF(done)）。
• 原子命题：公式在有限状态模型导出的原子命题上解释。工具到参数名的映射使 CTL 可以按稳定的参数名引用，而不随 P-LLM 的写法变化。

从计划到有限状态机

• 区域：自定义 AST 访问器抽出四类区域：TOOL CALL、ASSIGNMENT、条件 CONDITIONAL、循环 LOOP。这覆盖 CaMeL 解释器接受的 Python 子集；任意 while 和不受控的 break 被排除。表达式或参数内部的嵌套工具调用会先作为区域发出。抽取前有一次不改变行为的规范化。
• 模型：构造 M = (S, s0, Δ, Σ, L)。S 为状态，s0 为初态，Δ 为迁移，Σ 为状态变量更新，L 把状态标成原子命题集合。工具调用区域记录工具名、参数和目标变量；条件产生分支与汇合；循环用入口、体、出口，迭代是“继续或退出”的非确定选择。作者称这是对可能执行的过近似，状态空间有限，可能产生假阳性并拦下一些安全计划，但保留跨循环的潜在违规。
• 溯源格：prov 把变量映到 {trusted, user, untrusted, qllm}，全序为 trusted < user < untrusted < qllm。Q-LLM 输出为 qllm，外部工具输出为 untrusted，字面量为 trusted，用户查询参数为 user。派生值取依赖的最大溯源。若收件人来自 untrusted 或 qllm，则产生 recipient tainted。Figure 2 的例子把读频道、Q-LLM 抽信箱、发送私信连成 sINIT 到 sDONE，并在发送处同时标上调用与污点。
• 与 CaMeL 能力的对应：Readers 表示谁可以读，Sources 表示来源。作者称受邀者集合和描述的作者身份在规划时一般未知，静态 CTL 无法完全解析。CaMeLoT 把不可信、有条件可信或静态不可判定的值标为 tainted；公开与私有的区分故意留给 CaMeL，因为保密依赖执行时才有的读者能力。

模型检验与修复

• 编码：nuXmv 模型含有限程序计数器，以及工具调用指示、参数污点、溯源和“某动作是否已经发生”的历史谓词。顺序语句是确定迁移，条件每个分支一条迁移，循环为非确定的再迭代或退出。确认类工具可把 confirmation seen 置真并保持到后续状态。
• 选择与判定：引用的工具或命题出现在计划或相应领域配置中时，该 CTL 性质才被送入 nuXmv。全部成立则接受计划并交给 CaMeL 执行。失败时 nuXmv 返回反例轨迹；CaMeLoT 把它转成自然语言，包含被违反的性质、简化路径和一般修复说明，交给 P-LLM。验证重复直到接受或修复预算用尽。作者称这让人联想到 CEGAR（Clarke et al., 2003），但是把反例用作对该计划的自然语言细化。
• 实现边界：不改变 CaMeL 核心功能。工具签名用来把位置参数和关键字参数归一，使等价写法产生相同原子命题。作者计划以扩展 CaMeL 实现的方式提供 CaMeLoT；论文给出了仓库位置，此处不录网址。

从提示词抽出任务性质

• 流水线：Figure 3 为提示词到 LLM proposer、类型化义务、grounding、CTL 公式。LLM 不直接写 CTL。提议必须是 Table 7 中的一种形式，包括存在、全路径存在、先后、until、响应、可达、之后禁止、下一步禁止、副作用允许列表和原子条件。确定性的 grounding 检查工具是否有效，并拒绝畸形或未落地的义务。结果写入运行时任务登记，与安全策略走同一条 nuXmv 流水线。Section 5.3 给出 Banking 套件上的抽取示例。
• 与安全策略的分工：作者称提示词抽取捕捉任务是否完成，静态策略捕捉参数溯源，二者互补。例如“查到可疑交易之后，改密码必须仍可达”与“凡调用改密码则密码必须可信”不是同一条性质。

实验设置

• 三组实验：实验 1 测静态验证能复现多少 CaMeL 覆盖；实验 2 测超出 CaMeL 局部策略的性质；实验 3 测任务级性质能否从提示词抽出并验证。
• 模型：实验 1 与实验 2 的端到端部分、以及实验 3 的抽取与任务评测使用 Anthropic 的 claude-haiku-4-5-20251001。实验 3 的直接写 CTL 对照另用 GPT-4.1 nano、GPT-4.1 mini、Claude Haiku 4.5、Claude Sonnet 4.5。论文未把这些名字与具体版本号一一对应到每次调用的系统提示词全文。
• 基准：AgentDojo 的 Slack、Banking、Travel、Workspace，即原 CaMeL 评测所用套件；用户任务共 97 个（Banking 16、Slack 21、Travel 20、Workspace 40，Table 9）。另有一个简化 SOC 工作流、7 条 CTL（Table 4），以及 20 个受控案例（12 个来自 AgentDojo，每套件 3 个；8 个来自 SOC）。
• 基线：实验 1 为完整 CaMeL 策略。实验 2 为简化 CaMeL 命名空间：只跟踪污点，Q-LLM 输出标为 tainted，仅 block ip() 与 create incident ticket() 拒绝 tainted 输入。
• 指标：实验 1 把计划分为 pass（放行且行为符合意图）、fail（放行但不符合意图）、blocked（违反安全性质并被拒绝），并统计双方是否同意。覆盖分 Full、Partial、None，且把 Security 与 Confidentiality 分开（Table 1、Table 2）。实验 3 用 Exact、Faithful、F1、词汇表命中 Vocab.、grounding 存活 Surv.，以及 Clean tasks、合法输出、畸形和未落地计数。
• 协议：实验 1 在无提示注入下跑四个套件；CaMeLoT 关闭计划修复，仅当生成代码使用不支持的操作（如原地修改列表）时用一次修复提示替换该操作。实验 2 前半用固定安全计划及其手工不安全变体，以去掉语言模型生成的变异。实验 3 的 E3 同样用手工固定的正确计划与违规计划。论文未报告重复次数。

主结果

实验 1 的主对比是同一批 AgentDojo 任务上双方判定是否一致（Table 3）。

Swipe horizontally to read the table

套件	Both pass	Both fail	Both block	仅 CaMeLoT pass	仅 CaMeL pass
Slack	6	5	6	4	0
Banking	5	2	6	2	1
Travel	9	10	0	1	0
Workspace	22	5	5	2	6
Total	42	22	17	9	7

• 一致性：作者称双方大多在 pass 与 block 上一致，只在 75 次成功测试中的 16 次不同意。结论中作者称二者在 59/75 的情形上对“拦截还是放行”一致；42+17=59，对应 Both pass 与 Both block，16=9+7。
• 分歧来源：作者称分歧主要来自 CaMeL 按运行时性质拦截，例如资源的读者。双方都拦截时，CaMeLoT 在执行前拦截，从而避免不必要的工具调用并减少本会失败的计划的 token 用量。论文未报告具体 token 数或查询次数。
• 任务失败：97 个用户任务中有 22 个在两种方法下都 fail，因为生成的计划没有完成用户意图。作者认为更强的规划模型可能会改善这一点。

与 CaMeL 策略的静态重叠

• 覆盖：镜像 AgentDojo 上 CaMeL 策略时，有副作用函数的安全策略静态覆盖为 22/28；其余 6 条依赖无法仅从计划结构决定的运行时状态，留给 CaMeL。保密性质由读者定义，CaMeLoT 不直接处理，只在函数输出为公开时重叠。对无副作用函数的可信/不可信标记，覆盖为 24/46。
• Table 1（有副作用，Security 的 Full / Partial / None）：Slack 3/1/3，Banking 5/0/0，Travel 6/0/0，Workspace 8/0/2，合计 22/1/5。同表 Confidentiality 合计 Full 16、Partial 0、None 9。
• Table 2（输出污点标记）：Security 合计 Full 24、Partial 22、None 0；Confidentiality 合计 Full 23、Partial 0、None 23。各套件行见 Table 2，此处不逐格重复。

SOC 上超出 CaMeL 的性质

• 手工变体（Table 5）：7 条不安全计划全部被 CaMeLoT 拦住。简化 CaMeL 只拦住 S7（把来自 LLM 输出的 tainted IP 传给 block ip），S1–S6 均为未拦住。S1–S6 分别是隔离早于确认、强动作缺少事先人工批准、从未调用隔离、工单创建后未解决或升级、扫描附件后立即隔离、强动作发生在开工单之前。
• P-LLM 生成（Table 6）：四次测试使用同一模型。CaMeLoT 全部拦住，CaMeL 一次也没有拦住。规则对应为 S1 与 S2、S3、S4、S6。作者称这在预期之内，因为这些性质被故意设计成超出 CaMeL 的表达能力。
• 查询设置：每个测试有一条意图产生好计划的查询和一条意图偶然产生坏计划的查询，并附系统提示词。论文未报告这四次测试的好计划是否全部被放行。

提示词抽取

• E1（Table 9）：97 个任务都有已知正确解；标签只保留改变状态的步骤。Exact 为抽取的必需副作用集合与标签完全一致；Faithful 还计入正确的条件副作用。合计 Exact 85/97（87.6%），Faithful 88/97（90.7%），F1 0.86，Vocab. 与 Surv. 均为 100%。分套件 Exact：Banking 75.0%，Slack 85.7%，Travel 95.0%，Workspace 90.0%。
• E2（Table 10）：直接让模型写 CTL 时，Clean tasks 为 GPT-4.1 nano 12/97、GPT-4.1 mini 79/97、Claude Haiku 4.5 96/97、Claude Sonnet 4.5 94/97。Haiku 的合法输出为 493/494，畸形 0、未落地 1；Sonnet 为 551/554，畸形 2、未落地 1。类型化流水线配合 Haiku 为 97/97、182/182，畸形与未落地均为 0。作者称直接生成高度依赖模型，有的模型会发明看似合理但未落地的标识符，即使最好的一轮也至少有一条非法公式。
• E3（Table 11）：20 个受控案例中，抽出的公式拦住全部 20 个违规计划、验证全部 20 个正确计划，并与等价手写 CTL 全部一致。类别及 n 为：Existence 4、All-path liveness 1、Ordering/history 3、Enabled reachability 2、Until 1、Triggered response 1、Next-step prohibition 1、Absence after 1、Side-effect scope 4、Global taint/safety 2。

其他消融与分析

• 论文没有单独的参数消融表。与覆盖相关的分项已在 Table 1、Table 2。
• 实验 1 的例外是 9 次仅 CaMeLoT 放行、7 次仅 CaMeL 放行；Travel 的 Both block 为 0。
• 循环抽象可能假阳性并拦下安全计划；作者在讨论中把这写成过度污点与抽象粒度的权衡，未在 Table 3 中单列假阳性条数。
• 实验 2 的负面结果按作者的设计预期出现：简化 CaMeL 错过 S1–S6，端到端四次测试中 CaMeL 的拦截数为 0。
• E1 的低点在 Banking：Exact 与 Faithful 均为 75.0%，F1 为 0.79；作者未对此另作解释。
• E2 中 GPT-4.1 nano 的未落地标识符为 419、畸形 54，合法输出 182/655。

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

• 过度污点与拦截不足并存（Section 6）：有条件可信的函数输出被过度污点，可能过度拦截；值和读者能力未被建模，又可能拦截不足。作者把这写成执行前发现违规所省的 token，与误拦安全计划所浪费的 token 之间的权衡。论文未报告具体 token 数。
• 抽象粒度过粗（Section 6）：有限状态机只含污点，循环和条件的具体条件被省略，改为非确定选择。作者称这种抽象可能使更细模型能够验证的某些性质无法验证。
• 工具调用是黑盒（Section 6）：作者称可以用更模块化的方式利用调用的性质，例如 Hoare 式前后条件，并明确把这一点留作未来工作。
• 修复成本的边界（Section 6）：作者称无论运行时还是静态发现违规，修复成本本质上相同，因为两种情形都要生成计划。真正浪费只发生在假阳性，而且惩罚常常是一轮修复而不是一段部分执行。这是作者对成本的判断，不是测得的耗时。
• 运行时信息故意不在静态层解决（Section 6）：精确读者集合、动态计算的能力和工具特定的信任决定只在运行时可知，仍由 CaMeL 负责。因此 CaMeLoT 接受的计划仍可能在运行时被 CaMeL 拒绝。
• SOC 策略基准（Section 6）：作者称 SOC 示例说明了实际相关性，并建议未来需要开发更专门的 SOC 策略基准。Section 7 的后半在所给文本中被截断，截断之后是否还有局限，论文未在可见部分写明。

实验覆盖范围

• 被测规划模型在实验 1、实验 2 端到端和实验 3 的抽取评测中为 claude-haiku-4-5-20251001；直接生成 CTL 的对照为 Table 10 的四个模型。
• AgentDojo 实验覆盖 Slack、Banking、Travel、Workspace，共 97 个用户任务，且实验 1 为无提示注入；有副作用安全策略的静态 Full 覆盖为 Table 1 的 22/28，无副作用输出标记为 Table 2 的 24/46。
• SOC 部分包含 1 个工作流、Table 4 的 7 条 CTL、手工固定的安全计划及其不安全变体，以及 Table 6 的四次 P-LLM 生成测试。
• 任务抽取的 E3 为 20 个受控案例，正确计划与违规计划均手工固定；实验 1 除不支持的语法外关闭修复。论文未报告重复次数、token 用量或与人工判定的一致性。
• 动态能力、读者集合和工具特定信任仍按 Section 6 交给 CaMeL；作者写明工具的前后条件尚未纳入静态模型。

CaMeLoT 是 CaMeL 的神经符号扩展：在工具调用之前，用模型检验判断受限 Python 计划是否满足时序安全策略和从提示词抽出的任务性质。

• 问题：CaMeL 把策略写成工具调用时的 Python 判定，能挡住一部分被污染的数据流，但表达不了“工单最终必须关闭”或“隔离之前必须先批准”这类跨整段执行的约束，违规也要跑到该步才暴露。
• 做法：AST 抽出工具调用、赋值、分支和循环，循环按非确定迭代抽象成有限状态机，并用 trusted < user < untrusted < qllm 做保守污点传播。nuXmv 检验筛选后的 CTL。通过则进入 CaMeL 的运行时能力检查；失败则把反例交给 P-LLM，直到通过或修复预算用尽。任务侧由 LLM 提议 Table 7 的类型化义务，可信代码再落地并编译成 CTL。
• 重叠：无提示注入、claude-haiku-4-5-20251001、四个 AgentDojo 套件上，双方在 75 次成功测试中有 59 次对放行或拦截一致（Table 3；结论写 59/75）。22/97 的任务在两边都没有完成用户意图。有副作用安全策略的静态 Full 覆盖为 22/28（Table 1）。
• 时序性质：手工 SOC 变体中，CaMeLoT 拦住全部 7 条，简化 CaMeL 只拦住污点类 S7（Table 5）。P-LLM 生成的四次坏计划同样只被 CaMeLoT 拦住（Table 6）。
• 抽取：97 个任务上 Exact 为 87.6%、Faithful 为 90.7%，提议全部落在词汇表内并通过 grounding（Table 9）。类型化流水线的 Clean tasks 为 97/97，而直接写 CTL 的最好结果是 Claude Haiku 4.5 的 96/97（Table 10）。20 个受控案例中，抽出的公式与手写公式一致，并同时放行正确计划、拦住违规计划（Table 11）。

作者的结论是：执行前验证能覆盖 CaMeL 的很大一部分可静态化强制，并能表达局部按调用检查写不出来的顺序与活性；反例可以用于修复，任务级 CTL 则用来提高计划符合用户意图的机会。静态层故意不取代运行时的读者与能力检查。