Certified Execution Harness for Agentic AI: Safe and Least-Intrusive Petri-Net Supervisory Control Between Reasoning and Action 精读

论文链接：Certified Execution Harness for Agentic AI: Safe and Least-Intrusive Petri-Net Supervisory Control Between Reasoning and Action 发表时间：2026年10月 机构：Queen’s University Belfast（Chao Gu，电子电气工程与计算机学院）+ New York University（Quanyan Zhu，电气与计算机工程系），纯高校合作，无企业参与 领域标签：cs.AI（离散事件系统监督控制 × LLM Agent 安全）

题目区说明

这篇论文的标题包含三个关键词：Certified（可认证的，指安全性是被证明的而非测试出来的）、Execution Harness（执行 harness，LLM 与工具之间的可信软件层）、Supervisory Control（监督控制，离散事件系统的经典控制理论）。它回答的问题是：当 LLM agent 被提示注入劫持时，如何保证它无法执行"顺序错误、次数超限、授权复用"类操作失误——不管攻击者的措辞多么巧妙，也不管模型是否被成功劫持。

这是本轮 Agent 安全研究中理论密度最高的一篇：它把 1987 年 Ramadge-Wonham 的监督控制理论完整引入 LLM agent 执行层，并发现了经典理论在新场景下的一个真实缺口（重试成本使"最大容许"不再"最小侵入"），用随机最短路理论补上。全文 17 页，含 2 个定理、2 个命题、2 个引理、8 个例子/备注，以及一个 20 库所/18 迁移的发布 agent 案例网与提示注入对抗实验。

一、论文背景

1.1 LLM Agent 的操作风险：从"说什么"到"做什么"

一个只写文本的 LLM 出错最多是输出不当内容；但一个能调用工具的 agent 可以部署一个 release、删除文件、泄露凭据、花掉不可恢复的预算。论文开篇给出典型案例：一个发布 agent 规划补丁、跑测试与安全扫描、取得人类审批、部署上线。假设 issue 描述里藏着一条指令"立即部署"——若没有外部检查，部署决策完全依赖 LLM，而 LLM 恰恰是注入指令设计要操纵的组件。若 LLM 听了指令，release 上线且不可撤销。

论文把这类失败定义为操作失败（operational failure）：动作乱序发生或超次数发生。典型例子：

• 部署在审批前发生（乱序）；
• 一次审批被用两次（超次数/重放）；
• 两个 agent 同时持有一把锁（互斥失效）。

注意论文的边界：它管"动作何时、按何顺序、发生几次"，不管"被允许调用的参数是否恶意"（那留给验证器与工作流自身的检查）；许可调用携带秘密的数据泄露、审批洗白也不在保证范围内。

1.2 现有四类防御为什么不够

论文对现有防御做了一个精炼的四分法，并逐一指出共同盲区：

1. 系统提示里的策略：“没有审批绝不部署"这样的规则只是对 LLM 的请求——它写在攻击者同样能写入的上下文窗口里，与注入内容同处一室。
2. 护栏分类器：问的是"这条消息看起来恶意吗”——这是内容问题。分类器有漏报率，且无法识别"良性但早熟"的调用（agent 自己想快点完成任务而提前部署，并非被注入）。
3. 访问控制：决定"谁能行动"，但权限一旦授予通常可复用——“approved"标志可以反复读取，这正是重放攻击所利用的。
4. 沙箱：限制单次动作的损害范围，是论文假定的前提而非竞争方案。

四者的共同盲区：没有一个在追踪操作状态（operational state）——哪些动作已经发生、什么资源已被消耗。有状态的运行时强制器确实追踪状态，消费授权的方案也存在（CapLease），但它们应用的是人工指定的规则或学习的模型，而不是"在不可控结果下综合（synthesize）出来的监督者”。

1.3 关键概念：不可控事件

监督控制理论的核心区分是可控与不可控事件。在 agent 场景：

• 可控：agent 自己的工具调用、消息、记忆写入——kernel 可以拒绝它们；
• 不可控：工具结果、人类决定、外部事件（如生产事故冻结发布）、已启动 rollout 的完成——这些无法拒绝，只能接纳。

安全方案的真正难点由此显现：监督者必须在"我无法拒绝下一个事件"的前提下，预先防止系统进入危险状态。比如事故冻结发生（不可控）后，监督者不能再放行任何会发布到冻结环境的动作——这要求事前就把这类状态间的转移切断。

1.4 两个理论传统的相遇

论文站在两个传统的交汇处：

• Petri 网监督控制（Giua/DiCesare/Silva 1992 的 monitor place、Yamalidou et al. 1996 的 place invariant 反馈、Iordache/Antsaklis 2002 的线性约束综合）：用库所不变式强制线性约束，无需枚举状态。
• Ramadge-Wonham 监督控制（1987）：可控/不可控事件划分、最大容许安全非阻塞监督者的不动点综合。

这两个传统在制造系统领域成熟了三十年，但从未被用于 LLM agent 的执行 harness——论文的贡献正是这次系统性的移植加上为 agent 特有的"拒绝-重试"闭环补上的新理论。

二、论文定位和关联工作

2.1 谱系一：LLM Agent 的 harness 级防御（同期工作，论文 Related Work 详评）

