論文の概要: CaMeLoT: CaMeL orchestrated with Temporal logic for static verification and liveness

• arxiv url: http://arxiv.org/abs/2609.18674v1
• Date: Wed, 16 Sep 2026 13:52:16 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-20 08:55:53.827153
• Title: CaMeLoT: CaMeL orchestrated with Temporal logic for static verification and liveness
• Title（参考訳）: CaMeLoT: 静的検証と生存のための時間論理を用いたCaMeL
• Abstract要約: CaMeLoTは生成された計画を有限状態遷移系に変換する。 ツールコール、証明、テナント情報でラベル付けする。 CTLで表現された時間ポリシーに対してチェックする。
• 参考スコア（独自算出の注目度）: 1.2109519547057517
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.
• Abstract（参考訳）: LLMベースのエージェントは、プライベートデータへのアクセスやコマンドの実行が可能な外部ツールを呼び出すマルチステッププランを生成し、実行する。 この設定では、セキュリティは、単一のステップだけでなく、計画が生成する実行全体の特性である。 計画そのものは、ツールコール、制御フロー、データ依存をキャプチャする重要な成果物である。 ツール使用 LLM エージェントのプロンプト注入に対する既存の防御である CaMeL の補体 CaMeLoT について述べる。 CaMeLoTは、任意のツールが呼び出される前にエージェントの計画をチェックする静的な検証層を追加することで、CaMeLを拡張する。 CaMeLoTは生成されたプランを有限状態遷移システムに変換し、ツールコール、証明、テナント情報をラベル付けし、nuXmvモデルチェッカーを使用してCTLで表現された時間ポリシーに対してチェックする。 検証は実行前に行われるため、LLMコールやツールコールを使わずに、安全でない計画は拒否される。 検証が失敗した場合、モデルチェッカーは反例を返してエージェントにフィードバックを与え、プランを修復する。 我々は,AgentDojoベンチマーク,SOCワークフロー,即時抽出実験から得られたポリシーに基づいてCaMeLoTを評価し,CaMeLのランタイムチェック可能なカバレッジを保ちながら,実行前の時間特性の幅広いクラスを検証することを示した。

関連論文リスト

• Symbolic Temporal Supervision of LLM Agents Using Contracts [1.7188280334580195]
  本稿では,大規模言語モデル(LLM)エージェントのシンボリック時間監視のための契約ベースのフレームワークであるContrAgentを紹介する。 ContrAgentは、エージェントの振舞いを一連のツールコールとして捉え、それを固定されたチェック可能な述語セット上のトレースとしてフォーマル化する。 その後、有限トレース上の線形時間論理における仮定保証契約(sum-guarantee contract)を用いて必要な振る舞いを特定する。
  論文  参考訳（メタデータ） (2026-09-16T05:05:35Z)
• Fresh Memory, Stale Plans: Dependency-Scoped Validation for Distributed LLM-Agent Memory [29.800883966590007]
  PlanFenceは依存性スコープによるアクション検証プロトコルである。 一方、PlanFenceは無効なアクションなしですべてのタスクを完了します。
  論文  参考訳（メタデータ） (2026-09-03T03:56:15Z)
• ROPE: Routed Origin Policy Enforcement against Indirect Prompt Injection [61.4148196085256]
  本稿では,信頼という構造概念に根ざしたROPE(Routed Origin Policy Enforcement)について述べる。 提案手法では,(1)軌道の各段階において,攻撃可能コンテンツのみを起点とする値が,原点保護パラメータに到達しない,(2)注入のリワードがない,という2つの保証が認められている。
  論文  参考訳（メタデータ） (2026-08-27T01:22:14Z)
• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  大規模言語モデル(LLM)によって駆動されるエージェントシステムは、永続的な運用データを扱う現実世界にますます展開されている。 既存のアプローチはそのようなシステムレベルの保証を提供していません。 本稿では, 1 つの LLM とツールオーケストレーションハーネスからなるエージェントシステムのリレーショナル操作データに対する検証について述べる。
  論文  参考訳（メタデータ） (2026-08-04T13:01:30Z)
• Cordon: Semantic Transactions for Tool-Using LLM Agents [11.567293065381918]
  本稿では,コミット前にエージェント効果のステージングと検証を行うトランザクションランタイムシステムであるCordonを紹介する。 適度な承認とレイテンシのオーバーヘッドで、良質なタスク補完を保ちながら、不可逆的な効率の失敗を減らす。
  論文  参考訳（メタデータ） (2026-06-16T06:21:14Z)
• Agent libOS: A Library-OS-Inspired Runtime for Long-Running, Capability-Controlled LLM Agents [0.6345523830122165]
  大規模言語モデル(LLM)エージェントは、要求応答アシスタントから長期実行中のソフトウェアアクターへと進化している。 本稿では,LLMエージェントのためのライブラリOSをベースとしたランタイム基板であるAgens libOSを提案する。
  論文  参考訳（メタデータ） (2026-06-02T16:53:24Z)
• Securing LLM Agents Need Intent-to-Execution Integrity [49.490963596514185]
  我々は, LLMエージェントの確保には, エージェントの実行がユーザの意図を忠実に反映した場合に規定するエンドツーエンドの正当性を定義する必要があると主張している。 LLMエージェントはコンパイラと構造的に類似しており、セキュリティ違反はユーザ意図を保存しない誤った実行に対応する。 emphTool整合性、emph命令整合性、emphJudgment整合性、emphData整合性。
  論文  参考訳（メタデータ） (2026-05-16T12:53:31Z)
• Gecko: A Simulation Environment with Stateful Feedback for Refining Agent Tool Calls [56.407063247662336]
  本稿では,ルールとLLMを組み合わせてツール応答をシミュレートする総合環境であるGeckoを紹介する。 GATS は GPT-4o, GPT-5, Gemini-3.0-pro など様々な LLM のツールコール性能を一貫して改善している。
  論文  参考訳（メタデータ） (2026-02-22T15:02:00Z)
• Defeating Prompt Injections by Design [79.00910871948787]
  CaMeLは、Large Language Modelsを中心とした保護システムレイヤを作成する堅牢なディフェンスである。 CaMeLは、(信頼された)クエリから制御とデータフローを明示的に抽出する。 セキュリティをさらに改善するため、CaMeLは、権限のないデータフロー上のプライベートデータの流出を防止する機能の概念を使用している。
  論文  参考訳（メタデータ） (2025-03-24T15:54:10Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。