局部放行、全局拒绝：逐动作授权为何在 LLM Agent 中无法组合

逐动作授权不能组合成全局授权。

• 场景：单个LLM智能体在有界回合里调用工具，局部谓词逐次放行。作者认为用户授权的是整段回合，而不是一串分别获批的步骤。
• 不足：作者称护栏是单迹执行监控。从不误报的逐动作监控检不出关系型目的违规，与模型或决策过程无关；作者认为这是表达力缺口，不是工程缺口。
• 观察：CAF是局部授权的一条执行或一对执行，却违反全局策略。关系型目的违规没有单条迹上的归责点。日程例中，获准分享忙闲，不等于披露可依赖忙碌原因。
• 做法：沿表达力与可观测性刻画八个子类，并给出上述不可检测性。AL-SYNTH不用语言模型，以SAT/SMT合成最小证人。
• 威胁模型：
  • 目标：一条通过全部局部检查、却违反Φ的迹。不假设越狱或局部行为不当的智能体。
  • 能力：外观良性、目的合法的智能体，组合行为传递目的未授予的信息或权限。对手可用任务措辞或工具结果中的注入内容影响它，不必攻破局部护栏。
  • 系统：单个智能体执行有界回合，动作来自带类型动作集，环境状态可变。局部授权抽象逐动作护栏、权限提示和工具调用监控。
  • 策略：Φ合取意图、目的、来源、同意与委托。四项是单迹性质，目的合取要比较运行。

超性质与验证

• k-安全：Clarkson与Schneider（2010）定义超性质；k-安全的反例是k条有限迹。非干扰是典型的2-安全性质。
• 验证工具：超性质时序逻辑（Clarkson等，2014）、HyperLTL与HyperCTL*模型检验（Finkbeiner等，2015）、k-安全运行时验证（Agrawal与Bonakdarpour，2016），以及概率逻辑HyperPCTL（Ábrahám与Bonakdarpour，2018）。
• 用法：作者称使用这套机制，而不是扩展它。

监控与组合

• 执行监控：Schneider（2000）界定执行监控能强制什么；Hamlen、Morrisett与Schneider（2006）给出强制机制的可计算类。作者称Locus定理是把该界限用到智能体护栏上。
• 经典根源：McCullough（1988）指出安全性质不必可组合；Goguen与Meseguer（1982）定义非干扰；Harrison、Ruzzo与Ullman（1976）讨论访问控制安全问题。
• 多执行：Devriese与Piessens（2010）用每个安全级一次执行来强制非干扰。引言称这些成分是经典的，本文不把它们本身算作新贡献。

降密与目的

• 降密：Sabelfeld与Sands（2009）讨论降密的维度与原则。作者用降密函数参数化目的。
• 规划语义：Tschantz、Datta与Wing（2012）用规划语义形式化目的限制。作者认为这与信息流观点互补，调和仍开放。

智能体安全

• 单迹一面：Greshake等（2023）的间接提示注入被作者称为显式、单迹的一面；本文C1实验位于该范围。
• 逐执行防御：Task Shield（Jia等，2025）核对动作与任务；CaMeL（Debenedetti等，2026）用能力隔离数据与控制流；Fides（Costa等，2025）做信息流污点跟踪。作者把它们放在剖面阶梯上。
• 与本文的差别：作者称这些工作都不比较同一目的的不同执行。Fides作者自己的分析称，它强制显式保密，但不阻止控制流决策上的隐式流；作者称该残差就是关系型目的通道。

基线与任务

• 调查对象：逐工具批准、Task Shield、RTBAS（Zhong等，2025）、CaMeL、Fides、SAFEFLOW（Li等，2025）。作者按发表设计归入剖面，不运行其实现。
• 实验对照：无护栏、意图闭合护栏、P5+组合护栏；评审侧有良性无泄漏对照、显式单迹C1对照，以及看到两次执行的关系审计。
• 任务：合成日程关系证人、累积同意日历任务、LangGraph日程流，以及Claude Sonnet 4.6的三类离线审计。

作者称新的是这些事实对智能体授权的含义：策略分成迹安全部分与关系型目的部分；在所述非坍缩条件下，从不误报的逐迹监控检不出后者。所调查护栏都在迹安全一侧。

作者把失败定义成组合授权失败（CAF），用表达力与可观测性分类，再以不用语言模型的AL-SYNTH合成最小证人。