• CaMeL（Debenedetti et al., SaTML 2026, Defeating Prompt Injections by Design）：分离控制流与数据流——特权 LLM 只见可信查询并生成伪代码计划，隔离 LLM 解析不可信内容且无工具权，自定义解释器追踪数据 provenance 并按 capability 标签在工具调用时强制策略。AgentDojo 上可证明安全下解决 77% 任务（无防御 84%）。
• Progent（Shi et al., arXiv:2504.11703）：符号策略限制工具特权，且运行中动态更新策略。
• AgentSpec（Wang et al., ICSE 2026）：强制执行用户指定规则；ProbGuard（ASE 2026）：运行时监控学习的马尔可夫链，可能向 agent 返回违规信息。
• SafeHarness（arXiv:2604.13630）：限制能力的调用次数；CapLease（arXiv:2608.01710）：消费式授权状态，防重放。
• Ray（arXiv:2607.22868）：认证运行时安全的理论，其 gate 的阻塞决策影响后续提案，在期望风险约束下优化，每次阻塞合规提案有代价。

论文对这些工作的判词是一句结构性的总结：它们都没有建模授权的消耗、没有从含不可控事件的工作流模型综合出最大容许策略、没有针对"拒绝引发的重试"优化干预。

2.2 谱系二：监督控制与相关形式化方法（经典理论）

• Petri 网监督控制（monitor place 强制线性约束，Giua 等 1992；不可控迁移下的阻塞与可控性，1994）；
• 最大容许监督者对 agent 程序的刻画（De Giacomo et al., AAMAS 2012，ConGolog 情境演算 agent 的监督）；
• Petri 网组织 agent 工作流（Borghoff et al. 2025 的 TB-CSPN）；
• 攻击下的监督控制（Carvalho et al., Automatica 2018）——对手腐化 plant-监督者信道（传感器/执行器）；本文对手则作用于提议者（LLM 本身），威胁模型不同；
• 最优监督控制（Sengupta & Lafortune 1998；Kumar & Garg 1995）：已知"代价最优监督者可能更严"；本文的 Example 1 给出的是在所有提议者上无界的代价比值，且代价来源（拒绝引发的重试）是新的；
• 语言测度控制（Chattopadhyay & Ray 2007）：最优监督者当且仅当目标测度更小时禁用可控迁移——与本文阈值规则形式对偶，但本文安全是硬约束而非负权状态，且代价累积到任务结束、无随机终止；
• 安全滤波（control barrier functions, Ames et al. 2019）与盾牌合成（Bloem et al. 2015, shield synthesis；Alshiekh et al. 2018, safe RL shielding）：每时刻最小修改/最小干扰——Example 1 同样说明"每步拒绝最少"不等于"总体侵入最小"。

2.3 定位总结

一句话定位：这是首个把监督控制理论（含不可控迁移、monitor place、最大容许综合、重试代价优化）完整引入 LLM agent 执行安全的工作，与其说与 CaMeL 等竞争，不如说它在"防御可证明化"方向上补上了"操作状态显式建模 + 综合式监督者"这块此前所有 harness 防御都缺失的基座。

三、问题定义

3.1 从具体场景到抽象问题

具体场景：发布 agent 被注入"立即部署"。抽象的核心洞察是：“何动作已发生、何资源已被消耗"这一操作状态，本身就是一种与措辞无关、与模型是否被劫持无关的安全判据。

论文的深层结构类比是：

执行 harness ≈ 制造系统的监督控制器；LLM 提议 ≈ 不可靠的操作员指令；工具结果/人类决定 ≈ 不可控事件；授权/预算 ≈ 可消耗的资源 token

在这个视角下，“注入防御"问题被转化为一个有四十年历史的数学问题：给定含不可控迁移的 Petri 网与禁止状态集，离线综合一个监督者，使闭环永远避开禁止状态且总能到达终点。

3.2 形式化定义

AEPN（Agent 执行 Petri 网）：N = (P, T, A, Σ, κ, G, E, M0; ℓ, ω, χ)——前八项是着色 Petri 网（库所、迁移、弧、颜色集、颜色指派、守卫、弧表达式、初始标识），后三项给每个迁移标注：动作名 ℓ(t)（工具/消息名）、责任主体 ω(t)（哪个 agent/人/环境）、可控性 χ(t) ∈ {c, u}。

• mark（标识单元）：一个操作事实——一项能力、一条证据、一次审批、一单位预算。注意论文特意用 mark 而非 Petri 网文献惯用的 token，避免与 LLM 的文本 token 混淆。
• 颜色：mark 的元数据，如审批所批产物的密码学摘要（digest）——颜色绑定使"A 产物的审批不能花在 B 产物上"成为守卫条件，防审批偷换。
• 标识 M：mark 在库所上的分布 = 操作状态。
• 着色网可展开为无色网（颜色集有限时），监督者在展开网的可达集 Q 上综合。

准入规则（admission rule，式 1）——LLM 的每次提议 uk 经四重检查，全部通过才执行：

1. 接口解析：α(uk, Mk) = tk ≠ ⊥（提议能映射到某可控迁移）；
2. 验证器：V(uk, tk, Mk) = 1（内容/策略条件，如白名单）；
3. 网使能：tk ∈ En(Mk)（所需 mark 都在场——结构性检查，与措辞无关）；
4. 监督者允许：tk ∈ S(Mk)。

不通过则拒绝，拒绝作为错误返回 LLM——重规划闭环闭合：agent 可以再提议，每次重试耗一次推理调用。

安全迁移（Theorem 1）：四假设下网上安全性迁移到运行系统 X：

