发表机构
Accentrust; Georgia Institute of Technology; University of Illinois Urbana-Champaign（Accentrust; 佐治亚理工学院; 伊利诺伊大学厄巴纳-香槟分校）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对长时程工具使用AI智能体中自生成子目标带来的授权缺口，提出一种基于版本绑定见证和原子提交边界的运行时授权机制，在有限结构化域中证明其安全性并验证有效性。
AI 中文摘要
长时程工具使用的AI智能体会创建子目标、重新规划、委派工作并组合兄弟结果。逐工具的权限检查无法确保不断变化的目标图仍保持在委托人批准的任务范围内。我们在一个有限结构化域中解决这一授权缺口，该域包含一个委托人和一个授权根。每个提议的目标图变更都携带一个版本绑定的见证，证明其延续轨迹、资源、义务、不变量和结束条件细化了活动根契约；每个受保护的效果都在原子提交边界处被重新检查。自由形式的目标文本不提供任何权限。我们在显式中介、抽象、新鲜性和原子性假设下证明了轨迹策略和建模的禁止状态保持，以及条件性根成功保持、针对无记忆允许列表的分离结果、精确有限域可判定性，以及在健全抽象细化下的通用安全性单调性。一个可执行模型探索了340个状态和419个转换。在涵盖25个结构模式的96个匹配案例中，完整机制在48个漂移案例中提交了零个禁止状态，并完成了所有48个良性对应案例。两个公共上游运行时路径在32个案例中执行了258次原生调度，每个案例级别的决策和收据链均匹配。一项冻结的主机本地研究覆盖了129个合成单因素逐一变化单元，所有单元均匹配固定决策和原因。一个具有历史感知的延续比较器阻止了所有建模的不良轨迹前缀，但在11个案例中提交了所有操作，这些案例的违规位于类型化资源、新鲜性或显式连接证据中，超出了其轨迹投影范围。在注册的结构化域内，运行时授权保留了有用的重新规划，同时防止自生成的子目标成为新权限的来源。
英文摘要
Long-horizon tool-using AI agents create subgoals, replan, delegate work, and compose sibling results. Per-tool permission checks cannot establish that a changing goal graph remains within the principal-approved task. We address this authorization gap in a finite structured domain with one principal and one authorization root. Each proposed goal-graph mutation carries a version-bound witness that its continuation traces, resources, obligations, invariants, and closing condition refine the active root contract; every protected effect is rechecked at an atomic commit boundary. Free-form goal text supplies no authority. We prove trace-policy and modeled forbidden-state preservation under explicit mediation, abstraction, freshness, and atomicity assumptions, plus conditional root-success preservation, a separation result for memoryless allowlists, exact finite-domain decidability, and universal-safety monotonicity under sound abstraction refinement. An executable model explores 340 states and 419 transitions. Across 96 matched cases covering 25 structural schemas, the complete mechanism commits zero forbidden states in 48 drifted cases and completes all 48 benign counterparts. Two public upstream runtime paths execute 258 native dispatches across 32 cases, with every case-level decision and receipt chain matching. A frozen host-local study covers 129 synthetic one-factor-at-a-time cells, all matching fixed decisions and reasons. A history-aware continuation comparator blocks every modeled bad trace prefix but commits all operations in 11 cases whose violations lie in typed resources, freshness, or explicit-join evidence outside its trace projection. Within the registered structured domains, runtime authorization preserves useful replanning while preventing self-generated subgoals from becoming a source of new authority.
Comments38 pages, 3 figures, 8 tables