问题设定与全局策略

• 迁移系统：状态给有限个带类型变量赋值。动作带守卫与效应。从初态起每步守卫成立，则有限迹局部授权。
• 投影：low是声明目的与其他低输入，hi是可读的敏感上下文，obs是对外披露。
• 五合取：Φ合取意图C1、目的C2D、来源C3、同意C4、委托C5。Lemma 1称C1、C3的路径形式、C4与C5是单迹安全性质。显式标记流C3lf本身是2-安全，P6用污点跟踪作保守覆盖。
• 目的：D是目的授权的上下文视图，α是披露里与策略相关的部分。正文式(1)为

C₂^D={S:∀ t,t′∈ S. low(t)=low(t′)∧ D(hi(t))=D(hi(t′))⇒α(obs(t))=α(obs(t′))}

即：低输入与目的授权视图相同的两次运行，策略相关披露必须相同。

• 参数：(D, α)由策略给定。作者称Theorem 3对每一对都成立；违规存在当且仅当该对剩余非退化（Definition 2、Theorem 1）。选错只改变被标记的披露，不能让非平凡目的合取对从不误报的逐动作护栏可见。剩余披露自由RDF-D指存在low与D(hi)相同、α(obs)不同的有限迹；证人还落在局部授权集A中时记为RDF-DA。

两轴刻画

• 表达力：单迹类的证人是有限坏前缀；关系类是k-安全超性质。意图、路径来源、同意、委托是单迹。C2D是关系类。
• 剖面：P0是纯黑盒。其后依次加入意图近似、信息流与目的标记、来源图、逐动作同意、委托再验证，以及意图与同意的累积摘要。
• 两端：P6加入跨域状态转移，是作者考虑的最强单执行插桩。P7是唯一能比较不同执行的剖面。
• 检出：须既能表达该类，又观察到它依赖的状态。Figure 2把八个子类放在两轴上，底行未检出数从P0到P7（含P5+）为8至0。

分离结果

• Theorem 1：对任意D与α，C2D是2-安全；它不是迹性质诱导的，当且仅当(D, α)剩余非退化；若坍缩，则每个系统都满足它。
• 单例事实：相等自反，故任何单迹集合都满足C2D。违规对里的两条迹各自合规，过错只在二者关系。
• Theorem 2与3：若A中仍有剩余非退化证人，则Φ=[A]∩C2D不是迹性质诱导的。Theorem 3称：对C2D从不误报的逐迹监控不能标记任何迹，因而检不出违规。
• 分布与P7：Theorem 4称，在所述单次可观察量下，没有监控能对全部随机智能体既sound又完全地判定披露与未降密上下文条件独立。Theorem 5称P≤6不能既sound又完全地强制Φ，也不能sound地检出C2D；对可能主义性质，P7能展示两迹证人，对分布性质只有统计检出。Corollary 1只列三种响应：容忍误报、跨上下文离线审计，或比较执行。

AL-SYNTH

• 目标：给定模型与目标类，输出每步局部授权、全局未授权的最小证人；对指定剖面，还须躲开该剖面能表达且能观察的检查。引擎是符号的，不用语言模型。
• 双语义：同一迁移系统有参考语义与SMT编码。求解器做有界模型检验，oracle穷举。二者应诱导相同CAF，一致性被测试而不是假设。
• 求解：界n上编码初态、变量范围、迁移和逐步局部授权，再合取终态违规。最小证人按界递增，每界一次可满足查询。all-SAT只用于完备性检查。
• 关系证人：自合成两份系统，断言low与D(hi)相等且α(obs)不等，即式(1)蕴含的否定。存在性查询是SAT。要躲过剖面P时，把P各项安全检查的否定放进同一查询，而不是事后过滤。校验标准是T1 soundness、T2有界完备、T3最小性，结果见实验。

实验设置