• A1 初始对应：具体状态与初始标识对应；
• A2 步模拟：被接纳动作/外部事件对应迁移发射；内部步（推理、检索、收到拒绝）不改标识；
• A3 安全反射：标识不在禁止集 B ⇒ 具体状态安全；
• A4 完全中介：(a) agent 诱导的每个后果性动作必须经准入规则（由沙箱+凭据代理强制，排除绕过 kernel 直连部署服务的红箭头）；(b) 每个外部事件必须经认证信道在 kernel 中作为不可控迁移发射（工具结果与人类决定由构造观察；其他事件如事故须由源头认证上报，无法匹配已使能不可控迁移的事件触发停机升级人类）。

重规划闭环（核心新概念）：提议者 π(·|M)（对可控迁移+⊥的分布，可提议未使能的迁移）、环境移动 µ/ρ、监督者的控制模式 γS(M) = S(M) ∩ Enc(M)。每轮：以 µ 概率环境移动（代价 0），否则 agent 抽 t～π——在 γ 内则以代价 ca ∈ [0,1] 执行（ca=1 时计推理调用数，ca=0 时计拒绝数），否则以代价 1 拒绝。到终态 Mτ ∈ F（完成/弃权/升级）付终代价 g。目标：最小化期望总代价 J_S(M) = E[Σcost + g]——即侵入性（intrusiveness）。

3.3 这个抽象的精妙之处

三处设计体现了形式化的功力：

1. “拒绝≠禁用”：经典监督控制里被禁事件不发生就完了；LLM agent 收到拒绝会再提议——拒绝不是终点而是新的成本事件。这一个差异推翻了"最大容许=最优"的直觉，是全文理论的种子。
2. 可消耗授权使防重放成为线性不等式：“部署次数 ≤ 审批次数"由一个 monitor place 的不变式强制，对任意审批数成立、无需枚举状态；且该计数规则非正则（Myhill-Nerode 类两两不同）——有限自动机原理上表达不了，这从计算理论层面说明了为什么选 Petri 网而非 FSM。
3. 安全与侵入分层：安全性只依赖网+监督者（对提议与环境移动的任意序列成立），侵入优化依赖提议者模型但估计错误只损侵入性不损安全性（细化只删迁移）——把"必须对的"与"最好对的"分离，是工程可信度的关键设计。

四、问题解法

4.1 总体架构：不信任的提议者 + 可信的 kernel

图 1/图 2 的架构把系统切成两侧：

• 不可信侧（模型侧）：LLM + 上下文窗口（含所有可能被注入的内容：网页、文档、工具结果、同伴消息）+ 规划与上下文管理。规划只产生提议 uk。
• 可信侧（执行 harness）：接口（α 解析 + V 验证）、Petri 网 kernel（持有标识 Mk）、监督者 S、全量日志（每次提议与每次发射按主体 ω(t) 记录）。

七个 harness 组件到 AEPN 的映射（Remark 3）：规划→提议；上下文管理→历史 Hk（留在网外）；agent 状态→标识 Mk；工具→迁移 ℓ(t)；记忆→事实为 mark、文本留网外；编排→网结构+主体 ω；治理→监督者+禁止集 B+终集 F。这个映射表是把 agent 工程实践翻译成形式模型的词典。

4.2 消费式授权与 monitor place（第 IV-B 节）

前置条件两种形态：

• 测试（tested）：自环弧，发射后 mark 归还——“已批准"标志可无限复用（重放漏洞的来源）；
• 消耗（spent）：单向弧，发射吃掉 mark——tapprove 生产 papproved 的 mark，texec 消费它。状态方程给出 M(papproved) = M0 + y(tapprove) − y(texec) ≥ 0 对一切发射序列成立：执行数永不超过审批数+初始数，由网结构单独保证。

一般化：约束 η⊤y ≤ β 由一个 monitor place pc 强制（C(pc,·) = −η⊤），只禁 η(t)>0 的迁移且只在防违例时禁。颜色绑定：tapprove 给 mark 上产物 digest 色，texec 守卫要求消耗的 mark 颜色 = 所执行产物 digest——审批偷换被结构性阻止，且每个 digest 展开成独立库所，各自满足计数不等式。

4.3 最大容许监督者综合（第 IV-C 节）

两步不动点：

• 步骤一（安全）：W0 = Q\B，W_{j+1} = W_j \ UPre(Q\W_j)，稳定于对不可控发射封闭的最大子集 K⋆（U 是"某不可控迁移能进入该集"的标识集）。上确界安全监督者 S⋆ 只接纳射入 K⋆ 的可控迁移。
• 步骤二（非阻塞）：若 F 不可达则一味安全会饿死任务（拒绝一切也是安全的）。交替删除"K 内不可达 F 的标识"与步骤一的删除，联合不动点 K↑ ⊆ K⋆——对不可控封闭且每标识可在 K↑ 内达 F 的最大子集。S_K↑ = {t ∈ Enc(M) | Mt ∈ K↑} ∪ Tu。

命题 1（改编自 RW 经典）：安全非阻塞监督者存在 ⟺ M0 ∈ K↑；存在时 S_K↑ 是最大容许的（任何安全非阻塞 S 在其到达的每个标识上只允许 S_K↑ 允许的迁移）。综合离线完成，运行时准入是查表。

4.4 重规划闭环与"最大容许≠最小侵入”（第 V 节，主技术贡献）

Example 1（三库所反例网）：Mstart 可走 tenter 进 Mroom（room 里 agent 以概率 b 提议会被拒的 tfault、1−b 走 texit 到目标）或直接 tdirect。S_K↑ 两者都放行（room 安全）；更严的 S’ 拒 tenter 只留 tdirect。计算得：ca=1 时 J_{S_K↑} = 1 + a/(1−b) 而 J_{S’} = 1/(1−a)；当 b > a 时更严者更省，且 b→1 时 J_{S_K↑}/J_min → ∞——注入指令反复唆使 tfault（b≈1）时，最大容许监督者的成本可任意倍于最小侵入者。

