AIエージェントのツール実行計画を事前に形式検証する
CaMeLoT: CaMeL orchestrated with Temporal logic for static verification and liveness
この論文をやさしく読む
ひとことで言うと
AIが考えたツール操作の順序とデータの流れを、実行する前に数理的なルールと照合し、問題がある計画を止める仕組みです。
何に役立つ？
機密情報を扱うエージェントで、途中の手順だけでは分からない処理順序や情報の流れの制約を、事前に検査する用途があります。
この研究の面白いところ
単に計画を拒否するだけでなく、違反につながる実行経路を反例として返し、修正に使えるようにしています。
どこまで分かった？
検証対象は、計画から構成した有限状態モデルとCTLで表したポリシーです。要旨はすべての攻撃やモデル外の挙動への安全を保証せず、既存の実行時検査を補完する方式として説明しています。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
LLMを用いるエージェントは、機密データへのアクセスやコマンド実行が可能な外部ツールを呼び出す、多段階の計画を生成して実行する。この状況では、安全性は単独の手順だけでなく、計画が生む実行全体の性質である。計画そのものが、ツール呼び出し、制御フロー、データ依存関係を捉える重要な成果物となる。 本研究では、ツールを使うLLMエージェントへのプロンプトインジェクション対策である既存のCaMeLを補完するCaMeLoTを提案する。CaMeLoTは、どのツールも呼び出す前にエージェントの計画を確認する静的検証層をCaMeLへ追加する。生成された計画を有限状態遷移系へ変換し、ツール呼び出し、由来、汚染情報でラベル付けして、nuXmvモデル検査器によりCTLで表した時間的ポリシーと照合する。 検証が実行前に行われるため、安全でない計画はLLMやツールを呼び出さずに拒否される。これにより実行時に消費し得たトークンを節約するとともに、変更の巻き戻しや一時サンドボックスの後片付けも不要になる。検証に失敗すると、モデル検査器が反例を返し、計画を修正するためのフィードバックをエージェントへ与える。 AgentDojoベンチマーク、セキュリティオペレーションセンター（SOC）のワークフロー、プロンプト抽出実験から導いたポリシーでCaMeLoTを評価する。CaMeLが実行時に確認できる範囲を維持しつつ、幅広い時間的性質を実行前に検証できることを示す。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-16（UTC）
- 最新改訂
- 2026-09-16 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-16 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
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.
著者のコメント
Accepted at CAMLIS 2026 (Conference on Applied Machine Learning in Information Security)
arXiv ID: 2609.18674 ／ 要約の誤りについて