CaMeLoT: CaMeL orchestrated with Temporal logic for static verification and liveness
Researchers present CaMeLoT, extending CaMeL with CTL model checking that statically rejects unsafe LLM agent plans before any tool executes.
CaMeLoT adds a static verification layer to CaMeL, a runtime defense against prompt injection in tool-using LLM agents. It translates a generated plan into a finite-state transition system, labels it with tool calls, provenance, and taint information, and checks it against CTL temporal policies using the nuXmv model checker before any tool is invoked. Failed checks return counterexamples for plan repair, avoiding LLM calls, tool calls, and sandbox teardown. Evaluation covers policies derived from AgentDojo, SOC workflows, and prompt-extraction experiments.
- Static verification checks LLM agent plans before tool invocation
- Translates plans to finite-state systems verified against CTL policies
- Uses nuXmv model checker; counterexamples guide plan repair
- Evaluated on AgentDojo policies, SOC workflows, and prompt-extraction tests
Full article212 words · extracted from arxiv.org · click to collapse
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.
Text extracted automatically; images, tables and formatting may be missing. Original: https://arxiv.org/abs/2609.18674