机理：S_K↑ 放行进入"安全但多刺"的区域，然后在里面被迫反复拒绝；S’ 在入口一次拒绝，换来内部不再有拒绝。每步最少拒绝 ≠ 总体最少拒绝。

Theorem 2（值阈值细化）：闭环是 K↑ 上的随机最短路问题（Bertsekas-Tsitsiklis 框架，需 proper 策略存在+improper 策略代价无穷，论文严格验证两条件）。J_min 是 Bellman 方程唯一解；最大容许最小侵入监督者：

S_{J_min}(M) = {t ∈ S_K↑(M)∩Tc | J_min(Mt) ≤ J_min(M) + 1 − ca} ∪ Tu

即：拒绝某迁移当且仅当接纳它（ca + J_min(Mt)）比拒绝它（1 + J_min(M)）更贵。由 Lemma 1 的中值（mediant）结构（Dinkelbach 分式规划同型）导出。关键性质：细化只从 S_K↑ 删迁移——提议者估计错误只影响侵入性，安全性永不破坏；估计满足 B1（覆盖性）时 properness 亦保，真实提议者与环境平稳且满足假设 B 时以概率 1 到达 F。

计算：J_min 可经策略迭代（解 |K↑| 元线性方程组）或线性规划（J 是满足 O(|K↑||T|) 条件的最大 ΣJ——多项式时间）；每标识最优模式按 v_t 排序取前 m 个（O(|T|log|T|)）；候选 J 可在 O(|K↑||T|) 独立认证（可检验性——不管怎么算出来的，能验就行）。

并发动作的闭式（命题 2+推论 1）：正则 fork（两分支 t1/t2 可任意序、join 汇合、环境移动与分支可交换）上，细化在 M∅ 拒 t1 当且仅当

1/π2({1}) − 1/π1({2}) > 1/π2(∅)

（“拒绝 t1 在两检查间省下的期望拒绝 > 在首检查前新增的期望拒绝”），与 ca 和 J_min(M{1,2}) 无关；两条件互斥（最多定一个序）。且该决策恰好等价于一个 monitor place（t2→pc→t1，M0(pc)=0）——最小侵入的排序干预可以用与安全约束同构的机制实现，这是"编排即治理"的概念统一。

4.5 发布 agent 案例（第 VI 节）

20 库所/18 迁移的网：tplan 规划补丁 → fork-join 的测试 tci 与扫描 tscan → 判断 ok/fail → 请求评审 trequest → 评审 approve/reject（tapprove 消耗 previewer——评审员唯一，一次审批一人）→ 两阶段 rollout：tstart（消耗 papproved 的审批 mark 与 pwin 的窗口位、测试 pnf 无冻结）→ 不可控 tfinish/tfinish_fr 完成 → 可控 tpublish/tpublish_fr 发布到 plive/pbad；事故 tincident/tthaw 移动 pnf/pfr 之间的唯一 mark；tabort 丢弃被冻结抓住的 rollout。禁止集 B = 冻结期间发布（M(pbad)≥1）；终集 F = {plive 或 pabort 或 paborted 标记}。

非负 P-不变式覆盖所有库所（如 M(pnf)+M(pfr)=1，reviewer/approved/dep/staged/live/bad/aborted 之和=1）⇒ 网有界 ⇒ 综合可行。

综合的负结果（Table I 行 4，honest 指派）：诚实指派把 rollout 完成也当作不可控（部署基础设施完成已启动的 rollout，kernel 无法拒绝）时，“在飞 rollout + 冻结 + 完成"可不经监督者允许组合出危险标识——一切含在飞 rollout 的标识落在 K⋆ 之外，tstart 必须被禁。结论：单阶段发布机制下不存在安全监督者（阻塞与否皆然）。综合过程本身定位了病因（先删在飞 rollout 标识），修复方案由此导出：拆出可控的 tpublish 阶段（两阶段 rollout），K↑ = Q\B 恢复可部署。

这个"综合发现架构缺陷"的流程（synthesis as architectural debugging）是案例部分最有工程价值的演示：不是给现有架构配监督者，而是用综合的失败反推架构必须有什么样的"发布后仍可拒绝的步骤”。

五、评估指标与实验证据

5.1 指标体系

本文无学习式实验，评估由三块构成：形式结果（定理/命题的正确性）、综合数值（Table I/II）、注入对抗模拟（Fig. 9）。指标：

5.2 Table I：五种配置的综合结果

读法：行 1 无解冻转移，审批后在飞即被困（安全但到不了 F）⇒ S_K↑ 禁 tapprove；行 2/3 逐步修复可达性；行 4 换诚实指派后不可控完成使"在飞 rollout"标识整块出 K⋆ ⇒ 无任何安全监督者可部署——这是最重要的一行：它证明单阶段部署机制与"完成不可控"这一诚实建模在数学上不兼容，不是调监督者能救的；行 5 两阶段拆分恢复 K↑ = Q\B（staged 被 freeze 抓住仍可经 tthaw 到 F）。评审与判断加入 Tu 时结论不变（行 4 负结果保持——扩大 Tu 只删安全者；行 5 正结果保持——唯一射入 B 的是可控 tpublish_fr）。

5.3 Table II：早熟请求的期望代价（诚实 Tu + 判断/评审入 Tu，|K↑|=30）