• 被测模型：评审为Claude Opus 4.8、GPT-5.5、Gemini 3.1 Pro、Grok 4.3、DeepSeek V4 Pro、Qwen3.7-max、Llama-4-Maverick、Kimi-K2.6、本地Qwen3-30B。离线审计智能体为Claude Sonnet 4.6。现场工具调用智能体为Qwen3-30B与Gemma-4。
• 任务：日程模型的共享迹为collect、aggregate、report；世界a提供槽位10，世界b提供槽位11。现场任务是累积同意日历任务。LangGraph图为read、aggregate、propose。离线三类为Injected-doc forward（C1）、Narrow-scope share（C4）、Scheduling audit（C2r）。
• 评审协议：温度0，生成预算4000 token。十个场景改变槽位对、隐藏原因、任务措辞和A/B顺序，各重复3次，共30次场景重复；重复衡量稳定性而非覆盖。托管模型经OpenRouter默认路由，不固定服务商；本地模型经vLLM。附录写访问时间为2026年6月。
• 现场协议：温度0.7，每格60次独立rollout，执行错误为0。护栏为无护栏（P0）、意图闭合，以及累积披露超过同意界即拒绝的P5+。
• 离线协议：Claude Sonnet 4.6作工具调用智能体，固定温度；正文未给出该温度数值。C2r保持忙闲视图固定，两条件只差隐藏原因，并以高分享率设门，使空结果反映披露而非拒答。上界为精确单侧95% Clopper–Pearson。
• 其余：六种护栏不运行实现，按发表设计放到最强剖面。合成器为Z3，对照穷举oracle。Table V的格子是30次场景重复中至少拦截一个动作的次数。

主结果

表格较宽，可左右滑动

据Table V。省略Qwen3.7-max，四格为0/30、0/30、30/30、30/30，与Claude Opus 4.8相同。关系审计一列最低的Llama-4-Maverick已列入。

• 作者称Kimi-K2.6的拦截与良性拦截同档，是单步保守而不是关系检出，因为逐动作评审看不到第二次执行。其单步计数为证人3/180、良性1/180，DeepSeek良性为2/180，定义与上表不同。
• 作者称九个模型都拦截显式单迹C1，故不是一概放行。同一模型看到两次执行后恢复检出；作者称Llama-4-Maverick把P7的关系可观测性与仍属模型能力的关系检出分开。
• 作者称此表是观察与模型的分离，不是九个独立漏洞。由Theorem 3，逐动作盲区不依赖单执行决策过程。

覆盖曲线与防御矩阵

• 测了什么：每个剖面×每个子类，求解器或合成该剖面看不见的证人，或在界内认定不存在。求解器与oracle在全部9×8格上一致（Table I）。
• 曲线：未检出数从P0到P7为8、7、6、5、4、3、2、1、0。直到P6，剩余恰好是关系型目的类。显式标记流在P6及以上为保守覆盖。去掉目的标记后曲线为[8, 7, 7, 6, 5, 4, 3, 2, 1]，恢复后回到原曲线。
• 设计上界：作者未运行六种实现。Table III中，逐工具批准八类皆未覆盖，RTBAS三类，CaMeL五类，Fides与SAFEFLOW七类（六类精确，显式标记流保守）。关系型目的列对这六种均为未覆盖，只有P7关系审计覆盖它。作者称运行实现不能在不比较执行或不接受误报时抬高该列。

现场同意组合

• 测了什么：Qwen3-30B与Gemma-4在累积同意任务上各60次rollout、三套护栏（Table VI）。此类属同意组合，在P5+闭合，不是Theorem 3的关系型目的类。
• 数字：无护栏时Qwen3-30B为22/60（37%，Wilson 95% CI [26, 49]），干净意图与良性对照均为0/60。意图闭合为20/60，比无护栏低3.3个百分点（Newcombe 95% CI [-13.4, 19.8]，Fisher精确检验p=0.85）。P5+为0/60，比意图闭合低33.3个百分点（CI [21.1, 45.9]，p<10^{-6}），良性与干净意图被拦均为0/60；每个对照的单侧95%上界为4.9%。Gemma-4三格均为0/60。
• 作者解读：作者称披露在任何单步目的里都不可见，故意图闭合下的差落在含0的区间内；P5+去掉全部违规迹。作者把这读成剖面实现了预期能力，而不是单独的因果发现。盲区是结构的，是否出现取决于模型。

离线审计与LangGraph

