CaMeLoT：CaMeL 与时态逻辑编排，用于静态验证和活性
CaMeLoT: CaMeL orchestrated with Temporal logic for static verification and liveness
浏览论文内容
中文总结 AI 辅助
CaMeLoT 通过将 LLM 智能体的计划转换为有限状态系统并用 CTL 时态策略进行静态验证，在工具调用前拦截不安全计划，节省资源并提供反例反馈，扩展了 CaMeL 的防御能力。
中文摘要 AI 辅助
基于 LLM 的智能体会生成并执行多步骤计划，这些计划会调用可访问私有数据或执行命令的外部工具。在此场景下，安全性是整个计划执行过程的属性，而不仅仅是任何单个步骤的属性。计划本身是关键工件，它捕获了工具调用、控制流和数据依赖关系。我们提出了 CaMeLoT，它是 CaMeL 的补充，CaMeL 是一种针对使用工具的 LLM 智能体中提示注入的现有防御机制。CaMeLoT 通过增加一个静态验证层来扩展 CaMeL，该层在任何工具被调用之前检查智能体的计划。CaMeLoT 将生成的计划转换为有限状态转换系统，用工具调用、来源和污点信息对其进行标记，并使用 nuXmv 模型检查器根据以 CTL 表示的时态策略对其进行检查。由于验证发生在执行之前，不安全的计划会被拒绝，而无需使用 LLM 调用或工具调用，从而节省了运行时可能花费的令牌，以及回滚更改或拆除临时沙箱的需求。当验证失败时，模型检查器会返回一个反例，以向智能体提供反馈来修复计划。我们在源自 AgentDojo 基准、SOC 工作流和提示提取实验的策略上评估了 CaMeLoT，结果表明它在执行前验证了广泛的时态属性类别，同时保留了 CaMeL 的运行时可检查覆盖范围。
英文摘要
LLM-based agents generate and execute multi-step plans that invoke external tools which can access private data or execute commands. In this setting, security is a property of the entire execution that a plan creates, not just any single step. The plan itself is a critical artefact that captures the tool calls, control flow, and data dependencies. We present CaMeLoT, a complement to CaMeL, an existing defence against prompt injection in tool-using LLM agents. CaMeLoT extends CaMeL by adding a static verification layer that checks an agent's plan before any tool is invoked. CaMeLoT translates a generated plan into a finite-state transition system, labels it with tool calls, provenance and taint information, and checks it against temporal policies expressed in CTL using the nuXmv model checker. Because verification happens before execution, unsafe plans are rejected without using LLM calls or tool calls, saving tokens that runtime could have cost, as well as the need to unwind changes or teardown temporary sandboxes. When a verification fails, the model checker returns a counterexample to give feedback to the agent to repair the plan. We evaluate CaMeLoT on policies derived from the AgentDojo benchmark, SOC workflows, and prompt-extraction experiments, showing that it verifies a broad class of temporal properties before execution while preserving CaMeL's runtime-checkable coverage.
发表机构
- University of Edinburgh（爱丁堡大学）
- Norwegian Defence Research Establishment（挪威国防研究所）
- University of Oslo（奥斯陆大学）
机构由 AI 辅助整理，请以论文原文为准。