提议者：除两个"测试已跑、扫描未跑"的标识（每冻结态一个）以概率 h 早熟提议 tstart、否则提议 tscan 外，对其余使能可控迁移均匀、⊥ 质量 0.15。环境：指数延迟竞争（λok=0.9, λfail=0.1, λapprove=0.4, λreject=0.1, λfinish=1, λincident=0.02, λthaw=0.2）。

要点：

• h=0.98 时常规监督者比最小侵入者多付约 23.2 次期望拒绝/episode（395/17）——攻击性注入下常规监督者的隐性成本可视化。
• 阈值 h* = 43/60 ≈ 0.717：h 超过它，细化就在 fork 入口禁 tci（扫描先行，早熟请求高发的 M{1} 永不被到达）——恰是一个 monitor place（tscan→pc→tci）。
• 最后一行是对称性控制：早熟请求两边等概率时 π1({2})=π2({1})，细化=常规——ΔJ 归零，证明差异确来自"请求位置不对称"而非 h 本身。
• Fig. 8 给出 ΔJ(h) = max{0, h/(2(1−h)) − 43/34} 的解析式与曲线交叉。
• Remark 8 的稳健性：paborted 上的终代价 g_a 在 ≤ 1+5507/1037 ≈ 6.31 之前不改变任何结果；超过后 S_{J_min} 连 tabort 也拒绝，但 h* 与 monitor place 不变——结果对终代价标定的敏感度有精确边界。

5.4 Fig. 9：提示注入扫描（q_inj ∈ [0, 0.5]，每点 10^4 episodes，标准误 ≤ 0.005）

脚本化提议者：按序发出正确下一步，但注入指令以 q_inj 使其立即提议 tstart；另有 0.15 概率良性提前两步。三架构对比：

• 分类器的结构性缺陷被精确暴露：它只能拦"注入的"提议，拦不住"良性但早熟"的 tstart——q_inj=0 时未授权率仍约 0.15（正是良性早熟概率），因为早熟 tstart 执行时 papproved 还空着，这就是一次未授权部署。这一结果与 AEPN 无关地证明了"内容检测类防御无法覆盖操作失败”。
• kernel 恒 0 的机理：tstart 在 papproved 空时根本不使能（check iii 失败），无论措辞；对攻击监督者的注入（staged+冻结时"publish now"映射到使能的 tpublish_fr），check iv 的 S_K↑ 拒绝（唯一被拒的使能迁移）——两条路径都结构性封死。
• 代价：每 episode 约 1.5 次良性拒绝（都是"网尚未使能"的提议），拒绝的注入另计。任务完成 100% 是因为脚本拒绝后继续走下一步；真实 LLM 可能在拒绝后放弃任务——论文如实标注这是 script 提议者的局限（它测的是"一旦 LLM 被劫持各架构会怎样”，不是"多常被劫持”）。

5.5 实验设计如何支撑论点

• Table I 的行 4→5 对照是"综合发现架构缺陷并修复"的完整闭环：负结果不是失败而是诊断输出（先删在飞 rollout 标识 ⇒ 病因是不可控完成）。
• Table II 的行 2/3/4 构成剂量-反应+对称控制：ΔJ 随 h 单调、随对称性归零——“最大容许≠最小侵入"不是构造出来的奇观而是参数化家族中的系统性现象。
• Fig. 9 的 q_inj=0 截距是最聪明的实验设计：把"分类器失败"与"注入存在"解耦——分类器在零注入下也失败，证明其失败是结构性的。
• 三块证据的形式-数值-对抗互补：定理保证"任意序列安全”，表 II/Fig. 9 量化"代价是多少、对照物为何不行"。

六、效果优势的根源解释

本节解释：为什么 AEPN kernel 在注入下未授权率恒 0 且完成率 100%，为什么值阈值细化能省掉数十次拒绝，以及这些优势的边界。

6.1 根源机制与证据链

因果链 1：操作状态显式化 → 安全判定与内容脱钩 → 结构性零泄露

• 机制：mark/标识把"何动作已发生/何授权已消耗"变成数学对象；注入文本无论多巧妙，只能通过 LLM 的提议进入系统，而提议必须通过 check iii（使能）与 check iv（监督者）——两者都只看 (t, M)，不看措辞。
• 证据状态：论文实验已支持（Fig. 9 全区间 0；Fig. 1-2 架构；Theorem 1 迁移）。反事实：unmediated/classifier 在 q_inj=0 即 ≈0.15——去掉网的检查，良性早熟本身就产生未授权部署，说明问题从来不是"恶意内容"而是"无状态防护"。
• 根源：分类器把安全当内容问题（这条消息恶意吗），AEPN 把安全当状态问题（这个动作现在允许吗）——前者概率性且有漏报，后者对"前置条件不满足"类攻击是逻辑恒假的拒绝。

因果链 2：不可控迁移建模 → 监督者综合式预防 → 诚实指派下的架构诊断

• 机制：把工具结果/人类决定/事故设为不可控，综合算法被迫在它们发生前就切断危险前置状态——Table I 行 4 的"无安全监督者"结论正是综合在说：你的部署机制给了系统一条我无法干预的死亡之路（在飞→冻结→完成→bad）。
• 证据状态：论文实验已支持（Table I 行 4→5；行 5 的 K↑=Q\B）。
• 根源：规则指定式防御（AgentSpec 等）只能检查"你写了什么规则"；综合式防御能发现"你需要但没写的规则"（必须有发布后可控步骤）——这是从"规则执行"到"规则发现"的层级跃迁。

因果链 3：重试成本建模 → 拒绝策略的全局优化 → 值阈值细化