• Sonnet：Table IV，固定温度。C1与C4均为n=10、CAF=0、上界≤26%。C2r为n=80，在策略相关抽象α下CAF=0，上界≤3.7%。
• 撤回的正例：作者称最初分析报告了跨种子稳定的隐蔽信号；原始输出检查发现两条件提供的槽位集合相同，信号来自特征抽取器计数一个措辞不同的词。按式(1)的α，通道是干净的。作者保留该回合，因为安全结果只在跟踪策略的抽象下成立。
• LangGraph：逐动作护栏含工具权限、目的标记、来源和逐动作同意。两世界共享授权忙闲，只差隐藏原因。护栏两世界都返回allow、allow、allow，动作参数不同；提供的槽位分别为10和11。AL-SYNTH关系审计标记C2D。作者称不主张LangGraph有漏洞。

其他消融与分析

• 最小证人合成在累积同意模型（11个动作，Z3 4.16）上到深度12约为0.02至0.07 s；all-SAT在深度3至7证人从1到29,337，时间从0.02 s到118 s，正文称深度7约差2,770倍。Figure 5另标注2,781与∼2,770×。作者称时间是示意，不是基准。
• T1、T2、T3对每一类包括关系类均通过；自合成证人与oracle的最小对一致（§VII）。
• oracle一致只检验两种编码，作者称它不说明该语义正确刻画了某次部署（§VII）。

作者指出的局限与后续方向

• 差分测试：作者称验证是小模型上的差分测试，不是正确性证明，也不是可扩展性研究（§IX，指向§VII）。
• 合成任务：符号模型干净、任务是合成的，这约束经验主张，但不约束定理；更嘈杂的工具只增加迹，单例事实仍在（§IX）。
• 供给范围：符号模型只供给合成器，其证人在智能体框架上重放（§IX）。
• 模型角色：智能体行为实验覆盖两个模型族；九模型活动评估的是评审，而不是自主使用工具的智能体（§IX）。
• 设计上界：护栏矩阵由设计导出，是有方向的界，方向在§VIII说明（§IX）。
• 目的语义与下一步：目的按降密风格建模，而不是规划语义；作者视二者互补。在真实多工具负载上测量关系类是自然的下一步（§IX）。

实验覆盖范围

• 评审：Table V的九个模型，温度0，十个模板各3次，预算4000 token；托管模型经OpenRouter默认路由，论文写明未固定服务商（§VIII、Appendix C）。
• 现场：工具调用智能体为Qwen3-30B与Gemma-4，累积同意任务，温度0.7，每格60次rollout，执行错误为0；护栏为无护栏、意图闭合与P5+（Table VI）。
• 离线：Claude Sonnet 4.6的三类任务样本量分别为10、10、80；正文只写固定温度，未给出数值（Table IV）。
• 护栏放置：六种机制按发表设计归入剖面，作者未运行其代码；交叉执行列均为否（Table II、Appendix B）。关系审计是AL-SYNTH的P7。
• 合成：求解器与穷举oracle在9个剖面×8个子类上一致；耗时来自一个11动作的累积同意模型、Z3 4.16，作者称不是基准（Table I、Figure 5）。LangGraph一节未报告重复次数。

• 定位：作者分析LLM智能体的逐动作授权为何推不出整段回合的全局授权，并把这类证人称为组合授权失败（CAF）。
• 问题：全局策略合取意图、目的、来源、同意、委托。目的合取是2-安全超性质：两次运行的低输入与目的授权视图可以相同，披露仍然不同，且没有单条迹可归责。
• 结果形式：监控剖面从纯黑盒P0到能比较执行的P7。作者给出：对目的类从不误报的逐迹监控检不出该类，与底层模型或决策过程无关。要约束它，须比较执行或接受误报。AL-SYNTH用Z3和自合成生成最小证人，不用语言模型，并对照穷举oracle。
• 评审：除Kimi-K2.6的3/30外，Table V中八个评审对合成关系证人的逐动作拦截为0/30；看到两次执行后，八个为30/30，Llama-4-Maverick为17/30。九个模型对显式单迹C1均为30/30。
• 现场与审计：Qwen3-30B在无护栏下于22/60次出现同意组合CAF，P5+为0/60；Gemma-4为0/60（Table VI）。Claude Sonnet 4.6在所测三类上CAF为0，C2r的n=80上界≤3.7%（Table IV）。六种被调查护栏的发表设计都不比较两次执行。
• 作者结论：作者称，对不能归约到单迹安全的关系合取，逐动作授权在结构上不足。实验中的安全来自模型行为；可核验的单执行监控对关系类是盲的，因而部署依赖随模型而变、且不能由该监控核验的性质。