• 机制：拒绝不是终点而是昂贵事件（一次推理）；S_K↑ 逐标识最大容许（每步最少拒绝）在全局上可任意差——进入"安全但高拒绝区"的门口一次拒绝，远便宜于进去后被反复拒绝。阈值规则把"局部门禁"升级为"全局期望代价"的 Bellman 最优。
• 证据状态：论文实验已支持（Example 1 无界比值；Table II 的 395/17 vs 20/17；Fig. 8 解析式）。
• 根源：这是经典的"贪心 vs 全局最优"结构在监督控制中的显现，但"拒绝引发重试"这个代价源是 LLM agent 特有的——经典 SCT 里禁用事件没有这种"禁用本身产生新事件"的自反性。
• 反事实：去掉提议者模型（退回 S_K↑），h=0.98 时多付 23 倍期望拒绝；去掉阈值化只用 LP 解 J_min，结果相同（计算路径无关，J 可独立认证）——证明省的是"策略结构"不是"算力"。

因果链 4：细化只删迁移 → 估计错误不破坏安全

• 机制：S_{J_min} ⊆ S_K↑ 恒成立——即使 π 估计全错，细化后的监督者仍是安全非阻塞监督者之一（损失只是侵入性）。
• 证据状态：论文已证明（Theorem 2 后的讨论；Example 1 参数错估 (0.99,0.01)→(0.5,0.99) 时选 S’ 付 100 次期望调用 vs 2 次——侵入惩罚有限且无安全后果）。

6.2 相关工作检索与对照（交叉验证）

证据等级声明：四条因果链的论文内证据均已具备（实验+定理）；“结构防御优于内容检测"的跨工作泛化由 CaMeL 的独立证据线支持，但注意两者实验设定不同（AgentDojo vs 自建脚本注入），不能直接当作因果等价；“每步最小≠全局最小"在 shield 文献中的量化表现本文未测，属阅读者延伸对照。

6.3 综合判断与未决问题

多项研究共同支持的机制：

1. 把安全判定移出内容空间（进入数据流：CaMeL；进入控制状态：AEPN）可以消除对注入措辞的依赖——两条独立路线、独立基准、同构结论（结构性零/近零泄露 + 明确的效用代价）。这是最强的一层共识。
2. 消费式授权对防重放是必要的（CapLease 与 AEPN 的 monitor place 从不同抽象层级到达同一设计）。
3. 贪心的逐点最小干预在存在延迟代价（重试）时可任意次优（本文证明 + 经典最优控制已知现象 + shield 文献的哲学对照）。

仍属推测/单源的机制：

1. 重规划闭环的平稳提议者假设（π 只依赖当前标识；agent 可能在拒绝后坚持重复同一调用、放弃任务或批量提议）——论文自认侵入与终止结论依赖此假设，安全性不依赖；真实 LLM 提议者的分布形态及估计方法（本文案例用均匀+人为 h 参数）是最大悬置。
2. 四假设在真实系统的满足度：A4(b) 要求事故等第三方事件经认证信道上报 kernel（论文给出"kernel 在放行前主动查询冻结状态"的机制），但事件源覆盖的完备性是工程承诺而非数学结论；接口 α 是"最容易出错的部件”（论文自认——A2 的五个反例中接口错映射即破坏安全性）。
3. 规模化：综合复杂度对 |Q| 多项式（LP），但着色网展开可指数爆炸（Remark 1）；论文自列未来工作：组合综合、部分可观标识。20 库所的案例网与真实 agent 的几十上百工具差距未测。

优势成立的条件：操作失败类威胁（乱序/超次/重放/互斥），工作流可建模为有界 Petri 网，四假设可工程化满足。可能失效/不适用的条件：数据内容型攻击（许可调用的参数带毒——需验证器/CaMeL 类数据流控制补位）；“语义级"绕过（注入诱导 agent 走完合法但非意图的路径，如正当流程内塞入后门的补丁——论文 Remark 2 明确不管）；无法中止的外部过程（Table I 行 4 的教训：没有可控的最后一步就没有安全）；真实 LLM 在反复拒绝后的任务放弃行为（script 提议者未覆盖，完成率 100% 是乐观界）。

七、必要知识反推

假设让一个没有相关知识的人完成这项研究，最少必须知道什么？

7.1 领域知识层

• LLM agent 栈的真实结构：harness/scaffold 是什么（执行工具调用的软件）、上下文窗口里什么可信什么不可信——不知道这个就无法画出"不可信提议者/可信 kernel"的分界线（论文 Fig.1 的分界直接决定了哪些组件在可信基内）。
• 提示注入的威胁模型：注入内容如何进入上下文（网页/文档/工具结果/同伴消息）、劫持后能做什么——四类防御的批评（提示内策略/分类器/访问控制/沙箱）每条都对应对现役系统的具体了解。
• 操作失败 vs 内容失败的区别：不理解"乱序/超次/重放/互斥"这一失败分类，就会把问题误做成又一个内容检测器——论文的贡献恰恰建立在这个分类学上。

7.2 方法论知识层

• Petri 网理论：库所/迁移/标识/发射、着色网与展开、状态方程 M = M0 + Cy、P-不变式与有界性判定——消费式授权的计数保证与案例网的有界性证明都靠它。
• 监督控制理论：Ramadge-Wonham 的可控/不可控划分、禁止/终态标识集、UPre 不动点、最大容许安全非阻塞监督者（K⋆/K↑ 的构造）——整个安全层是经典理论的移植。
• 线性约束与 monitor place：Giua 等 1992 起的"η⊤y ≤ β 由一个库所强制"结果——审批计数、预算、变更窗口全部是这一个引理的实例化。
• 随机最短路/动态规划：Bertsekas-Tsitsiklis 框架（proper 策略、Bellman 方程唯一解、策略迭代/值迭代的收敛条件）——Theorem 2 的证明骨架；Dinkelbach 分式规划（pattern value 的中值结构）。
• 形式语言理论基础：Myhill-Nerode 类与正则性——“计数约束非正则"的论证排除了 FSM 方案，是模型选型的理论依据。
• 并发理论：fork/join、互斥、竞争条件——两 agent 一锁的例子与并发动作排序问题需要这部分语言。

7.3 工程知识层

• 发布工程实务：变更窗口、rollout、事故冻结、staged/publish 两阶段、评审员审批——案例网不是玩具恰恰因为它逐个映射了这些真实 DevOps 概念；Table I 行 4 的负结果只有懂发布流程的人才知道其分量（“已启动的部署基础设施会完成 rollout，你拦不住"是诚实的运维事实）。
• 安全工程：沙箱、凭据代理（broker）作为 A4(a) 的强制手段、认证信道、密码学 digest 绑定（颜色）——四假设的"如何满足"讨论全部落在经典安全工程手段上。
• LLM 成本结构：每次提议=一次推理调用=时间与金钱——这是侵入性计量单位（ca=1 计调用）的现实基础，也是"拒绝很贵"这一全篇动机的来源。
• 仿真实验设计：指数延迟竞争的连续时间离散化、脚本化提议者、10^4 episodes 与标准误报告——注入实验的统计规范性。

7.4 知识融合的关键节点

1. 融合节点一（控制理论 × agent 工程）：把"LLM 提议"读作"不可靠操作员指令”、“工具结果"读作"不可控事件”——这个翻译词典（第 IV 节 Remark 3 的七组件映射）让三十年的 SCT 工具箱整体平移到 agent 安全。没有这个节点，两边各自都是成熟的，但永远不会相遇。
2. 融合节点二（重试现象 × 随机最优控制）：识别出"拒绝引发再提议、每次重试耗一次推理"是经典框架里没有的代价结构，并意识到这把监督者选择变成了一个随机最短路问题——Example 1 的三库所小网 + Theorem 2 的 Bellman 刻画，是现象观察与数学工具的精准对接。
3. 融合节点三（综合 × 架构设计）：Table I 行 4 的失败没有被当作实验挫折而是被读作架构诊断（“部署机制缺少可控的最后一步”）——这需要同时相信数学（综合结果的绝对性）与工程（rollout 完成确实不可拒绝）的判断力。综合即调试。
4. 融合节点四（安全性 × 最优性的分层）：让最优层依赖估计（提议者模型）而安全层不依赖（细化只删迁移）——这个分层设计让理论结果在估计不可靠的现实里仍然可部署，是形式化方法落地工程的关键一步。

八、论文中可以提取的通用性灵感

灵感 1：把安全判定从内容空间移到状态空间

• 核心思想：对抗注入/操纵的最稳路径不是更好地区分内容善恶，而是让系统状态本身决定什么被允许——判定函数只看 (动作, 状态)，不看措辞。
• 论文证据：Fig. 9 中 kernel 未授权率全区间恒 0（对任意 q_inj 与任意措辞），而内容分类器在零注入下也失败（良性早熟 ≈0.15）；Theorem 1 保证对提议与环境移动的任意序列成立。
• 推广场景：
  1. 权限系统设计：一次性能力票据（capability token）替代可复用角色权限；
  2. API 网关：按"调用历史状态"而非"请求内容"准入（防重放/防乱序的通用化）；
  3. 金融交易风控：清算状态机决定订单可执行性，合规检查不依赖消息文本；
  4. 数据库权限：行级消费式配额（读一次耗一次授权）防爬取；
  5. 物联网/工控：设备指令的顺序约束网络化，防指令注入。

灵感 2：可消耗授权——“许可"应该是易耗品而非财产

• 核心思想：可无限复用的授权（标志位、角色、会话权限）是重放与滥用之母；把每次授权建模为可消耗的计数资源，约束自动成为线性不变式。
• 论文证据：texec 消耗 papproved 的 mark ⇒ 执行数 ≤ 审批数对一切序列成立（式 2）；“approved 标志可反复读取，重放攻击正利用此"与 Myhill-Nerode 非正则性论证；颜色 digest 绑定防审批偷换。
• 推广场景：
  1. OAuth/能力系统：delegation 链上的每级授权单次有效；
  2. 预算管理：部门预算、云资源配额的 Petri 网化（配额=mark，消耗=发射）；
  3. 合规审批流：一份合同一个审批编号，用后作废；
  4. 区块链交易：UTXO 模型本质就是消费式授权（可作 AEPN 的天然实现层）；
  5. 版本发布：变更窗口=库所，一个窗口一次 rollout 的硬约束。

灵感 3：拒绝不是终点而是成本事件——干预要算总账

• 核心思想：对会重试的对象（agent、用户、机器人）的每次拒绝/阻塞都诱发后续行为，评估干预策略必须算期望总代价而非逐次最优。
• 论文证据：Example 1 中 S_K↑ 每步拒绝最少却在 b→1 时代价任意大；Table II 中 h=0.98 时 23.2 倍差距；阈值规则 J_min(Mt) ≤ J_min(M)+1−ca 就是"接纳 vs 拒绝"的总账比较。
• 推广场景：
  1. 人机交互中的拒绝/纠错设计：错误提示引发的重复尝试成本纳入 UX 评估；
  2. 防火墙/限流策略：被封禁方的重试风暴使"逐包最优"策略总体最差；
  3. 教育与行为矫正：反馈的即时干扰 vs 长期学习曲线的权衡；
  4. 机器人安全停止：急停次数 vs 路径规划的期望时间；
  5. moderation 系统：内容拦截引发的改写重试循环的成本核算。

灵感 4：综合即架构调试——用"无解"反推设计缺陷

• 核心思想：当形式综合报告"约束下无解"时，失败点就是架构缺陷的精确定位；设计验证不应只问"这个架构安全吗”，更要问"什么样的架构才可能安全”。
• 论文证据：Table I 行 4：诚实建模（rollout 完成不可控）下单阶段发布无任何安全监督者；综合先删在飞 rollout 标识直接指出病因；行 5 拆出 tpublish 即恢复 K↑=Q\B——架构修复由数学失败导出。
• 推广场景：
  1. 协议设计：形式化方法发现"无可达成公平性"逼出第三方托管；
  2. 分布式系统：综合失败揭示缺少可拒绝的补偿步骤（Saga 模式的理论根据）；
  3. 组织流程设计：审批流无法满足职责分离 ⇒ 缺少独立终审角色；
  4. 产品权限模型：发现无法同时满足隐私约束与协作需求 ⇒ 缺少中间授权层；
  5. 立法/合规：目标不可同时满足时暴露隐藏的制度变量。

灵感 5：把"必须对的"与"最好对的"分层——估计错误只损效率不损安全

• 核心思想：系统设计中让安全层不依赖任何估计/预测（对最坏情况成立），让优化层自由使用估计（错了只退化性能）——这个分层是可证明系统获得工程弹性的通用模式。
• 论文证据：细化只删迁移 ⇒ 任意错误的提议者估计下仍是安全监督者；估计 (0.99,0.01)→(0.5,0.99) 的错估只把代价从 2 升到 100 而不破坏保证；J 可独立于求解方法被 O(|K↑||T|) 认证。
• 推广场景：
  1. 自动驾驶规划：硬约束层（碰撞避免，任何预测下成立）+ 效率层（轨迹优化，预测驱动）；
  2. 推荐系统：合规过滤器（规则硬保证）+ 排序模型（预测软优化）；
  3. 供应链：安全库存（最坏情况）+ JIT 优化（预测）；
  4. 数据库查询优化：正确性（计划等价性保证）与代价估计分离；
  5. 免疫系统类比：先天免疫（模式硬编码）+ 适应性免疫（预测性抗体）。

灵感 6：不可控事件的诚实清单——防御设计从承认"拦不住什么"开始

• 核心思想：安全设计的第一步不是列能拦什么，而是穷举不可控事件（工具结果、人类决定、外部事故、已启动过程）并对每个给出接纳策略——诚实的不可控清单决定架构形态。
• 论文证据：A4(b) 的分类处理（工具结果由构造观察/人类决定经认证接口/第三方事件认证上报+不匹配即停机升级）；Remark 4 对"未被观察的事件无法触发停机"的坦白及"放行前主动查询冻结状态"的机制；Table I 行 4 正是对"rollout 完成不可控"的诚实承认导致的架构重构。
• 推广场景：
  1. 事故响应手册：按"不可撤回事件"分类设计预案（已发出的邮件/已执行的转账）；
  2. 数据库事务：不可回滚外部调用（支付网关）的Saga 补偿设计；
  3. 谈判策略：对方不可控反应的博弈树剪枝；
  4. 太空/深海工程：通信不可控中断下的自主决策边界；
  5. 政策设计：市场参与者不可控行为下的监管容错。

灵感 7：同一机制（monitor place）统一安全约束与编排决策

• 核心思想：当最优干预呈现"排序"形态时，它可能与安全约束同构——治理（安全）与编排（效率）可以在同一个形式机制里表达，而非两套系统。
• 论文证据：命题 2 + 推论 1：最小侵入对并发动作的排序决策恰等于一个 monitor place（tscan→pc→tci）；与审批计数的 monitor place 结构相同——h* 阈值两侧是"自由序"与"一个库所定序"的精确分界。
• 推广场景：
  1. 微服务编排：依赖注入容器中的顺序约束与安全策略同一 DSL；
  2. 数据管线：血缘约束（数据未脱敏不进下游）与性能调度统一为图约束；
  3. 交通调度：信号灯（安全）与绿波（效率）的统一约束求解；
  4. 编译器优化：语义保持（安全）与指令调度（效率）共用依赖图；
  5. 项目管理：合规里程碑（治理）与关键路径（编排）在同一依赖网络上。

附录：关键符号速查

• mark：库所中的标识单元（能力/审批/预算/证据），论文术语，区别于 Petri 文献的 token 与 LLM 的文本 token；
• 标识 M / marking：mark 在各库所的分布，即操作状态；
• En(M) / Enc(M) / Enu(M)：M 处使能的全部/可控/不可控迁移；
• B / F / Q / K⋆ / K↑：禁止标识集 / 终态标识集 / 可达集 / 对不可控封闭的最大安全子集 / 再加非阻塞（F 可达）后的联合不动点；
• S_K↑ / S_{J_min}：最大容许监督者 / 其值阈值细化（最大容许最小侵入监督者）；
• π / µ / ρ / ca / g：提议者分布 / 环境移动概率 / 不可控分布 / 接纳代价（计调用为 1、计拒绝为 0）/ 终态代价；
• J_S / J_min / Φγ / v_t：监督者 S 的期望总代价（侵入性）/ 最优代价 / 模式值 / 迁移 t 的净价值（J(Mt)+ca−1）；
• h*：早熟请求概率阈值 43/60，超过则细化强制"扫描先行”。