《AI 执行工程论纲》全文版

AI 执行工程论纲

Theses on AI Execution Engineering

版本 1.0　｜　2026 年 7 月　｜　Havenlon Labs　｜　成都海文隆安全科技有限公司

本书提出一门尚未成立的工程学的十条公理、若干定义与命题。

这些理论并非来自纯粹抽象推演，而是从近两年的软件、协议、Runtime、Evidence 与硬件边界实践中逐步总结出来的。

它面向评判而非接受：指出某条公理不必要，或指出一个违反它而仍然成立的系统，都是对本书的有效反驳。

目录

序言　一门尚未存在的工程学

第 0 章　术语、符号与阅读约定

0.1 论断类型与编号约定 　　0.2 符号表 　　0.3 术语表

第 1 章　执行缝隙 Execution Gap

1.1 传统安全的保护域：节点而非路径 　　1.2 AI 引入的结构性变化 　　1.3 执行缝隙的定义与成因 　　1.4 与相邻学科的边界 　　1.5 本章命题小结

第 2 章　执行控制 Execution Control

2.1 判定函数与控制链 　　2.2 意图绑定 Intent Binding 　　2.3 最终否决权（Final Veto） 　　2.4 物理信任边界 　　2.5 证据与判定证明 　　2.6 公理体系（A1–A10）

第 3 章　对抗性完整 Adversarial Completeness

3.1 完整性命题 　　3.2 威胁分类学 EX-STRIDE 　　3.3 四态语义与状态机 　　3.4 保守默认与 Fail Secure 　　3.5 验证方法与残余风险

第 4 章　EBL 执行边界语言

4.1 现有表达形式的不足 　　4.2 执行边界的性质 　　4.3 Constitution 　　4.4 Runtime 　　4.5 Evidence 与 Proof 　　4.6 最小理论模型与非目标

附录

附录 A　端到端案例推演

A.1 场景与意图对象 　　A.2 候选执行 　　A.3 EBL 策略与 AST 　　A.4 第一次裁决：EXPIRED 　　A.5 Fail Secure 　　A.6 证据更新与第二次裁决 　　A.7 硬件边界与执行 　　A.8 案例结论

附录 B　参考架构与硬件边界

B.1 分层参考架构 　　B.2 TEE 与独立 MCU 　　B.3 带外确认与显示绑定 　　B.4 固件锁与底线固化 　　B.5 边界不是单个芯片

附录 C　公理索引・定义索引・失败矩阵

C.1 公理索引 　　C.2 定义索引 　　C.3 失败矩阵

图表索引

图

图 1-1　执行链上的七处关系断裂

图 2-1　从意图到现实的控制链

图 2-2　意图绑定的验证关系

图 2-3　执行控制的分层与能力归属

图 2-4　判定证明的结构

图 3-1　证据状态转移

图 4-1　边界的单向性

图 4-2　Runtime 的输入封闭与输出结构

图 4-3　EBL 的六类对象

图 B-1　执行边界的分层参考架构

表

表 0-1　全书符号约定

表 1-1　传统安全机制的保护域

表 1-2　AI 系统对执行链各维度的扩张

表 1-3　相邻领域的保护域与覆盖边界

表 2-1　执行控制与三类既有机制的判定属性

表 2-2　控制链的五项判定义务

表 2-4　三类传统机制与 Final Veto 的判定属性对比

表 2-3　证据与日志的角色区别

表 2-5　公理的层次结构

表 3-1　安全命题示例

表 3-2　EX-STRIDE 威胁分类矩阵

表 3-3　四态对应的处置差异

表 3-4　误拒绝与误放行的代价结构

表 4-1　现有表达形式与边界语言要求的对照

表 4-2　EBL 宪法条款及其公理依据

表 4-3　判定证明的重放层次

表 4-4　EBL 的非目标

表 C-1　公理速查

表 C-2　证据状态与条件求值结果

序言　一门尚未存在的工程学

过去数十年，软件工程的核心目标是让计算正确发生。编程语言、算法、数据库、网络协议与操作系统的演进，围绕稳定性、效率与可靠性展开；构建于其上的安全体系——身份认证、权限控制、访问管理、加密通信与系统防护——同样服务于一个未曾改变的目标：保证数字世界中的计算按预期完成。这一范式支撑了互联网时代的全部基础设施，也塑造了今天绝大多数信息系统的形态。

该范式成立的隐含前提是：软件提供能力，人类作出执行决定。无论转账、签署合同、启动设备还是批准业务流程，最终将一个数字结论转化为现实动作的主体始终是人。软件在这条路径上承担计算职责，不承担执行职责。

这一前提正在失效。越来越多的 AI 系统不再仅生成内容，而是理解目标、规划任务、调用工具、编排流程，并通过接口与设备影响现实。从企业工作流到工业控制，从数字资产到机器人系统，AI 正在成为现实执行链中的一个环节，而非链外的信息处理工具。由此，一个此前不必单独提出的问题变得必须回答：一个数字意图，需要满足哪些条件，才有资格进入现实世界。

问题的性质与计算正确性不同。计算错误通常表现为程序崩溃、数据异常或服务中断，其后果限于数字域且多数可回滚；执行错误则表现为资金被错误转移、设备被错误启动、权限被错误授予，其后果发生于现实且往往不可撤销。需要被保护的对象，因此从程序本身扩展为从意图到现实结果之间的整条执行路径。

传统软件工程未系统回答这一问题，传统安全工程也未回答——后者的保护域是身份、权限与访问，其判定对象是"谁可以访问什么"，而非"这一个具体动作是否有资格发生"。两者之间存在一片无人认领的区域，本书称之为执行缝隙。

本书提出 AI 执行工程（AI Execution Engineering） 这一工程视角，用以处理该区域的问题。它不替代软件工程，也不是安全工程的延伸，其对象是另一类长期缺乏系统研究的问题：数字系统如何安全、可验证、可追溯地影响现实世界。

围绕这一对象，本书建立四个相互衔接的理论部件，构成一条完整的逻辑链——发现问题，建立控制，证明控制有效，将理论转化为可运行的工程规则：

• Execution Gap（执行缝隙）：界定数字意图进入现实过程中长期存在而未被单独治理的风险区间。
• Execution Control（执行控制）：建立独立于业务系统的裁决机制，使现实动作处于可约束、可证明的边界之内。
• Adversarial Completeness（对抗性完整）：在恶意攻击、异常状态与未知条件下，论证控制能力是否仍然成立。
• EBL（Execution Boundary Language）：将上述结论形式化为可验证、可执行、可审计的规则，使边界能够被工程实现。

本书的体裁是论纲，不是导论。这一区分是实质性的：导论面向已经存在的学科，任务是引导入门；论纲面向尚未成立的学科，任务是提出一组可被检验、也可被推翻的起点。因此本书的写法是给出十条公理、若干定义与命题，并明确标注哪些结论是推导所得、哪些只是工程选择。读者被期待的姿态不是接受，而是评判——指出某条公理不必要，或指出某个系统在违反它的情况下依然成立，都是对本书的有效反驳。

书中不回避未完成的部分。语言尚需设计，Runtime 尚需验证，硬件边界尚未形成标准，不同行业将产生不同实现。但问题已经出现，且不会随着模型能力提升而自行消失。相反的关系更接近事实：AI 越智能、执行越自动、工具越丰富，现实世界越需要一条不会被智能本身绕过的边界。

未来十年需要建立的，不只是更强的模型、更好的 Agent 与更高效的自动化。在这些能力之下，还须存在另一层基础设施。它不负责让系统做更多事情，而负责守住哪些事情仍然不能发生；它不替代人的判断，而确保人的意图不会在进入现实之前被无声改写；它不依赖任何永远可信的主体，而要求关键执行由证据、规则与边界共同证明。

这就是本书所讨论的工程学。

第 0 章　术语、符号与阅读约定

本章不含论证，仅供查阅。首次阅读可跳过 0.3，在正文遇到术语时回查。

0.1 论断类型与编号约定

本书对所有独立成立的论断标注类型。读者可据此判断一项陈述的效力来源，以及反驳它需要付出什么。

工程约定这一类型的存在是刻意的。一门新学科最易犯的错误，是把自身的设计偏好伪装成必然性。凡本书无法从公理推出、而确实作出了取舍之处，一律标为 E 并写明代价。

各章节前以引文格式出现的单句为题记，属修辞性表述，不承担论证责任。正文中带〔补〕标记的段落，为原始论证之外补充的内容。

0.2 符号表

表 0-1　全书符号约定

判定函数的完整形式：

Γ : (I, x, P, K, Ev, Ctx, t) → (d, π)

0.3 术语表

按主题分组。每条给出中文术语、英文对应与工程定义。定义中不含形容词性描述——若删去修饰后定义不再成立，说明该定义依赖修辞而非属性。

问题域

控制机制

边界与能力

证据与证明

失败语义

语言与运行时

对抗分析

第 1 章　执行缝隙 Execution Gap

题记：每一步都合法，最终结果仍然可能是错的。

1.1 传统安全的保护域：节点而非路径

现代安全体系由四类机制构成，它们分别把守执行路径上的不同位置。身份机制保护主体入口，回答"谁进入了系统"；权限机制保护能力边界，回答"谁获得了什么资格"；认证机制保护通信来源，回答"这个请求来自何处"；审批机制保护组织决策，回答"谁表达了同意"。四者在各自的问题域内成熟且有效，其价值不因 AI 的出现而降低。

问题不在于任一机制的有效性，而在于它们的组织方式。这四类机制通常由不同团队、按不同标准、在不同时期分散建设：身份系统只负责身份，权限系统只负责访问，审批系统只负责流程，签名系统只负责签名，执行系统只负责把收到的命令转化为结果。每个系统都完整履行了自身职责，但没有任何一个系统对整条路径负责。

表 1-1　传统安全机制的保护域

上表最后一列构成一个共同的空白：没有任何一列回答"最终发生的现实结果，为什么可以被认为是最初意图的合法延续"。 该问题不属于其中任何一个机制的职责，因而在架构上无人认领。

由此产生一种在实践中常见、在设计上却未被预期的局面：用户身份真实，权限配置正确，审批流程通过，数字签名有效，接口调用成功，设备按指令运行——而最终发生的事情，仍然可能不是用户希望发生的事情。这不是某个节点失守的结果，而是节点之间缺乏连续约束的结果。

命题 P1.1（局部正确的非传递性） 执行链上每个组件均满足其自身规格，不蕴含链的端到端结果符合原始意图。因此"所有组件分别正确 ⇒ 整体结果正确"不是有效推论。

P1.1 是本书全部后续论证的起点。若该推论成立，执行控制便无必要；正因其不成立，才需要一个以整条路径而非单个节点为对象的机制。

1.2 AI 引入的结构性变化

AI 并非第一种能够自动执行任务的软件。脚本、工作流引擎、规则系统、自动化平台与工业控制系统早已承担大量无人干预的操作，自动化本身并不新鲜。真正的变化在于路径的确定时刻：传统自动化沿预先定义的路径运行，路径在部署时确定，运行时不变；AI 系统则在运行过程中解释目标、选择路径并生成动作，路径在运行时才被确定。

这一差别使得"部署时审查路径"这一传统安全手段失去覆盖能力。审查者在部署时能看到的是能力集合，而非将被实际组合出的路径。以下九个维度分别说明该变化如何在执行链的不同位置扩大缝隙。

表 1-2　AI 系统对执行链各维度的扩张

九个维度的共同结构是：每一项都增加了从意图到动作之间的转换次数或转换自由度，而转换正是关系断裂发生的位置（见 1.3）。传统自动化中转换次数少且固定，缝隙表现为个别系统的集成缺陷；AI 系统中转换次数多且可变，缝隙不再是集成时的例外，而成为架构的常态属性。

命题 P1.2（缝隙的常态化） 在运行时确定路径的系统中，执行缝隙不是可通过更严格的集成测试消除的缺陷，而是路径不可预先枚举这一性质的直接结果。

其推论具有工程意义：治理执行缝隙的手段不能是"把所有路径都审查一遍"，因为路径集合在部署时不存在。可行的手段只能是在路径的终点设置约束，即对最终执行对象进行裁决。这一结论将在第 2 章展开。

1.3 执行缝隙的定义与成因

转换点即断裂点

考察一条最简执行链：

Intent → Policy → Approval → Execution

用户提出意图，系统依策略判断，相关方完成审批，执行系统产生结果。从组件构成看这条路径已经完整，但逐段检查可以发现，每两个节点之间都存在一次转换：意图须被解释为结构化请求；请求须被映射为策略输入；策略结论须被转化为审批对象；审批结果须被绑定到最终 Payload；Payload 须被投递到具体执行对象；执行对象须在正确状态与时刻完成动作。

这些转换不自然成立。每一次转换都可能丢失约束、替换对象、补全缺失字段或改变作用范围，而链上通常不存在验证转换忠实性的环节。以意图为例：人类意图天然不完整——"把这笔款付掉"未指明账户、网络、币种、手续费上限与截止时间；"恢复服务器"未指明允许重启的服务范围、是否可丢失当前任务、是否允许切换备用节点。缺失部分必然由下游补全，而补全结果不受原始意图约束。

另一端同样存在结构性局限。多数执行系统的职责被有意设计得狭窄：区块链节点验证交易格式与签名，操作系统验证调用者权限，工业控制器验证命令是否符合协议，API 服务验证 Token、参数类型与请求结构。这些验证保证命令可被接受，不判断命令是否应当被接受。其后果是一组相互指向的假设：上层认为执行端会保障安全，执行端认为上层已完成判断，中间系统认为自己只负责传递，审批系统认为自己只负责收集同意，AI 认为自己只负责完成任务。每一层都把关键责任定位在另一层。

定义

定义 D1.3.1（执行缝隙 / Execution Gap） 从原始意图形成到最终现实结果发生之间，由解释、策略映射、审批、编排、参数生成、对象绑定与状态变化共同构成，而缺乏端到端执行约束的结构性空间。

执行缝隙不是一个时间间隔，也不对应任何单一组件。它是一组关系断裂的集合：意图与请求之间、请求与策略事实之间、策略结论与审批对象之间、审批对象与最终 Payload 之间、Payload 与具体执行对象之间、数字状态与现实状态之间、授权责任与最终后果之间。

图 1-1　执行链上的七处关系断裂

#mermaid-svg-CfzVlvhM265RBRjM{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;fill:#333;}@keyframes edge-animation-frame{from{stroke-dashoffset:0;}}@keyframes dash{to{stroke-dashoffset:0;}}#mermaid-svg-CfzVlvhM265RBRjM .edge-animation-slow{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 50s linear infinite;stroke-linecap:round;}#mermaid-svg-CfzVlvhM265RBRjM .edge-animation-fast{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 20s linear infinite;stroke-linecap:round;}#mermaid-svg-CfzVlvhM265RBRjM .error-icon{fill:#552222;}#mermaid-svg-CfzVlvhM265RBRjM .error-text{fill:#552222;stroke:#552222;}#mermaid-svg-CfzVlvhM265RBRjM .edge-thickness-normal{stroke-width:1px;}#mermaid-svg-CfzVlvhM265RBRjM .edge-thickness-thick{stroke-width:3.5px;}#mermaid-svg-CfzVlvhM265RBRjM .edge-pattern-solid{stroke-dasharray:0;}#mermaid-svg-CfzVlvhM265RBRjM .edge-thickness-invisible{stroke-width:0;fill:none;}#mermaid-svg-CfzVlvhM265RBRjM .edge-pattern-dashed{stroke-dasharray:3;}#mermaid-svg-CfzVlvhM265RBRjM .edge-pattern-dotted{stroke-dasharray:2;}#mermaid-svg-CfzVlvhM265RBRjM .marker{fill:#333333;stroke:#333333;}#mermaid-svg-CfzVlvhM265RBRjM .marker.cross{stroke:#333333;}#mermaid-svg-CfzVlvhM265RBRjM svg{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;}#mermaid-svg-CfzVlvhM265RBRjM p{margin:0;}#mermaid-svg-CfzVlvhM265RBRjM .label{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;color:#333;}#mermaid-svg-CfzVlvhM265RBRjM .cluster-label text{fill:#333;}#mermaid-svg-CfzVlvhM265RBRjM .cluster-label span{color:#333;}#mermaid-svg-CfzVlvhM265RBRjM .cluster-label span p{background-color:transparent;}#mermaid-svg-CfzVlvhM265RBRjM .label text,#mermaid-svg-CfzVlvhM265RBRjM span{fill:#333;color:#333;}#mermaid-svg-CfzVlvhM265RBRjM .node rect,#mermaid-svg-CfzVlvhM265RBRjM .node circle,#mermaid-svg-CfzVlvhM265RBRjM .node ellipse,#mermaid-svg-CfzVlvhM265RBRjM .node polygon,#mermaid-svg-CfzVlvhM265RBRjM .node path{fill:#ECECFF;stroke:#9370DB;stroke-width:1px;}#mermaid-svg-CfzVlvhM265RBRjM .rough-node .label text,#mermaid-svg-CfzVlvhM265RBRjM .node .label text,#mermaid-svg-CfzVlvhM265RBRjM .image-shape .label,#mermaid-svg-CfzVlvhM265RBRjM .icon-shape .label{text-anchor:middle;}#mermaid-svg-CfzVlvhM265RBRjM .node .katex path{fill:#000;stroke:#000;stroke-width:1px;}#mermaid-svg-CfzVlvhM265RBRjM .rough-node .label,#mermaid-svg-CfzVlvhM265RBRjM .node .label,#mermaid-svg-CfzVlvhM265RBRjM .image-shape .label,#mermaid-svg-CfzVlvhM265RBRjM .icon-shape .label{text-align:center;}#mermaid-svg-CfzVlvhM265RBRjM .node.clickable{cursor:pointer;}#mermaid-svg-CfzVlvhM265RBRjM .root .anchor path{fill:#333333!important;stroke-width:0;stroke:#333333;}#mermaid-svg-CfzVlvhM265RBRjM .arrowheadPath{fill:#333333;}#mermaid-svg-CfzVlvhM265RBRjM .edgePath .path{stroke:#333333;stroke-width:2.0px;}#mermaid-svg-CfzVlvhM265RBRjM .flowchart-link{stroke:#333333;fill:none;}#mermaid-svg-CfzVlvhM265RBRjM .edgeLabel{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-CfzVlvhM265RBRjM .edgeLabel p{background-color:rgba(232,232,232, 0.8);}#mermaid-svg-CfzVlvhM265RBRjM .edgeLabel rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-CfzVlvhM265RBRjM .labelBkg{background-color:rgba(232, 232, 232, 0.5);}#mermaid-svg-CfzVlvhM265RBRjM .cluster rect{fill:#ffffde;stroke:#aaaa33;stroke-width:1px;}#mermaid-svg-CfzVlvhM265RBRjM .cluster text{fill:#333;}#mermaid-svg-CfzVlvhM265RBRjM .cluster span{color:#333;}#mermaid-svg-CfzVlvhM265RBRjM div.mermaidTooltip{position:absolute;text-align:center;max-width:200px;padding:2px;font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:12px;background:hsl(80, 100%, 96.2745098039%);border:1px solid #aaaa33;border-radius:2px;pointer-events:none;z-index:100;}#mermaid-svg-CfzVlvhM265RBRjM .flowchartTitleText{text-anchor:middle;font-size:18px;fill:#333;}#mermaid-svg-CfzVlvhM265RBRjM rect.text{fill:none;stroke-width:0;}#mermaid-svg-CfzVlvhM265RBRjM .icon-shape,#mermaid-svg-CfzVlvhM265RBRjM .image-shape{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-CfzVlvhM265RBRjM .icon-shape p,#mermaid-svg-CfzVlvhM265RBRjM .image-shape p{background-color:rgba(232,232,232, 0.8);padding:2px;}#mermaid-svg-CfzVlvhM265RBRjM .icon-shape .label rect,#mermaid-svg-CfzVlvhM265RBRjM .image-shape .label rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-CfzVlvhM265RBRjM .label-icon{display:inline-block;height:1em;overflow:visible;vertical-align:-0.125em;}#mermaid-svg-CfzVlvhM265RBRjM .node .label-icon path{fill:currentColor;stroke:revert;stroke-width:revert;}#mermaid-svg-CfzVlvhM265RBRjM :root{–mermaid-font-family:\”trebuchet ms\”,verdana,arial,sans-serif;}#mermaid-svg-CfzVlvhM265RBRjM .gap>*{stroke-dasharray:5 5!important;}#mermaid-svg-CfzVlvhM265RBRjM .gap span{stroke-dasharray:5 5!important;}

① 解释损耗

② 事实缺证

③ 对象不一致

④ 绑定缺失

⑤ 投递偏移

⑥ 状态漂移

⑦ 责任断裂

意图

结构化请求

策略判断

审批对象

最终 Payload

执行对象

现实结果

图中每条虚线代表一次未被验证的转换。执行控制的任务，即是把其中每一条虚线转化为可验证的实线关系。

合法路径产生错误结果

执行缝隙最难处理之处在于，它不依赖任何违规行为。考察一条完全合法的路径：用户合法登录，提出真实请求，AI 合法调用工具，Agent 使用被授权的接口，策略引擎正常返回允许，审批者完成确认，签名系统生成有效签名，执行端成功完成动作。从日志看，八个步骤全部正常。但若第一步中模型误解了执行对象，其后七个安全机制所保护的，是这一误解沿链条顺利传播的过程。

命题 P1.3（合法路径的失效） 合法主体、合法权限与合法流程的组合，不排除产生与原始意图不符的现实结果。因此执行缝隙不能被归类为访问控制缺陷、模型安全缺陷或业务逻辑漏洞——它横跨三者的边界。

责任缺失

上述结构的组织成因是清晰的。现代系统按组件划分责任：模型团队负责模型能力，Agent 团队负责任务编排，身份团队负责认证，安全团队负责权限，业务团队负责审批，设备团队负责执行，审计团队负责留痕。每个团队都能证明其组件符合设计要求，而现实结果不由任何单一组件产生，它由整条链共同产生。

若组织未定义独立的执行控制责任，系统便默认接受 P1.1 所否定的那个推论。

命题 P1.4（端到端责任缺失） 在按组件划分责任的组织结构中，若不设立以最终现实结果为对象的独立责任主体，则执行链上不存在对该结果负责的主体。所有人负责一部分，等价于无人负责最终结果。

P1.4 是一项组织命题而非技术命题，但它决定技术方案能否落地：执行控制若不对应一个明确的责任主体，其部署将缺乏组织依据。

1.4 与相邻学科的边界

AI 执行工程不在真空中提出。它与若干成熟领域存在交集，但保护域不同。明确边界的目的不是划分地盘，而是说明为何既有领域的成果无法直接覆盖本书所定义的问题。

表 1-3　相邻领域的保护域与覆盖边界

其中与本书最接近的是功能安全与形式化验证。两者都建立了"证明而非声明"的传统，本书的对抗性完整（第 3 章）与判定证明（第 2.5 节）直接受其影响。差别在于判定对象：功能安全处理"设备失效是否导致危险"，其输入指令的正确性是前提而非结论；形式化验证处理"实现是否符合规约"，规约的正确性同样是前提。AI 执行工程恰好处理这两个被作为前提的部分——指令是否忠实于意图，以及在无法证明时应当发生什么。

与 SRE 的关系需要单独说明，因为二者存在真实的方向冲突。SRE 以可用性为优化目标，故障时倾向于保持服务；执行控制以保守失败为架构属性，无法证明时拒绝放行。该冲突不可通过技术手段消解，只能通过明确划分适用范围来处理：对可回滚的数字操作，可用性优先合理；对不可撤销的现实动作，保守失败优先。这一划分本身是工程约定，其论证见 3.4。

1.5 本章命题小结

四条命题共同确立了本书的问题域：需要被治理的对象不是任何单个节点，而是节点之间的转换关系；需要被建立的机制不是更严格的组件规格，而是以最终执行对象为判定对象的独立裁决。第 2 章给出该机制的结构。

第 2 章　执行控制 Execution Control

2.1 判定函数与控制链

题记：审计告诉你发生了什么。执行控制决定它是否发生。

2.1.1 控制的对象

"控制"是一个被过度使用的词。权限控制、访问控制、流程控制、设备控制、风险控制都可简称为控制，但它们各自约束的对象不同：权限约束主体的能力范围，访问约束资源的可达性，流程约束步骤的顺序。执行控制所约束的对象是唯一的——最终进入现实的那一个动作。

这一对象的确定性带来一组具体的判定内容。执行控制需要回答的不是"该主体是否有权做这类事"，而是：将要执行的精确动作是什么，作用于哪个对象，依据哪些事实，是否与原始意图保持一致，被批准的是否仍是当前这个对象，当前状态是否仍满足必要条件，是否存在足以否决的异常。

定义 D2.1.1（执行控制 / Execution Control） 在现实动作发生之前，对意图、最终执行对象、条件、证据及其相互绑定关系进行独立裁决，并仅在完整条件被证明成立时释放执行能力的一组工程机制。

定义中的三个限定词各自排除一类常见误解：之前排除审计，独立排除自证，证明成立排除默认放行。以下逐一说明。

2.1.2 三项区分性质

执行控制常被误认为已由现有机制提供。将其与审计、权限、流程三者对照，可见其判定属性均不相同。

表 2-1　执行控制与三类既有机制的判定属性

其一，位置在结果之前。 审计记录系统做了什么、由谁操作、是否成功，这对追责与复盘不可替代，但它无法阻止已经发生的动作。只能发出告警而不能中止执行的系统，属于监控系统，不属于控制系统。执行控制必须处于一个特定位置：条件不成立时，现实动作不能发生（公理 A5、A10）。

其二，判定单次动作而非长期资格。 权限通常长期存在——账户在一段时期内持有某项能力，服务长期可调用某接口。执行控制的判定则是一次性的：这一笔、这一台、这一次、这组参数，在当前状态下是否允许。同一主体的同类操作在不同时刻可以得到不同结果。持有转账权限不蕴含任何一笔转账都应被允许，因为目标账户是否与意图绑定、金额是否与审批一致、是否仍在时间窗口内、是否出现冲突证据，都属于权限模型不表达的信息（公理 A9）。

其三，检查结果而非过程外观。 一条流程可以在外观上高度完备：多因素认证、三人审批、加密传输、硬件密钥签名、全程留痕。但若审批对象与签名对象之间不存在可验证绑定，上述机制保护的只是"一个错误结果被顺利地完成"。执行控制不接受流程完整性作为放行依据，它的判据是最终执行对象能否由完整证据证成（公理 A3、A7）。

由第三项直接得到：

命题 P2.1（控制深度） 控制点若不覆盖最终执行对象，则无法关闭执行缝隙。仅控制意图、仅控制审批、或仅控制签名，均不构成执行控制。

2.1.3 判定函数

将上述性质形式化，执行控制的核心是一个判定函数：

Γ : (I, x, P, K, Ev, Ctx, t) → (d, π)

Γ 接收意图 I、候选执行对象 x、策略 P、宪法 K、证据集 Ev、上下文 Ctx 与判定时刻 t，输出决策 d ∈ {ALLOW, DENY, SAFE_MODE} 及判定证明 π。

Γ 须满足三项性质，它们同时构成 Runtime 实现的验收标准：

• 确定性：相同输入产生相同 (d, π)。这排除了以概率模型充当判定组件（见 §2.3.2）。
• 封闭性：Γ 不读取参数以外的隐式状态。这排除了"上层已经判断过"这一类隐含前提——上层提交的是证据，不是结论（公理 A7）。
• 单调收缩性：∀P，ALLOW(Γ) ⊆ ALLOW(Γ|P=∅)。策略只能缩小放行集合。这是公理 A4 的形式表达。

输出为三值而非布尔值，是因为"证明不成立"与"证明成立且结论为拒绝"是两种不同状态，压缩后将丢失运维所需的区分（详见 §3.3）。

2.1.4 控制链

判定函数是单点视角。将其置入完整路径，得到执行控制链。

图 2-1　从意图到现实的控制链

#mermaid-svg-W8KaEHm2DMEwOUW1{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;fill:#333;}@keyframes edge-animation-frame{from{stroke-dashoffset:0;}}@keyframes dash{to{stroke-dashoffset:0;}}#mermaid-svg-W8KaEHm2DMEwOUW1 .edge-animation-slow{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 50s linear infinite;stroke-linecap:round;}#mermaid-svg-W8KaEHm2DMEwOUW1 .edge-animation-fast{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 20s linear infinite;stroke-linecap:round;}#mermaid-svg-W8KaEHm2DMEwOUW1 .error-icon{fill:#552222;}#mermaid-svg-W8KaEHm2DMEwOUW1 .error-text{fill:#552222;stroke:#552222;}#mermaid-svg-W8KaEHm2DMEwOUW1 .edge-thickness-normal{stroke-width:1px;}#mermaid-svg-W8KaEHm2DMEwOUW1 .edge-thickness-thick{stroke-width:3.5px;}#mermaid-svg-W8KaEHm2DMEwOUW1 .edge-pattern-solid{stroke-dasharray:0;}#mermaid-svg-W8KaEHm2DMEwOUW1 .edge-thickness-invisible{stroke-width:0;fill:none;}#mermaid-svg-W8KaEHm2DMEwOUW1 .edge-pattern-dashed{stroke-dasharray:3;}#mermaid-svg-W8KaEHm2DMEwOUW1 .edge-pattern-dotted{stroke-dasharray:2;}#mermaid-svg-W8KaEHm2DMEwOUW1 .marker{fill:#333333;stroke:#333333;}#mermaid-svg-W8KaEHm2DMEwOUW1 .marker.cross{stroke:#333333;}#mermaid-svg-W8KaEHm2DMEwOUW1 svg{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;}#mermaid-svg-W8KaEHm2DMEwOUW1 p{margin:0;}#mermaid-svg-W8KaEHm2DMEwOUW1 .label{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;color:#333;}#mermaid-svg-W8KaEHm2DMEwOUW1 .cluster-label text{fill:#333;}#mermaid-svg-W8KaEHm2DMEwOUW1 .cluster-label span{color:#333;}#mermaid-svg-W8KaEHm2DMEwOUW1 .cluster-label span p{background-color:transparent;}#mermaid-svg-W8KaEHm2DMEwOUW1 .label text,#mermaid-svg-W8KaEHm2DMEwOUW1 span{fill:#333;color:#333;}#mermaid-svg-W8KaEHm2DMEwOUW1 .node rect,#mermaid-svg-W8KaEHm2DMEwOUW1 .node circle,#mermaid-svg-W8KaEHm2DMEwOUW1 .node ellipse,#mermaid-svg-W8KaEHm2DMEwOUW1 .node polygon,#mermaid-svg-W8KaEHm2DMEwOUW1 .node path{fill:#ECECFF;stroke:#9370DB;stroke-width:1px;}#mermaid-svg-W8KaEHm2DMEwOUW1 .rough-node .label text,#mermaid-svg-W8KaEHm2DMEwOUW1 .node .label text,#mermaid-svg-W8KaEHm2DMEwOUW1 .image-shape .label,#mermaid-svg-W8KaEHm2DMEwOUW1 .icon-shape .label{text-anchor:middle;}#mermaid-svg-W8KaEHm2DMEwOUW1 .node .katex path{fill:#000;stroke:#000;stroke-width:1px;}#mermaid-svg-W8KaEHm2DMEwOUW1 .rough-node .label,#mermaid-svg-W8KaEHm2DMEwOUW1 .node .label,#mermaid-svg-W8KaEHm2DMEwOUW1 .image-shape .label,#mermaid-svg-W8KaEHm2DMEwOUW1 .icon-shape .label{text-align:center;}#mermaid-svg-W8KaEHm2DMEwOUW1 .node.clickable{cursor:pointer;}#mermaid-svg-W8KaEHm2DMEwOUW1 .root .anchor path{fill:#333333!important;stroke-width:0;stroke:#333333;}#mermaid-svg-W8KaEHm2DMEwOUW1 .arrowheadPath{fill:#333333;}#mermaid-svg-W8KaEHm2DMEwOUW1 .edgePath .path{stroke:#333333;stroke-width:2.0px;}#mermaid-svg-W8KaEHm2DMEwOUW1 .flowchart-link{stroke:#333333;fill:none;}#mermaid-svg-W8KaEHm2DMEwOUW1 .edgeLabel{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-W8KaEHm2DMEwOUW1 .edgeLabel p{background-color:rgba(232,232,232, 0.8);}#mermaid-svg-W8KaEHm2DMEwOUW1 .edgeLabel rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-W8KaEHm2DMEwOUW1 .labelBkg{background-color:rgba(232, 232, 232, 0.5);}#mermaid-svg-W8KaEHm2DMEwOUW1 .cluster rect{fill:#ffffde;stroke:#aaaa33;stroke-width:1px;}#mermaid-svg-W8KaEHm2DMEwOUW1 .cluster text{fill:#333;}#mermaid-svg-W8KaEHm2DMEwOUW1 .cluster span{color:#333;}#mermaid-svg-W8KaEHm2DMEwOUW1 div.mermaidTooltip{position:absolute;text-align:center;max-width:200px;padding:2px;font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:12px;background:hsl(80, 100%, 96.2745098039%);border:1px solid #aaaa33;border-radius:2px;pointer-events:none;z-index:100;}#mermaid-svg-W8KaEHm2DMEwOUW1 .flowchartTitleText{text-anchor:middle;font-size:18px;fill:#333;}#mermaid-svg-W8KaEHm2DMEwOUW1 rect.text{fill:none;stroke-width:0;}#mermaid-svg-W8KaEHm2DMEwOUW1 .icon-shape,#mermaid-svg-W8KaEHm2DMEwOUW1 .image-shape{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-W8KaEHm2DMEwOUW1 .icon-shape p,#mermaid-svg-W8KaEHm2DMEwOUW1 .image-shape p{background-color:rgba(232,232,232, 0.8);padding:2px;}#mermaid-svg-W8KaEHm2DMEwOUW1 .icon-shape .label rect,#mermaid-svg-W8KaEHm2DMEwOUW1 .image-shape .label rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-W8KaEHm2DMEwOUW1 .label-icon{display:inline-block;height:1em;overflow:visible;vertical-align:-0.125em;}#mermaid-svg-W8KaEHm2DMEwOUW1 .node .label-icon path{fill:currentColor;stroke:revert;stroke-width:revert;}#mermaid-svg-W8KaEHm2DMEwOUW1 :root{–mermaid-font-family:\”trebuchet ms\”,verdana,arial,sans-serif;}

d = ALLOW，释放 cap

d = DENY

证明不完整

x / Ev / Ctx 变化，A9 重裁决

Intent定义目标与不可变约束 I.inv

Policy定义业务必要条件

Approval绑定 hash(x)

Evidence证明条件当前成立

Candidate Execution x精确动作对象

Final Veto / Γ确定性裁决

Execution现实动作

SAFE_MODE

拒绝

这条链与普通工作流的差别在于传递物的性质。工作流逐级传递结论：上一环节完成，下一环节据此继续。控制链逐级建立可验证关系：意图定义目标与边界，策略定义必要条件，审批绑定具体对象，证据证明条件当前成立，候选执行表达精确动作，最终裁决对全部关系一次性求值。任一关系不成立，链条不产生 ALLOW。

据此，一个完整的执行控制过程须回答五个问题，它们分别对应链上的环节与公理：

表 2-2　控制链的五项判定义务

本章其余各节依次展开第 3 至第 5 项：§2.2 处理意图与最终对象的绑定，§2.3 处理否决权的归属与独立性，§2.4 处理否决在物理层的生效方式，§2.5 处理条件成立的证明形式。

〔补〕关于回边的说明。 图 2-1 中由 Execution 指向 Γ 的虚线是公理 A9 的结构表达，原稿未显式给出。它意味着控制链不是有向无环图：长时执行、分批执行与流式执行场景中，Ctx 在执行过程中持续变化，单次裁决的有效性存在时间边界。该边界的确定属于工程约定，本书不给出通用取值。

2.2 意图绑定 Intent Binding

题记：上层批准的是一种描述，底层执行的是另一种对象。

2.2.1 意图与执行之间的三重距离

公理 A2 断言 I ≠ x，其依据是三项彼此独立的性质。

其一，意图天然不完整。 "把这笔款付掉"未指明账户、网络、币种、手续费上限与截止时间；"恢复服务器"未指明允许重启的服务、是否可丢失当前任务、是否允许切换备用节点；"打开仓库"涉及身份、时段、区域、设备状态与现场人员等多项未言明的条件。缺失部分必然由下游补全，补全结果不受原始表述约束。

其二，同一意图对应多个执行方案。 支付可经由不同网络、不同手续费策略、不同结算时点完成；设备恢复可经由重启、切换备用节点或降级运行达成。方案之间在成本、风险与不可逆程度上差异显著，而意图本身不区分它们。

其三，意图在链上被反复转换。 从自然语言到结构化请求，到策略输入，到审批对象，到最终 Payload，到执行对象——每一次转换都是一次重新表达，每一次重新表达都是一次可能的偏移点（图 1-1）。

三者共同决定：意图不能作为执行的直接依据，只能作为执行的约束来源。

2.2.2 意图对象与不变量集

若意图仅存在于对话记录、会议纪要或使用者的认知中，它无法参与裁决。执行控制要求意图被固化为可哈希、可签名、可引用、可审计的对象。

定义 D2.2.1（意图对象 / Intent Object） 表达期望发生什么并携带约束的可验证结构，至少包含：意图标识、发起主体、目标对象、操作类型、必要约束、允许范围、禁止条件、有效时间、证据要求、审批要求、可接受的执行结果。后续所有策略求值、审批与执行，须引用同一意图对象或其无歧义派生对象。

一种直觉的绑定方法是保存原始提示词与最终命令并比较二者。该方法不可行：自然语言意图与机器指令不处于同一表达层。"向供应商支付合同尾款"对应一段结构化交易数据，一个设备操作目标对应多条低层控制命令，两者之间不存在文本层面的可比性。文本相似度既不充分也不必要。

可行的做法是定义哪些属性必须在全部转换中保持不变，即意图的不变量集 I.inv：

I.inv = {执行对象, 数量或金额, 时间窗口, 目标系统, 风险等级,
允许的方法, 禁止条件, 审批范围, 最终载荷摘要}

系统无须证明中间表达逐字相同，只须证明 I.inv 中每一项从起点延续至终点。

定义 D2.2.2（意图绑定 / Intent Binding） 候选执行对象 x 与意图对象 I 之间的可验证关系，满足：x 的对应属性在 I.inv 的每一项上与 I 一致，且该一致性可由 π 重放验证。任一项不一致，绑定失败。

图 2-2　意图绑定的验证关系

#mermaid-svg-LhWCr7uyhygGPOHt{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;fill:#333;}@keyframes edge-animation-frame{from{stroke-dashoffset:0;}}@keyframes dash{to{stroke-dashoffset:0;}}#mermaid-svg-LhWCr7uyhygGPOHt .edge-animation-slow{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 50s linear infinite;stroke-linecap:round;}#mermaid-svg-LhWCr7uyhygGPOHt .edge-animation-fast{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 20s linear infinite;stroke-linecap:round;}#mermaid-svg-LhWCr7uyhygGPOHt .error-icon{fill:#552222;}#mermaid-svg-LhWCr7uyhygGPOHt .error-text{fill:#552222;stroke:#552222;}#mermaid-svg-LhWCr7uyhygGPOHt .edge-thickness-normal{stroke-width:1px;}#mermaid-svg-LhWCr7uyhygGPOHt .edge-thickness-thick{stroke-width:3.5px;}#mermaid-svg-LhWCr7uyhygGPOHt .edge-pattern-solid{stroke-dasharray:0;}#mermaid-svg-LhWCr7uyhygGPOHt .edge-thickness-invisible{stroke-width:0;fill:none;}#mermaid-svg-LhWCr7uyhygGPOHt .edge-pattern-dashed{stroke-dasharray:3;}#mermaid-svg-LhWCr7uyhygGPOHt .edge-pattern-dotted{stroke-dasharray:2;}#mermaid-svg-LhWCr7uyhygGPOHt .marker{fill:#333333;stroke:#333333;}#mermaid-svg-LhWCr7uyhygGPOHt .marker.cross{stroke:#333333;}#mermaid-svg-LhWCr7uyhygGPOHt svg{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;}#mermaid-svg-LhWCr7uyhygGPOHt p{margin:0;}#mermaid-svg-LhWCr7uyhygGPOHt .label{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;color:#333;}#mermaid-svg-LhWCr7uyhygGPOHt .cluster-label text{fill:#333;}#mermaid-svg-LhWCr7uyhygGPOHt .cluster-label span{color:#333;}#mermaid-svg-LhWCr7uyhygGPOHt .cluster-label span p{background-color:transparent;}#mermaid-svg-LhWCr7uyhygGPOHt .label text,#mermaid-svg-LhWCr7uyhygGPOHt span{fill:#333;color:#333;}#mermaid-svg-LhWCr7uyhygGPOHt .node rect,#mermaid-svg-LhWCr7uyhygGPOHt .node circle,#mermaid-svg-LhWCr7uyhygGPOHt .node ellipse,#mermaid-svg-LhWCr7uyhygGPOHt .node polygon,#mermaid-svg-LhWCr7uyhygGPOHt .node path{fill:#ECECFF;stroke:#9370DB;stroke-width:1px;}#mermaid-svg-LhWCr7uyhygGPOHt .rough-node .label text,#mermaid-svg-LhWCr7uyhygGPOHt .node .label text,#mermaid-svg-LhWCr7uyhygGPOHt .image-shape .label,#mermaid-svg-LhWCr7uyhygGPOHt .icon-shape .label{text-anchor:middle;}#mermaid-svg-LhWCr7uyhygGPOHt .node .katex path{fill:#000;stroke:#000;stroke-width:1px;}#mermaid-svg-LhWCr7uyhygGPOHt .rough-node .label,#mermaid-svg-LhWCr7uyhygGPOHt .node .label,#mermaid-svg-LhWCr7uyhygGPOHt .image-shape .label,#mermaid-svg-LhWCr7uyhygGPOHt .icon-shape .label{text-align:center;}#mermaid-svg-LhWCr7uyhygGPOHt .node.clickable{cursor:pointer;}#mermaid-svg-LhWCr7uyhygGPOHt .root .anchor path{fill:#333333!important;stroke-width:0;stroke:#333333;}#mermaid-svg-LhWCr7uyhygGPOHt .arrowheadPath{fill:#333333;}#mermaid-svg-LhWCr7uyhygGPOHt .edgePath .path{stroke:#333333;stroke-width:2.0px;}#mermaid-svg-LhWCr7uyhygGPOHt .flowchart-link{stroke:#333333;fill:none;}#mermaid-svg-LhWCr7uyhygGPOHt .edgeLabel{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-LhWCr7uyhygGPOHt .edgeLabel p{background-color:rgba(232,232,232, 0.8);}#mermaid-svg-LhWCr7uyhygGPOHt .edgeLabel rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-LhWCr7uyhygGPOHt .labelBkg{background-color:rgba(232, 232, 232, 0.5);}#mermaid-svg-LhWCr7uyhygGPOHt .cluster rect{fill:#ffffde;stroke:#aaaa33;stroke-width:1px;}#mermaid-svg-LhWCr7uyhygGPOHt .cluster text{fill:#333;}#mermaid-svg-LhWCr7uyhygGPOHt .cluster span{color:#333;}#mermaid-svg-LhWCr7uyhygGPOHt div.mermaidTooltip{position:absolute;text-align:center;max-width:200px;padding:2px;font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:12px;background:hsl(80, 100%, 96.2745098039%);border:1px solid #aaaa33;border-radius:2px;pointer-events:none;z-index:100;}#mermaid-svg-LhWCr7uyhygGPOHt .flowchartTitleText{text-anchor:middle;font-size:18px;fill:#333;}#mermaid-svg-LhWCr7uyhygGPOHt rect.text{fill:none;stroke-width:0;}#mermaid-svg-LhWCr7uyhygGPOHt .icon-shape,#mermaid-svg-LhWCr7uyhygGPOHt .image-shape{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-LhWCr7uyhygGPOHt .icon-shape p,#mermaid-svg-LhWCr7uyhygGPOHt .image-shape p{background-color:rgba(232,232,232, 0.8);padding:2px;}#mermaid-svg-LhWCr7uyhygGPOHt .icon-shape .label rect,#mermaid-svg-LhWCr7uyhygGPOHt .image-shape .label rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-LhWCr7uyhygGPOHt .label-icon{display:inline-block;height:1em;overflow:visible;vertical-align:-0.125em;}#mermaid-svg-LhWCr7uyhygGPOHt .node .label-icon path{fill:currentColor;stroke:revert;stroke-width:revert;}#mermaid-svg-LhWCr7uyhygGPOHt :root{–mermaid-font-family:\”trebuchet ms\”,verdana,arial,sans-serif;}

约束

引用

摘要

逐项校验 I.inv

否

意图对象 Ihash(I), I.inv

审批绑定 hash(x)

候选执行 x

Γ

绑定成立

DENY / 重新审批

绑定失败的判定是逐项的，且不接受近似。原始意图批准向账户 A 支付 10 万元：目标变为账户 B，绑定失败；金额变为 11 万元，绑定失败；网络由测试环境变为生产环境，绑定失败；审批已过期，绑定失败；Payload 重新生成导致摘要变化，绑定失败。此处的严格性是刻意的——绑定机制的全部作用，就是阻止"上层批准一种描述、底层执行另一种对象"这一结构。

2.2.3 意图不构成充分条件

意图为真不蕴含执行应当发生。现实状态持续变化，昨日合理的动作今日可能已不合理：供应商账户已更换，设备进入维护状态，风险等级变化，目标对象被撤销，法规条件改变，审批者离职，时间窗口结束，环境证据失效。

命题 P2.2（意图的必要非充分性） 意图对象的存在与绑定成立，是 d = ALLOW 的必要条件，不是充分条件。执行前须另行确认该意图在当前 Ctx 与 t 下仍然有效。

P2.2 与公理 A9 共同排除了一种常见设计：将一次意图确认视为一段时期内的通行证。意图是判定的起点，不是判定的结论。

2.3 最终否决权（Final Veto）

2.3.1 结构性偏向与否决职责的缺位

执行链上的组件——业务系统、Agent 编排器、工作流引擎、审批系统、签名服务、终端设备——在设计目标上均以"推动动作完成"为优化方向。业务系统以任务完成率衡量，编排器以目标达成率衡量，审批系统以流程闭环率衡量，签名服务以请求响应成功率衡量。这一共同倾向并非实现缺陷，而是各组件职责定义的直接结果。其后果是：在一条完整执行链上，可能不存在任何一个以"阻止动作"为首要职责的组件。

由此产生一个结构性判断：若系统中的每一层都只具备"放行"这一有效输出，则该系统不存在边界。分散在各层的拒绝能力——参数校验失败、余额不足、流程超时——均属于功能性拒绝，它们服务于业务正确性，而非执行安全性；这类拒绝在条件被满足或被重试消解后即自动让位于放行。执行控制所要求的是另一类能力：一种独立于业务成功与否、以"证明不成立即拒绝"为唯一判据的输出。

定义 2.3.1（最终否决权 / Final Veto） 在候选执行 x 获得跨越执行边界的必要能力之前，由独立于 x 生成方的判定组件所持有的拒绝能力。该能力满足三项条件：(a) 判定发生在最终动作之前且不可跳过；(b) 输出的非 ALLOW 结果不可被上层组件覆盖、重试或重新解释；© 判定所依据的输入包含最终执行对象本身，而非其上游描述。

Final Veto 的职责边界是狭窄的：它不提出替代方案，不优化流程，不理解业务语义。其唯一命题是判断当前条件是否构成 ALLOW 的完整证明（公理 A8）。这一狭窄性是设计目标而非能力局限——判定组件承担的语义越少，其行为的确定性越高，可被诱导的表面越小。

2.3.2 与传统授权机制的比较分析

审批、数字签名与模型判断三者常被当作执行链的"最后一道关卡"。以定义 2.3.1 的三项条件逐一核验，可见三者均不满足。

（一）审批：时序缺陷。 审批具备拒绝能力，但其发生位置通常处于流程中段。审批完成之后，执行对象仍可能被重新生成、参数被补全、路由被改写、系统状态被变更。当审批人所拒绝或批准的是一段业务描述，而最终执行系统所接收的是一个精确对象时，两者之间不存在可验证的对应关系，审批的授权语义因而无法延伸至最终动作（公理 A3）。审批的失效不在于其判断质量，而在于其判断对象与执行对象之间的时序错位。

（二）数字签名：语义缺陷。 签名机制回答的命题是"某私钥是否同意签署这段数据"。该命题不蕴含"这段数据是否符合原始意图"“参数是否在传递中被替换”“目标账户是否正确”“当前系统状态是否仍然安全”“证据集合是否完整”"是否存在相互矛盾的证据"这六项判断中的任何一项。若签名模块仅对上层提交的 Payload 执行签署，它在功能上是执行链的最后一道技术手续，而非最后一道判断。

命题 P2.4（签名不构成否决） 设签名函数 Sign(k, m) 的判定域仅为密钥 k 的持有状态，则对任意 x，Sign 无法区分 x 是否满足 I.inv。因此在 A2 与 A3 之下，Sign 不满足定义 2.3.1©，不构成 Final Veto。 推论 C2.4：Final Veto 必须位于签名或执行能力授予之前，并有权拒绝提供该能力。

（三）模型判断：确定性缺陷。 AI 组件可有效参与异常发现、风险分析与方案比较，这类能力属于上层判断，价值明确。但 Final Veto 要求同一规则与同一输入产生同一结果（Γ 的确定性性质，见 2.1）。基于概率输出的组件其行为可被上下文改写、被提示词诱导、被措辞影响；在关键条件缺失时，它可能给出"酌情判断"，在证据冲突时，它可能通过语言层面的解释消解矛盾。这两种行为恰好违反公理 A8 所要求的保守闭合。因此，模型可以参与判断，但不应持有最后边界。

表 2-4　三类传统机制与 Final Veto 的判定属性对比

2.3.3 独立性要求

若最终否决权由被控制的系统自身提供，该否决与被否决对象处于同一信任域，一旦该域被攻陷，否决能力与执行能力同时失效。以下结构均属于此类同域配置：SaaS 既生成请求又裁决请求；管理员既配置规则又可关闭规则；Agent 既产生执行对象又验证该对象；钱包既展示交易摘要又直接签署 Payload；设备主控既接收网络指令又决定是否执行。这些配置中的"拒绝"在形式上存在，在对抗条件下不成立（公理 A6）。

据此，Final Veto 的独立性须在六个维度上分别成立：执行路径独立、状态判断独立、规则来源独立、密钥或能力控制独立、日志与证据独立、故障模式独立。其中故障模式独立最易被忽略：若判定组件与被判定系统共享同一供电、同一时钟源或同一网络通道，则一次共因故障即可同时消除两者，独立性在故障域上并不成立。

独立不等于孤立。判定组件可以接收上层提供的信息，但不得将上层结论直接采纳为事实——上层提交的是证据，而非判断。这一区分是 2.5 节 Evidence 模型的直接前提。

2.3.4 输出域与默认态度

执行系统的状态空间不止于"允许"与"拒绝"。当证据缺失、过期或相互冲突时，系统所处的并非"拒绝"，而是"无法完成证明"。将这两类状态压缩为同一个布尔值，会使运维侧丢失区分补交证据、重新签发与人工裁定的依据（详见 3.3）。因此 Final Veto 的输出域定义为 {ALLOW, DENY, SAFE_MODE}，并附带判定证明 π。

工程约定 E2.3（默认态度） 判定组件的默认输出为非 ALLOW。ALLOW 仅在存在完整证明 π 时产生。该约定是设计选择，其代价是可用性下降；其正当性依据在于 3.4 所论证的代价不对称性，而非逻辑必然。

需要明确的是，Final Veto 不承诺判断正确。它承诺的是一项弱得多、但可验证的性质：在证明不成立时，现实动作不会发生。这一性质可被测试、可被审计、可被形式化陈述，而"判断永远正确"不能。导论采用前者作为工程目标，正是因为后者不可交付。

2.4 物理信任边界

题记：硬件的价值不只是保护密钥，而是保护不能发生的事情。

2.4.1 灵活性与确定性的分层

软件的优势在于灵活：可远程升级、动态配置、快速扩展、适应业务变化。安全关键边界所需的属性恰好相反：行为确定、攻击面小、难以修改、不可被远程说服、故障模式可预测、关键约束不可关闭。两组属性存在结构性张力，将它们置于同一层，通常得到一个既不够灵活也不够安全的系统。

执行控制因此采取分层策略：复杂性留在上层，确定性下沉到边界。 上层承担理解、规划、编排与优化，边界只承担一项狭窄职责——在证明不成立时不释放能力。

2.4.2 定义与判据

定义 D2.4.1（物理信任边界 / Physical Trust Boundary） 由独立硬件域独占某项现实动作必要能力所构成的执行边界，满足：(a) 关键执行能力位于该域内；(b) 上层软件不能绕过其裁决直接完成执行；© 边界可独立作出拒绝；(d) 关键规则不可由普通管理员关闭；(e) 关键密钥或控制能力不向上层暴露；(f) 边界能够验证对象、状态与证据；(g) 裁决结果被独立记录。

"使用硬件"不等于具备物理信任边界。一个可被远程更新、完全接受主机命令、不作独立状态判断的硬件模块，在架构上仍是软件系统的外接执行器，其信任域与上层同一，因而不满足公理 A6。

命题 P2.3（密钥保护不等于执行保护） 若硬件模块仅对上层提交的 Payload 执行签名，则其保护对象为密钥而非执行。此类模块降低密钥泄露风险，但不降低错误执行风险。

由 P2.3 可知，硬件安全模块、硬件钱包与安全芯片的既有部署，不自动构成执行边界。使其构成边界，须令其进一步回答：当前 Payload 是否与意图绑定，是否与审批对象一致，必要证据是否完整，时间与状态是否有效，是否触发固定限制，是否存在否决条件。

2.4.3 必要能力

边界的控制力来自其对某项必要能力 cap 的独占。可作为 cap 的能力包括：最终签名密钥、设备启动信号、电源控制、执行令牌、关键通信通道、不可替代的授权证明、最终命令解密能力。

判据是单一的：若上层系统可绕开边界直接完成执行，则该边界是辅助组件而非边界。公理 A10 的工程含义即在于此——边界须成为执行链的必要节点，使得 d ≠ ALLOW ⇒ 动作不可发生。

图 2-3　执行控制的分层与能力归属

#mermaid-svg-NHdIwalUZnhZBQes{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;fill:#333;}@keyframes edge-animation-frame{from{stroke-dashoffset:0;}}@keyframes dash{to{stroke-dashoffset:0;}}#mermaid-svg-NHdIwalUZnhZBQes .edge-animation-slow{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 50s linear infinite;stroke-linecap:round;}#mermaid-svg-NHdIwalUZnhZBQes .edge-animation-fast{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 20s linear infinite;stroke-linecap:round;}#mermaid-svg-NHdIwalUZnhZBQes .error-icon{fill:#552222;}#mermaid-svg-NHdIwalUZnhZBQes .error-text{fill:#552222;stroke:#552222;}#mermaid-svg-NHdIwalUZnhZBQes .edge-thickness-normal{stroke-width:1px;}#mermaid-svg-NHdIwalUZnhZBQes .edge-thickness-thick{stroke-width:3.5px;}#mermaid-svg-NHdIwalUZnhZBQes .edge-pattern-solid{stroke-dasharray:0;}#mermaid-svg-NHdIwalUZnhZBQes .edge-thickness-invisible{stroke-width:0;fill:none;}#mermaid-svg-NHdIwalUZnhZBQes .edge-pattern-dashed{stroke-dasharray:3;}#mermaid-svg-NHdIwalUZnhZBQes .edge-pattern-dotted{stroke-dasharray:2;}#mermaid-svg-NHdIwalUZnhZBQes .marker{fill:#333333;stroke:#333333;}#mermaid-svg-NHdIwalUZnhZBQes .marker.cross{stroke:#333333;}#mermaid-svg-NHdIwalUZnhZBQes svg{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;}#mermaid-svg-NHdIwalUZnhZBQes p{margin:0;}#mermaid-svg-NHdIwalUZnhZBQes .label{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;color:#333;}#mermaid-svg-NHdIwalUZnhZBQes .cluster-label text{fill:#333;}#mermaid-svg-NHdIwalUZnhZBQes .cluster-label span{color:#333;}#mermaid-svg-NHdIwalUZnhZBQes .cluster-label span p{background-color:transparent;}#mermaid-svg-NHdIwalUZnhZBQes .label text,#mermaid-svg-NHdIwalUZnhZBQes span{fill:#333;color:#333;}#mermaid-svg-NHdIwalUZnhZBQes .node rect,#mermaid-svg-NHdIwalUZnhZBQes .node circle,#mermaid-svg-NHdIwalUZnhZBQes .node ellipse,#mermaid-svg-NHdIwalUZnhZBQes .node polygon,#mermaid-svg-NHdIwalUZnhZBQes .node path{fill:#ECECFF;stroke:#9370DB;stroke-width:1px;}#mermaid-svg-NHdIwalUZnhZBQes .rough-node .label text,#mermaid-svg-NHdIwalUZnhZBQes .node .label text,#mermaid-svg-NHdIwalUZnhZBQes .image-shape .label,#mermaid-svg-NHdIwalUZnhZBQes .icon-shape .label{text-anchor:middle;}#mermaid-svg-NHdIwalUZnhZBQes .node .katex path{fill:#000;stroke:#000;stroke-width:1px;}#mermaid-svg-NHdIwalUZnhZBQes .rough-node .label,#mermaid-svg-NHdIwalUZnhZBQes .node .label,#mermaid-svg-NHdIwalUZnhZBQes .image-shape .label,#mermaid-svg-NHdIwalUZnhZBQes .icon-shape .label{text-align:center;}#mermaid-svg-NHdIwalUZnhZBQes .node.clickable{cursor:pointer;}#mermaid-svg-NHdIwalUZnhZBQes .root .anchor path{fill:#333333!important;stroke-width:0;stroke:#333333;}#mermaid-svg-NHdIwalUZnhZBQes .arrowheadPath{fill:#333333;}#mermaid-svg-NHdIwalUZnhZBQes .edgePath .path{stroke:#333333;stroke-width:2.0px;}#mermaid-svg-NHdIwalUZnhZBQes .flowchart-link{stroke:#333333;fill:none;}#mermaid-svg-NHdIwalUZnhZBQes .edgeLabel{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-NHdIwalUZnhZBQes .edgeLabel p{background-color:rgba(232,232,232, 0.8);}#mermaid-svg-NHdIwalUZnhZBQes .edgeLabel rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-NHdIwalUZnhZBQes .labelBkg{background-color:rgba(232, 232, 232, 0.5);}#mermaid-svg-NHdIwalUZnhZBQes .cluster rect{fill:#ffffde;stroke:#aaaa33;stroke-width:1px;}#mermaid-svg-NHdIwalUZnhZBQes .cluster text{fill:#333;}#mermaid-svg-NHdIwalUZnhZBQes .cluster span{color:#333;}#mermaid-svg-NHdIwalUZnhZBQes div.mermaidTooltip{position:absolute;text-align:center;max-width:200px;padding:2px;font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:12px;background:hsl(80, 100%, 96.2745098039%);border:1px solid #aaaa33;border-radius:2px;pointer-events:none;z-index:100;}#mermaid-svg-NHdIwalUZnhZBQes .flowchartTitleText{text-anchor:middle;font-size:18px;fill:#333;}#mermaid-svg-NHdIwalUZnhZBQes rect.text{fill:none;stroke-width:0;}#mermaid-svg-NHdIwalUZnhZBQes .icon-shape,#mermaid-svg-NHdIwalUZnhZBQes .image-shape{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-NHdIwalUZnhZBQes .icon-shape p,#mermaid-svg-NHdIwalUZnhZBQes .image-shape p{background-color:rgba(232,232,232, 0.8);padding:2px;}#mermaid-svg-NHdIwalUZnhZBQes .icon-shape .label rect,#mermaid-svg-NHdIwalUZnhZBQes .image-shape .label rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-NHdIwalUZnhZBQes .label-icon{display:inline-block;height:1em;overflow:visible;vertical-align:-0.125em;}#mermaid-svg-NHdIwalUZnhZBQes .node .label-icon path{fill:currentColor;stroke:revert;stroke-width:revert;}#mermaid-svg-NHdIwalUZnhZBQes :root{–mermaid-font-family:\”trebuchet ms\”,verdana,arial,sans-serif;}

提交 x 与 Ev

(d, π)

d = ALLOW 时释放 cap

此路径必须不存在

底层：物理信任边界（不可绕过）

独占 cap宪法 K 固化

中层：裁决（确定）

EBL RuntimeΓ 求值，输出 (d, π)

上层：业务与智能（灵活）

业务系统

AI Agent 编排

现实动作

图中虚线是全章最重要的一条线：它标记了一条必须不存在的路径。架构评审的核心问题不是"边界是否存在"，而是"该虚线是否真的不存在"。

2.4.4 Owner ≠ God

物理边界蕴含一项组织性结论：系统所有者拥有管理权，不自动拥有关闭全部安全约束的能力。该原则将策略划分为两层——可编程策略 P 由授权方按业务需要修改；固定底线 K 在边界内固化，任何管理身份均不可关闭、削弱或旁路（公理 A4）。

工程约定 E2.4（底线固化位置） K 应固化于持有 cap 的硬件域内，其变更须经由与常规配置不同的物理路径（如现场操作、多方持有的物理凭证、或不可逆的固件熔丝）。该约定的代价是变更成本显著上升，其正当性依据是：可被远程修改的底线，在远程攻陷场景中不成立。

2.4.5 边界不是孤岛

独立不等于孤立。边界须接收上层提供的信息——意图对象、审批记录、证据集合、状态快照——否则无法作出有意义的判定。区分在于信息的地位：上层提交的是证据，不是结论（公理 A7）。边界对证据执行独立验证，对结论不予采信。

同时，边界须具备独立的故障模式。若判定组件与被判定系统共享供电、时钟源或通信通道，一次共因故障即可同时消除两者，A6 所要求的独立性在故障域上不成立。

2.5 证据与判定证明

题记：ALLOW 不是系统没有发现问题，而是系统已经形成完整证明。

2.5.1 结论与事实

上游系统常以结论形式提交信息：“风控已通过”“合规已检查”“身份已验证”。这类陈述在链上被逐级采信，形成一条信任传递链。其问题在于，信任不因传递而增强，却在传递中失去可核验性：接收方无法判断该结论基于何种事实、在何时成立、针对哪个对象成立。

执行控制要求关键事实以证据形式进入判定，且证据是一等输入而非附属记录。

定义 D2.5.1（证据 / Evidence） 用于证成某项条件的可验证事实对象，至少携带四项元数据：类型（证明何种条件）、来源（由谁签发及其可验证凭据）、主体绑定（所描述的对象）、时间语义（生效时刻与有效期）。缺少任一项的输入不构成证据。

2.5.2 证据与日志

证据与日志可能使用相同数据，但在架构中承担不同角色。

表 2-3　证据与日志的角色区别

一次完整执行的证据集最终也应进入审计存储，但只有在执行前参与判定的部分，才属于执行控制的范畴。

2.5.3 四项语义要求

有效期。 证据描述的是某一时刻的事实，而非永久成立的命题。风控快照、设备状态、余额、授权范围均随时间变化。证据须携带有效期，超出后状态转为 EXPIRED，不再参与证明（公理 A8、A9）。

对象绑定。 证据须绑定其所描述的具体对象。"该账户已通过合规审查"若不绑定账户标识，则可被用于证成任意账户；"设备处于安全状态"若不绑定设备标识与状态快照时刻，则可被复用于其他设备或其他时刻。

冲突保留。 当多份同类证据相互矛盾时，系统不得通过选取其一、取多数或按来源优先级消解冲突。冲突本身是一项事实，须被保留并触发 CONFLICT 状态。将冲突消解为单一结论，等于用一次未经证明的裁量替代证据（公理 A7）。

关系独立性。 多方确认常以数量表达——两人批准、三人签名、多数通过。数量不蕴含独立性：三个账户可能由同一人控制，多个服务可能依赖同一凭证，多个审批者可能来自同一管理域，多个传感器可能共享同一故障源。

命题 P2.5（计数不构成独立性证明） 证据数量 n > 1 不蕴含这些证据的失效事件相互独立。若不表达独立性维度，多方确认在共因失效下退化为单方确认。

因此独立性须作为一等语义被显式表达，其维度至少包括：身份主体、设备、信任域、密钥来源、组织角色、物理位置、故障路径。

2.5.4 完整证明与 ALLOW

传统策略系统广泛使用缺省行为：字段缺失时采用默认配置，状态未知时沿用上次结果，检查失败时为可用性继续执行。在可回滚的业务场景中，这类设计有其合理性；在不可逆执行中，它直接违反公理 A8。

d = ALLOW 须由完整证明产生，即以下条件全部成立：每一项必要条件都有对应证据；每一份证据 σ(e) = VALID；每一份证据与对象绑定；证据间不存在未解决的冲突；最终对象与意图及审批一致；未触发任何固定否决条件。

这一要求区分了两种性质相反的判断。"系统未发现问题"是消极判断，其成立依赖于检查的完备性，而检查的完备性无法自证；"系统已形成完整证明"是积极判断，其成立由 π 显式承载，可被重放与审计。执行控制只接受后者。

图 2-4　判定证明的结构

#mermaid-svg-dCEwMXM9GQvGWY8S{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;fill:#333;}@keyframes edge-animation-frame{from{stroke-dashoffset:0;}}@keyframes dash{to{stroke-dashoffset:0;}}#mermaid-svg-dCEwMXM9GQvGWY8S .edge-animation-slow{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 50s linear infinite;stroke-linecap:round;}#mermaid-svg-dCEwMXM9GQvGWY8S .edge-animation-fast{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 20s linear infinite;stroke-linecap:round;}#mermaid-svg-dCEwMXM9GQvGWY8S .error-icon{fill:#552222;}#mermaid-svg-dCEwMXM9GQvGWY8S .error-text{fill:#552222;stroke:#552222;}#mermaid-svg-dCEwMXM9GQvGWY8S .edge-thickness-normal{stroke-width:1px;}#mermaid-svg-dCEwMXM9GQvGWY8S .edge-thickness-thick{stroke-width:3.5px;}#mermaid-svg-dCEwMXM9GQvGWY8S .edge-pattern-solid{stroke-dasharray:0;}#mermaid-svg-dCEwMXM9GQvGWY8S .edge-thickness-invisible{stroke-width:0;fill:none;}#mermaid-svg-dCEwMXM9GQvGWY8S .edge-pattern-dashed{stroke-dasharray:3;}#mermaid-svg-dCEwMXM9GQvGWY8S .edge-pattern-dotted{stroke-dasharray:2;}#mermaid-svg-dCEwMXM9GQvGWY8S .marker{fill:#333333;stroke:#333333;}#mermaid-svg-dCEwMXM9GQvGWY8S .marker.cross{stroke:#333333;}#mermaid-svg-dCEwMXM9GQvGWY8S svg{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;}#mermaid-svg-dCEwMXM9GQvGWY8S p{margin:0;}#mermaid-svg-dCEwMXM9GQvGWY8S .label{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;color:#333;}#mermaid-svg-dCEwMXM9GQvGWY8S .cluster-label text{fill:#333;}#mermaid-svg-dCEwMXM9GQvGWY8S .cluster-label span{color:#333;}#mermaid-svg-dCEwMXM9GQvGWY8S .cluster-label span p{background-color:transparent;}#mermaid-svg-dCEwMXM9GQvGWY8S .label text,#mermaid-svg-dCEwMXM9GQvGWY8S span{fill:#333;color:#333;}#mermaid-svg-dCEwMXM9GQvGWY8S .node rect,#mermaid-svg-dCEwMXM9GQvGWY8S .node circle,#mermaid-svg-dCEwMXM9GQvGWY8S .node ellipse,#mermaid-svg-dCEwMXM9GQvGWY8S .node polygon,#mermaid-svg-dCEwMXM9GQvGWY8S .node path{fill:#ECECFF;stroke:#9370DB;stroke-width:1px;}#mermaid-svg-dCEwMXM9GQvGWY8S .rough-node .label text,#mermaid-svg-dCEwMXM9GQvGWY8S .node .label text,#mermaid-svg-dCEwMXM9GQvGWY8S .image-shape .label,#mermaid-svg-dCEwMXM9GQvGWY8S .icon-shape .label{text-anchor:middle;}#mermaid-svg-dCEwMXM9GQvGWY8S .node .katex path{fill:#000;stroke:#000;stroke-width:1px;}#mermaid-svg-dCEwMXM9GQvGWY8S .rough-node .label,#mermaid-svg-dCEwMXM9GQvGWY8S .node .label,#mermaid-svg-dCEwMXM9GQvGWY8S .image-shape .label,#mermaid-svg-dCEwMXM9GQvGWY8S .icon-shape .label{text-align:center;}#mermaid-svg-dCEwMXM9GQvGWY8S .node.clickable{cursor:pointer;}#mermaid-svg-dCEwMXM9GQvGWY8S .root .anchor path{fill:#333333!important;stroke-width:0;stroke:#333333;}#mermaid-svg-dCEwMXM9GQvGWY8S .arrowheadPath{fill:#333333;}#mermaid-svg-dCEwMXM9GQvGWY8S .edgePath .path{stroke:#333333;stroke-width:2.0px;}#mermaid-svg-dCEwMXM9GQvGWY8S .flowchart-link{stroke:#333333;fill:none;}#mermaid-svg-dCEwMXM9GQvGWY8S .edgeLabel{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-dCEwMXM9GQvGWY8S .edgeLabel p{background-color:rgba(232,232,232, 0.8);}#mermaid-svg-dCEwMXM9GQvGWY8S .edgeLabel rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-dCEwMXM9GQvGWY8S .labelBkg{background-color:rgba(232, 232, 232, 0.5);}#mermaid-svg-dCEwMXM9GQvGWY8S .cluster rect{fill:#ffffde;stroke:#aaaa33;stroke-width:1px;}#mermaid-svg-dCEwMXM9GQvGWY8S .cluster text{fill:#333;}#mermaid-svg-dCEwMXM9GQvGWY8S .cluster span{color:#333;}#mermaid-svg-dCEwMXM9GQvGWY8S div.mermaidTooltip{position:absolute;text-align:center;max-width:200px;padding:2px;font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:12px;background:hsl(80, 100%, 96.2745098039%);border:1px solid #aaaa33;border-radius:2px;pointer-events:none;z-index:100;}#mermaid-svg-dCEwMXM9GQvGWY8S .flowchartTitleText{text-anchor:middle;font-size:18px;fill:#333;}#mermaid-svg-dCEwMXM9GQvGWY8S rect.text{fill:none;stroke-width:0;}#mermaid-svg-dCEwMXM9GQvGWY8S .icon-shape,#mermaid-svg-dCEwMXM9GQvGWY8S .image-shape{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-dCEwMXM9GQvGWY8S .icon-shape p,#mermaid-svg-dCEwMXM9GQvGWY8S .image-shape p{background-color:rgba(232,232,232, 0.8);padding:2px;}#mermaid-svg-dCEwMXM9GQvGWY8S .icon-shape .label rect,#mermaid-svg-dCEwMXM9GQvGWY8S .image-shape .label rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-dCEwMXM9GQvGWY8S .label-icon{display:inline-block;height:1em;overflow:visible;vertical-align:-0.125em;}#mermaid-svg-dCEwMXM9GQvGWY8S .node .label-icon path{fill:currentColor;stroke:revert;stroke-width:revert;}#mermaid-svg-dCEwMXM9GQvGWY8S :root{–mermaid-font-family:\”trebuchet ms\”,verdana,arial,sans-serif;}

证据 e₁σ = VALID

条件 c₁

证据 e₂σ = VALID

证据 e₃σ = VALID

条件 c₂

规则求值P ∧ K

绑定关系I ↔ x ↔ Approval

π：判定证明

d = ALLOW

证明图中的任一节点失效——证据状态非 VALID、绑定不成立、规则未满足——均不产生 ALLOW，且失效位置在 π 中可被定位。这一可定位性是运维可行性的前提：拒绝若不能说明原因，系统将在实践中被绕过。

2.5.5 证据链

一次执行通常跨越多个阶段：意图创建、策略选择、审批提交、状态采集、对象生成。各阶段产生的证据之间存在引用与依赖关系，构成证据链。链结构的意义在于，它使"某项事实为何成立"可被逐级追溯至可验证的源头，而非终止于某个不可核验的断言。

〔补〕关于证明的存储边界。 完整保存全部证据将带来存储与隐私成本，且在多数场景下不必要。可行的工程折中是保存证明的可重放最小集：证据摘要、来源凭据、状态标记与规则版本，使裁决可被重新求值而不必保留原始数据全文。该折中的代价是，原始数据一旦不可获取，重放只能验证一致性而不能验证真实性。

2.6 公理体系（A1–A10）

以下十条构成本书的公理集合。它们不是从原稿论证中"总结"出来的要点，而是被选定为起点的命题——第 2 章前五节的作用，是说明为什么这十条值得被当作起点。

A1　意图可验证性

若不存在可验证的意图对象 I，则 Γ 无定义，输出 d = DENY。

否则会怎样：没有 I 作为参照，任何执行结果都无法被判定为"偏离"。系统可以正确运行，却无法说明自己运行得对不对。 关联：D2.2.1 意图对象、§1.3 执行缝隙的起点。

A2　转换非同一性

I ≠ x。从 I 到 x 必须经过受约束的转换，且转换须保持 I.inv。

否则会怎样：把意图直接当作执行，等于承认自然语言描述与精确动作之间不存在语义损耗。原稿 2.2 全节即在论证该损耗必然存在。 关联：§2.2 Intent Binding、威胁类 X2 意图漂移。

A3　审批对象绑定

任何授权须绑定 hash(x)，不得仅绑定 I 的自然语言描述。

否则会怎样：授权与执行指向不同对象，审批在时序上失去约束力。 关联：§2.3.2、威胁类 X3 对象替换。

A4　策略非权威性

判定为 P ∧ K 的合取。P 不可关闭、削弱或旁路 K。

形式化推论：∀P，ALLOW(Γ) ⊆ ALLOW(Γ|P=∅)——任何策略只能收缩放行集合，不能扩大。 否则会怎样：可编程层获得了修改底线的能力，安全性退化为配置正确性。 关联：§4.3 Constitution、威胁类 X6 权限越权。

A5　边界否决权

若系统中不存在能输出非 ALLOW、且该输出不可被覆盖的组件，则该系统不构成执行控制系统。

否则会怎样：所有组件都只能说"可以"，边界在形式上存在而在功能上缺席。 关联：D2.3.1 Final Veto。

A6　否决独立性

生成 x 的信任域与执行 Γ 的信任域不得同一。

否则会怎样：单点攻陷同时消灭执行能力的约束与约束本身。 关联：§2.3.3 六维独立性、威胁类 X9 供应链污染。

A7　事实证据化

关键条件的成立须由 Ev 证明。来源可信度不构成证明。

否则会怎样：判定退化为对上游组件的信任传递，信任在链条上不可累积却被当作可累积。 关联：§2.5 Evidence、威胁类 X4 证据伪造。

A8　保守闭合

d = ALLOW ⟺ 存在完整证明 π。证据状态 σ(e) ∈ {VALID, UNKNOWN, MISSING, EXPIRED, CONFLICT}，其中仅 σ(e) = VALID 的证据可参与 π。

关键约束：四种非 VALID 状态不可压缩为单一布尔值——它们对应四种不同的运维响应（补交／重新验证／重新签发／人工裁定）。 否则会怎样：无法证明被当作可以执行。 关联：§3.3 四态状态机、E2.3 默认态度。

A9　重裁决义务

x、Ev、Ctx 任一发生变化，既有 (d, π) 立即失效，须重新求值。

否则会怎样：判定结果成为可复用的通行证，时间差本身变成攻击面。 关联：§2.2 意图不能成为永久授权、威胁类 X5 证据失效。

A10　能力控制

边界须独占某项现实动作的必要能力 cap，使得 d ≠ ALLOW ⇒ 该动作不可发生。

否则会怎样：否决只是一个可以被绕过的建议。这是全书中唯一一条要求物理实现的公理——A1–A9 可以在软件中成立，A10 不能。 关联：§2.4 物理信任边界、附录 B。

公理之间的关系

表 2-5　公理的层次结构

四层构成一条闭合链：确定对象（对象层）→ 确定权威（权威层）→ 确定理由（证明层）→ 确定生效方式（实现层）。任何一层缺失，其余三层的成果都不构成执行控制。 原稿反复论证的"合法路径也可以产生错误结果"，其结构性原因正是现有系统通常只实现了其中一到两层。

〔补〕公理集合的独立性说明。 A1–A10 并非互相独立：A3 可视为 A2 与 A9 在授权环节的特例，A6 在某些实现下可由 A10 推出。本书仍将它们并列为公理，理由是工程可检查性——每一条对应一项可以在具体系统上单独核验的性质。这是选择，不是最小公理集。 若追求最小性，可压缩至六条，代价是失去逐条审计的便利。

第 3 章　对抗性完整 Adversarial Completeness

题记：安全功能说明系统拥有什么；安全命题说明什么仍然不能发生。

3.1 完整性命题

3.1.1 三项非蕴含关系

执行控制机制的存在，不等于该机制在对抗条件下成立。三种常见的等同关系均不成立。

其一，无缺陷不等于安全。 缺陷指实现偏离规格。一个零缺陷的系统仍可能被攻破，因为其规格本身可能未覆盖某类攻击路径。测试与形式化验证提高的是实现对规格的忠实度，不提高规格对威胁的覆盖度。

其二，正确运行不等于边界成立。 系统在预期输入下产生预期输出，只说明它在设计场景中工作。边界是否成立，取决于系统在非预期输入、组件失效与主体恶意时的行为，而这些状态通常不出现在功能测试的输入集中。

其三，局部安全不等于整体安全。 这是命题 P1.1 在安全域中的重述：每个组件满足自身安全规格，不蕴含链的端到端安全命题成立。跨组件的转换关系不属于任何单个组件的规格。

定义 D3.1.1（对抗性完整 / Adversarial Completeness） 在明确声明的威胁模型与故障模型之下，系统的关键执行约束仍然成立的性质。其成立须同时明确：威胁模型的边界、固定安全底线的内容、允许失效的组件集合、不得同时失效的信任集合、失效时系统进入的状态、必须拒绝执行的情形、以及可被独立验证的结论。

定义中"明确声明"是实质要求。对抗性完整不主张"无人能够攻破本系统"——不存在可抵抗无限资源、任意物理接触与全部攻击面的系统。它主张的是一个有条件、可证伪的命题：在已声明的模型内，即使部分组件被攻陷，关键约束不被绕过。声明边界是该性质的组成部分，而非其免责声明。

3.1.2 从安全功能到安全命题

安全能力常以功能清单表达：多因素认证、多重签名、加密传输、硬件密钥、审批流程、风险检测、审计留痕。功能清单说明系统拥有什么，不说明在什么条件下什么事情不能发生，因而不可被证伪。

对抗性完整要求把安全表述为命题。命题的形式是"即使 X，仍然不能 Y"：

表 3-1　安全命题示例

每一条命题都指定了被假定失守的部分，以及在该前提下仍须保持的结论。这一形式使安全主张可被攻击性测试直接检验：构造条件 X，观察 Y 是否发生。

命题 P3.1（可证伪性要求） 不指明失守前提的安全主张不可被证伪，因而不构成对抗性完整的证据。

由此得到本章的方法论立场：声明不是证明。 系统具备某项机制，与该机制在攻陷条件下仍然生效，是两个独立的问题，后者须单独论证。

3.2 威胁分类学 EX-STRIDE

3.2.1 分类维度的选择

传统威胁建模以 STRIDE 为代表，其分类维度面向数据与身份：仿冒、篡改、抵赖、信息泄露、拒绝服务、权限提升。该维度适配的问题域是"数据与访问的安全"，与执行控制的问题域不重合——执行缝隙的成因是转换关系的断裂（D1.3.1），而转换关系不出现在 STRIDE 的任一类别中。

一种直觉的替代做法是按威胁主体分类：AI、管理员、内部成员、供应链、设备、网络。原稿采用该组织方式，其优点是直观，缺点是不可闭合——主体集合随技术演进持续扩张，任何枚举都会过时。

本书改按受损环节分类。环节由判定函数的参数集合决定，而参数集合是有限且固定的：I、x、P、K、Ev、cap、Γ 本身。因此按环节分类可以闭合：任何攻击若要改变执行结果，必须作用于其中至少一项。主体信息不丢失，它降级为每一类下的"典型来源"。

3.2.2 分类矩阵

表 3-2　EX-STRIDE 威胁分类矩阵

矩阵的使用方式是逐列而非逐行：对一个具体系统，逐一检查每个环节是否存在未被覆盖的攻击类，而非枚举已知攻击手法。手法会更新，环节不会。

3.2.3 故障与攻击的同一处置

组件失效与恶意攻击在成因上不同，在判定输入上可能完全相同：一个因网络分区而无法获取的证据，与一个被攻击者阻断的证据，在 Γ 看来都是 σ(e) = MISSING。

命题 P3.2（故障与攻击的判定等价） 若 Γ 无法区分某一输入状态由故障还是攻击导致，则对该状态的处置必须按攻击假设执行。按故障假设放宽处置，等价于向攻击者提供一条可主动构造的绕过路径。

P3.2 排除了一类常见设计——“服务异常时跳过检查”。异常是攻击者可以制造的条件，因此异常路径上的宽松处置就是攻击面本身。

3.3 四态语义与状态机

3.3.1 四种非成立状态

公理 A8 规定证据状态 σ(e) ∈ {VALID, UNKNOWN, MISSING, EXPIRED, CONFLICT}。四种非 VALID 状态的成因彼此独立：

• UNKNOWN：证据已提交，但系统无法完成验证。系统不知道该事实是否成立。
• MISSING：判定所需的证据未提交。系统缺少作出判断的输入。
• EXPIRED：证据曾经成立，其有效期已过。系统持有的是历史事实而非当前事实。
• CONFLICT：存在与之矛盾的同类证据。系统同时持有两个不能同时为真的断言。

图 3-1　证据状态转移

#mermaid-svg-9JwRQciybb1PR0hr{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;fill:#333;}@keyframes edge-animation-frame{from{stroke-dashoffset:0;}}@keyframes dash{to{stroke-dashoffset:0;}}#mermaid-svg-9JwRQciybb1PR0hr .edge-animation-slow{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 50s linear infinite;stroke-linecap:round;}#mermaid-svg-9JwRQciybb1PR0hr .edge-animation-fast{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 20s linear infinite;stroke-linecap:round;}#mermaid-svg-9JwRQciybb1PR0hr .error-icon{fill:#552222;}#mermaid-svg-9JwRQciybb1PR0hr .error-text{fill:#552222;stroke:#552222;}#mermaid-svg-9JwRQciybb1PR0hr .edge-thickness-normal{stroke-width:1px;}#mermaid-svg-9JwRQciybb1PR0hr .edge-thickness-thick{stroke-width:3.5px;}#mermaid-svg-9JwRQciybb1PR0hr .edge-pattern-solid{stroke-dasharray:0;}#mermaid-svg-9JwRQciybb1PR0hr .edge-thickness-invisible{stroke-width:0;fill:none;}#mermaid-svg-9JwRQciybb1PR0hr .edge-pattern-dashed{stroke-dasharray:3;}#mermaid-svg-9JwRQciybb1PR0hr .edge-pattern-dotted{stroke-dasharray:2;}#mermaid-svg-9JwRQciybb1PR0hr .marker{fill:#333333;stroke:#333333;}#mermaid-svg-9JwRQciybb1PR0hr .marker.cross{stroke:#333333;}#mermaid-svg-9JwRQciybb1PR0hr svg{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;}#mermaid-svg-9JwRQciybb1PR0hr p{margin:0;}#mermaid-svg-9JwRQciybb1PR0hr defs #statediagram-barbEnd{fill:#333333;stroke:#333333;}#mermaid-svg-9JwRQciybb1PR0hr g.stateGroup text{fill:#9370DB;stroke:none;font-size:10px;}#mermaid-svg-9JwRQciybb1PR0hr g.stateGroup text{fill:#333;stroke:none;font-size:10px;}#mermaid-svg-9JwRQciybb1PR0hr g.stateGroup .state-title{font-weight:bolder;fill:#131300;}#mermaid-svg-9JwRQciybb1PR0hr g.stateGroup rect{fill:#ECECFF;stroke:#9370DB;}#mermaid-svg-9JwRQciybb1PR0hr g.stateGroup line{stroke:#333333;stroke-width:1;}#mermaid-svg-9JwRQciybb1PR0hr .transition{stroke:#333333;stroke-width:1;fill:none;}#mermaid-svg-9JwRQciybb1PR0hr .stateGroup .composit{fill:white;border-bottom:1px;}#mermaid-svg-9JwRQciybb1PR0hr .stateGroup .alt-composit{fill:#e0e0e0;border-bottom:1px;}#mermaid-svg-9JwRQciybb1PR0hr .state-note{stroke:#aaaa33;fill:#fff5ad;}#mermaid-svg-9JwRQciybb1PR0hr .state-note text{fill:black;stroke:none;font-size:10px;}#mermaid-svg-9JwRQciybb1PR0hr .stateLabel .box{stroke:none;stroke-width:0;fill:#ECECFF;opacity:0.5;}#mermaid-svg-9JwRQciybb1PR0hr .edgeLabel .label rect{fill:#ECECFF;opacity:0.5;}#mermaid-svg-9JwRQciybb1PR0hr .edgeLabel{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-9JwRQciybb1PR0hr .edgeLabel p{background-color:rgba(232,232,232, 0.8);}#mermaid-svg-9JwRQciybb1PR0hr .edgeLabel rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-9JwRQciybb1PR0hr .edgeLabel .label text{fill:#333;}#mermaid-svg-9JwRQciybb1PR0hr .label div .edgeLabel{color:#333;}#mermaid-svg-9JwRQciybb1PR0hr .stateLabel text{fill:#131300;font-size:10px;font-weight:bold;}#mermaid-svg-9JwRQciybb1PR0hr .node circle.state-start{fill:#333333;stroke:#333333;}#mermaid-svg-9JwRQciybb1PR0hr .node .fork-join{fill:#333333;stroke:#333333;}#mermaid-svg-9JwRQciybb1PR0hr .node circle.state-end{fill:#9370DB;stroke:white;stroke-width:1.5;}#mermaid-svg-9JwRQciybb1PR0hr .end-state-inner{fill:white;stroke-width:1.5;}#mermaid-svg-9JwRQciybb1PR0hr .node rect{fill:#ECECFF;stroke:#9370DB;stroke-width:1px;}#mermaid-svg-9JwRQciybb1PR0hr .node polygon{fill:#ECECFF;stroke:#9370DB;stroke-width:1px;}#mermaid-svg-9JwRQciybb1PR0hr #statediagram-barbEnd{fill:#333333;}#mermaid-svg-9JwRQciybb1PR0hr .statediagram-cluster rect{fill:#ECECFF;stroke:#9370DB;stroke-width:1px;}#mermaid-svg-9JwRQciybb1PR0hr .cluster-label,#mermaid-svg-9JwRQciybb1PR0hr .nodeLabel{color:#131300;}#mermaid-svg-9JwRQciybb1PR0hr .statediagram-cluster rect.outer{rx:5px;ry:5px;}#mermaid-svg-9JwRQciybb1PR0hr .statediagram-state .divider{stroke:#9370DB;}#mermaid-svg-9JwRQciybb1PR0hr .statediagram-state .title-state{rx:5px;ry:5px;}#mermaid-svg-9JwRQciybb1PR0hr .statediagram-cluster.statediagram-cluster .inner{fill:white;}#mermaid-svg-9JwRQciybb1PR0hr .statediagram-cluster.statediagram-cluster-alt .inner{fill:#f0f0f0;}#mermaid-svg-9JwRQciybb1PR0hr .statediagram-cluster .inner{rx:0;ry:0;}#mermaid-svg-9JwRQciybb1PR0hr .statediagram-state rect.basic{rx:5px;ry:5px;}#mermaid-svg-9JwRQciybb1PR0hr .statediagram-state rect.divider{stroke-dasharray:10,10;fill:#f0f0f0;}#mermaid-svg-9JwRQciybb1PR0hr .note-edge{stroke-dasharray:5;}#mermaid-svg-9JwRQciybb1PR0hr .statediagram-note rect{fill:#fff5ad;stroke:#aaaa33;stroke-width:1px;rx:0;ry:0;}#mermaid-svg-9JwRQciybb1PR0hr .statediagram-note rect{fill:#fff5ad;stroke:#aaaa33;stroke-width:1px;rx:0;ry:0;}#mermaid-svg-9JwRQciybb1PR0hr .statediagram-note text{fill:black;}#mermaid-svg-9JwRQciybb1PR0hr .statediagram-note .nodeLabel{color:black;}#mermaid-svg-9JwRQciybb1PR0hr .statediagram .edgeLabel{color:red;}#mermaid-svg-9JwRQciybb1PR0hr #dependencyStart,#mermaid-svg-9JwRQciybb1PR0hr #dependencyEnd{fill:#333333;stroke:#333333;stroke-width:1;}#mermaid-svg-9JwRQciybb1PR0hr .statediagramTitleText{text-anchor:middle;font-size:18px;fill:#333;}#mermaid-svg-9JwRQciybb1PR0hr :root{–mermaid-font-family:\”trebuchet ms\”,verdana,arial,sans-serif;}

未提交

已提交，验证未完成

来源与签名校验通过

补充提交并校验通过

t 超出有效期

出现矛盾的同类证据

重新签发并校验

冲突源被独立裁定失效

参与判定证明 π

MISSING

UNKNOWN

VALID

EXPIRED

CONFLICT

ALLOW_ELIGIBLE

DENY

SAFE_MODE

CONFLICT 单独指向 SAFE_MODE 而非 DENY，是因为矛盾证据意味着系统对当前状态的认知本身不可靠。此时不仅本次执行不应放行，同类执行的判定前提也已存疑，故须进入受限状态而非仅拒绝单次请求。

3.3.2 不可压缩性

一种常见实现将上述四态映射为布尔值：σ(e) = VALID 记为 true，其余记为 false。该映射在放行判定上无损——四种状态均不产生 ALLOW——但在恢复路径上有损。

表 3-3　四态对应的处置差异

命题 P3.3（四态不可压缩） 从四态到布尔值的映射丢失恢复路径信息。在丢失该信息的系统中，所有非放行结果只能表述为"拒绝"，运维方无法确定应由谁采取何种动作，其后果是拒绝在实践中被绕过而非被解决。

P3.3 的工程含义常被低估：一个无法说明拒绝原因的边界，会因运维不可行而被要求关闭，最终以配置开关的形式失去效力。可解释性不是边界的附加特性，而是其存活条件。

3.3.3 未知不可被上层解释消解

上层组件常具备将未知转化为结论的能力：模型可以给出合理推测，业务系统可以采用默认值，运维流程可以按经验判断。这些能力在信息处理中有价值，在边界判定中不可采纳。

理由由公理 A7 直接给出：上层提交的是证据，不是结论。一个"根据历史推断该账户合规"的判断，其本身是一项待证事实，不是对合规性的证明。若允许该判断替代证据，则任何缺失都可通过增加一层推断消解，A8 的保守闭合失效。

Unknown 的价值恰在于它是一个不可被语言消解的状态。它把"系统不知道"这一事实保留在判定链上，使其无法被措辞更自信的表述覆盖。

3.4 保守默认与 Fail Secure

3.4.1 Fail Open 的结构性吸引力

用户不倾向于接受拒绝，企业不倾向于接受流程中断，自动化平台以任务完成率为指标，设备系统以持续运行为目标。这些压力共同作用于工程决策，产生一组常见设计：网络断开时使用缓存，证据缺失时采用默认值，服务异常时跳过检查，风控不可用时继续交易，硬件故障时切换软件执行，审批超时时沿用旧授权。

这些设计的共同结构是：系统为了继续工作，让保护机制自动退化。 其危险不在于系统进入了明确的不安全模式——那是可见的、可审计的；而在于退化是静默的，系统在外观上仍在正常运行。

3.4.2 代价不对称

是否采用保守默认，取决于两类错误的代价比较。

表 3-4　误拒绝与误放行的代价结构

在可回滚的数字操作中，两类代价量级接近，可用性优先是合理选择。在不可逆的现实执行中，代价高度不对称：误拒绝的成本有界且可预测，误放行的成本无界且不可回收。

工程约定 E3.1（保守默认） 对不可逆执行，判定组件的默认输出为非 ALLOW。该约定的代价是可用性下降，其依据是表 3-4 的代价不对称性，而非逻辑必然。在可回滚场景中，本书不主张采用该约定。

明确标注为工程约定而非公理，是因为其正当性依赖于场景的不可逆性这一经验前提。若某系统的全部动作皆可无成本回滚，E3.1 不适用。

3.4.3 默认拒绝不等于永久拒绝

Fail Secure 的含义是"在证明恢复之前不继续执行"，不是"遇到异常即永久停止"。恢复过程本身被纳入控制：请求新证据、重新采集状态、重新审批、切换独立验证通道、进入受限模式、缩小执行范围、要求现场人工确认、执行预定义的恢复协议。

Safe Mode 是该受限状态的具体形式，它不是关机，而是一组预先定义的能力子集。典型配置包括：禁止新的高风险执行、只读不写、只允许撤销不允许新增、只允许本地不允许远程、限制金额与速率、要求额外独立证据、要求现场确认，同时保留必要的通信与审计能力。其设计目标可表述为一句：系统失去完整能力时，不失去边界。

3.4.4 Fail Secure 是架构属性

若 Fail Secure 表现为一项配置，它可被关闭；若它仅由上层软件实现，它可被绕过；若安全系统失效后业务系统仍能直接调用执行能力，则系统的实际行为是 Fail Open，无论文档如何描述。

保守默认须体现于架构：最终执行能力由边界独占（A10）；边界失联时不存在替代路径；必要证据缺失时不释放能力；上层无法自行构造 ALLOW；恢复须重新建立完整证明。

由此可得对"降级"的约束。功能降级与安全降级性质不同：前者减少能力，后者不得取消底线。云服务不可用时，系统可以停止高风险远程执行、保留本地只读、降低额度、增加现场确认；但不能切换为"云端验证失败，故由本地管理员直接执行"。后者不是降级，是绕过。

命题 P3.4（降级的界限） 任何降级路径若使系统在降级后能够执行降级前被 K 禁止的动作，则该路径是一条绕过路径，而非降级设计。

3.4.5 紧急机制

多数系统为异常情形保留 Break Glass 机制，这在现实运营中往往必要。但紧急机制是最易被滥用的路径：若"紧急"可由单一管理员声明，紧急模式可关闭全部验证，且事后缺少独立证据，则攻击者的目标简化为获取紧急权限。

对抗性完整不要求取消紧急操作，要求的是对其加以约束：范围明确、触发条件可证明、权限最小化、时限有限、操作不可隐藏、须独立记录，且部分固定底线在紧急模式下仍不可关闭。紧急情况可以改变策略 P，不应使宪法 K 消失。

3.5 验证方法与残余风险

对抗性完整须以可执行的验证活动支撑，其最小集合包含五项：威胁模型（明确声明假定的攻击者能力与允许失效的组件）；失败矩阵（枚举关键失败方式及其对应处置，见附录 C）；不变量（在任何输入与状态下须保持为真的性质，作为自动化测试的断言）；对抗测试（按表 3-2 逐环节构造攻击条件，验证表 3-1 的安全命题）；控制失效的证明方式（预先定义如何检测边界已被绕过，而非依赖事后发现）。

本书不覆盖以下情形，须在采用其结论时另行处理：物理接触无限制且时间无限的攻击者；边界硬件在制造环节即被植入后门且无远程认证手段的情形；全部独立证据来源同时被同一主体控制的情形；以及执行动作本身可逆而使 E3.1 不适用的场景。明确列出未覆盖范围是 D3.1.1 的组成部分——未声明边界的完整性主张，不构成完整性。

第 4 章　EBL 执行边界语言

题记：边界语言的价值不在于什么都能做，而在于它做不到不该做的事。

4.1 现有表达形式的不足

4.1.1 边界语言的五项要求

第 2、3 章的结论对表达执行边界规则的形式提出了具体要求。任何候选表达形式须同时满足：

以这五项为判据，考察现有的五类表达形式。

表 4-1　现有表达形式与边界语言要求的对照

前两类的缺口在于表达能力不足，后两类的缺口在于表达能力过剩。这一对比给出了 EBL 的设计定位。

4.1.2 非图灵完备是要求而非缺陷

图灵完备意味着语言可表达任意可计算过程。对通用开发这是能力，对执行边界这是负担：无界循环、任意递归、动态内存增长、不可预测的终止时间与难以静态分析的控制流，使系统无法预先保证某条规则一定终止，也无法计算其资源上界。

而边界须知道：规则一定结束、最坏步骤数、内存上界、不访问未声明数据、裁决中不产生副作用。

命题 P4.1（表达能力的上界） 满足要求 2 与要求 3 的语言不能是图灵完备的。因此 EBL 主动放弃图灵完备不是能力妥协，而是要求的直接推论。

EBL 因此在语言谱系上更接近防火墙规则、包过滤语言、有限状态机与声明式约束语言，而非通用程序设计语言。它不需要回答任意计算问题，只需回答一个有限问题：在给定规则与完整输入下，本次候选执行是否允许跨越边界。

4.1.3 自然语言不能作为最终规则

一种自然的设想是：既然模型能够理解自然语言，安全策略也可直接以自然语言书写。该设想在规则生成环节可行，在规则裁决环节不可行。

理由是要求 1。自然语言规则的结论依赖解释，而解释依赖上下文、措辞与解释者状态。同一条"大额转账需要额外审批"，在不同上下文中对"大额"的判定可以不同；同一条规则由不同模型或同一模型在不同提示下求值，可得不同结论。裁决因此不可复现，π 无法重放，A8 所要求的完整证明失去意义。

可行的分工是：自然语言用于表达意图与起草规则，EBL 用于固化与裁决规则。模型可以把业务描述转写为 EBL 规则供人审阅，但不参与规则的求值。

工程约定 E4.1（生成与裁决分离） 允许模型生成 EBL 规则，不允许模型充当 EBL 求值器。生成结果须经人工或确定性工具审查后方可部署。该约定的代价是规则变更速度下降。

4.2 执行边界的性质

4.2.1 定义

定义 D4.2.1（执行边界 / Execution Boundary） 候选执行须获得放行才能跨越、且跨越后动作即进入现实的单向控制点。执行边界由两部分构成：一组可求值的规则，以及对某项必要能力 cap 的独占。

定义强调"两部分构成"，因为二者缺一时边界均不成立。只有规则而不独占能力，规则可被绕过（违反 A10）；只独占能力而无规则，则能力的释放缺乏判据，边界退化为一个开关。

4.2.2 六项性质

其一，边界不是配置。 配置描述系统如何工作，边界描述什么不能发生。二者的区别体现在变更路径上：配置由运营流程变更，边界的固定部分不应经由同一路径变更（E2.4）。若边界与配置共用变更通道，则获得配置权即获得关闭边界的能力。

其二，边界控制的是候选执行，不是意图。 边界的输入是已完全具化的 x，而非其上游描述。这是公理 A3 与命题 P2.1 的共同结论：控制点若不覆盖最终对象，则不构成边界。

其三，边界必须看到最终对象及其绑定关系。 仅判断操作类型不足以裁决。边界须验证 x 与 I、P、Approval、Ev 之间的关系是否成立，且对象变化须使既有证明失效（A9）。

其四，边界不创造行动。 边界只对候选执行作出放行或不放行的判断，不生成替代方案、不修正参数、不补全缺失字段。补全属于上层职责，边界执行补全即意味着它同时是生成方与裁决方，违反 A6。

其五，边界是单向门。 通过边界的方向只有一个：从候选执行到现实。不存在"先执行后补证明"的反向路径，也不存在在拒绝后由上层重试消解拒绝的机制。

图 4-1　边界的单向性

#mermaid-svg-jthjZj105hefzzz3{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;fill:#333;}@keyframes edge-animation-frame{from{stroke-dashoffset:0;}}@keyframes dash{to{stroke-dashoffset:0;}}#mermaid-svg-jthjZj105hefzzz3 .edge-animation-slow{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 50s linear infinite;stroke-linecap:round;}#mermaid-svg-jthjZj105hefzzz3 .edge-animation-fast{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 20s linear infinite;stroke-linecap:round;}#mermaid-svg-jthjZj105hefzzz3 .error-icon{fill:#552222;}#mermaid-svg-jthjZj105hefzzz3 .error-text{fill:#552222;stroke:#552222;}#mermaid-svg-jthjZj105hefzzz3 .edge-thickness-normal{stroke-width:1px;}#mermaid-svg-jthjZj105hefzzz3 .edge-thickness-thick{stroke-width:3.5px;}#mermaid-svg-jthjZj105hefzzz3 .edge-pattern-solid{stroke-dasharray:0;}#mermaid-svg-jthjZj105hefzzz3 .edge-thickness-invisible{stroke-width:0;fill:none;}#mermaid-svg-jthjZj105hefzzz3 .edge-pattern-dashed{stroke-dasharray:3;}#mermaid-svg-jthjZj105hefzzz3 .edge-pattern-dotted{stroke-dasharray:2;}#mermaid-svg-jthjZj105hefzzz3 .marker{fill:#333333;stroke:#333333;}#mermaid-svg-jthjZj105hefzzz3 .marker.cross{stroke:#333333;}#mermaid-svg-jthjZj105hefzzz3 svg{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;}#mermaid-svg-jthjZj105hefzzz3 p{margin:0;}#mermaid-svg-jthjZj105hefzzz3 .label{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;color:#333;}#mermaid-svg-jthjZj105hefzzz3 .cluster-label text{fill:#333;}#mermaid-svg-jthjZj105hefzzz3 .cluster-label span{color:#333;}#mermaid-svg-jthjZj105hefzzz3 .cluster-label span p{background-color:transparent;}#mermaid-svg-jthjZj105hefzzz3 .label text,#mermaid-svg-jthjZj105hefzzz3 span{fill:#333;color:#333;}#mermaid-svg-jthjZj105hefzzz3 .node rect,#mermaid-svg-jthjZj105hefzzz3 .node circle,#mermaid-svg-jthjZj105hefzzz3 .node ellipse,#mermaid-svg-jthjZj105hefzzz3 .node polygon,#mermaid-svg-jthjZj105hefzzz3 .node path{fill:#ECECFF;stroke:#9370DB;stroke-width:1px;}#mermaid-svg-jthjZj105hefzzz3 .rough-node .label text,#mermaid-svg-jthjZj105hefzzz3 .node .label text,#mermaid-svg-jthjZj105hefzzz3 .image-shape .label,#mermaid-svg-jthjZj105hefzzz3 .icon-shape .label{text-anchor:middle;}#mermaid-svg-jthjZj105hefzzz3 .node .katex path{fill:#000;stroke:#000;stroke-width:1px;}#mermaid-svg-jthjZj105hefzzz3 .rough-node .label,#mermaid-svg-jthjZj105hefzzz3 .node .label,#mermaid-svg-jthjZj105hefzzz3 .image-shape .label,#mermaid-svg-jthjZj105hefzzz3 .icon-shape .label{text-align:center;}#mermaid-svg-jthjZj105hefzzz3 .node.clickable{cursor:pointer;}#mermaid-svg-jthjZj105hefzzz3 .root .anchor path{fill:#333333!important;stroke-width:0;stroke:#333333;}#mermaid-svg-jthjZj105hefzzz3 .arrowheadPath{fill:#333333;}#mermaid-svg-jthjZj105hefzzz3 .edgePath .path{stroke:#333333;stroke-width:2.0px;}#mermaid-svg-jthjZj105hefzzz3 .flowchart-link{stroke:#333333;fill:none;}#mermaid-svg-jthjZj105hefzzz3 .edgeLabel{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-jthjZj105hefzzz3 .edgeLabel p{background-color:rgba(232,232,232, 0.8);}#mermaid-svg-jthjZj105hefzzz3 .edgeLabel rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-jthjZj105hefzzz3 .labelBkg{background-color:rgba(232, 232, 232, 0.5);}#mermaid-svg-jthjZj105hefzzz3 .cluster rect{fill:#ffffde;stroke:#aaaa33;stroke-width:1px;}#mermaid-svg-jthjZj105hefzzz3 .cluster text{fill:#333;}#mermaid-svg-jthjZj105hefzzz3 .cluster span{color:#333;}#mermaid-svg-jthjZj105hefzzz3 div.mermaidTooltip{position:absolute;text-align:center;max-width:200px;padding:2px;font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:12px;background:hsl(80, 100%, 96.2745098039%);border:1px solid #aaaa33;border-radius:2px;pointer-events:none;z-index:100;}#mermaid-svg-jthjZj105hefzzz3 .flowchartTitleText{text-anchor:middle;font-size:18px;fill:#333;}#mermaid-svg-jthjZj105hefzzz3 rect.text{fill:none;stroke-width:0;}#mermaid-svg-jthjZj105hefzzz3 .icon-shape,#mermaid-svg-jthjZj105hefzzz3 .image-shape{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-jthjZj105hefzzz3 .icon-shape p,#mermaid-svg-jthjZj105hefzzz3 .image-shape p{background-color:rgba(232,232,232, 0.8);padding:2px;}#mermaid-svg-jthjZj105hefzzz3 .icon-shape .label rect,#mermaid-svg-jthjZj105hefzzz3 .image-shape .label rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-jthjZj105hefzzz3 .label-icon{display:inline-block;height:1em;overflow:visible;vertical-align:-0.125em;}#mermaid-svg-jthjZj105hefzzz3 .node .label-icon path{fill:currentColor;stroke:revert;stroke-width:revert;}#mermaid-svg-jthjZj105hefzzz3 :root{–mermaid-font-family:\”trebuchet ms\”,verdana,arial,sans-serif;}

提交

d = ALLOW，释放 cap

d ≠ ALLOW

补充证据后重新提交，重新裁决

不存在此方向

上层：生成 x、收集 Ev

执行边界规则 + cap 独占

现实动作

返回 π 与失败语义

图中虚线标记的反向路径不存在：现实动作一旦发生，边界不再具备控制力。这决定了边界必须位于动作之前而非之后，也决定了审计不能替代边界（表 2-1）。

其六，规则组合，不互相覆盖。 复杂系统需要多类规则：金额限制、时间窗口、设备状态、审批数量、角色独立性、地理约束、风险约束、对象绑定、固定硬限制。这些规则来自不同层级，其组合方式必须被明确定义。

关键约束是：后写的业务规则不得覆盖固定底线。若宿主系统规定"设备状态未知时不得 ALLOW"，则任何业务规则不得写成"金额较小时，设备状态未知也可继续"。允许此类覆盖，等于把策略语言变成关闭边界的工具。

命题 P4.2（组合律） EBL 规则的组合运算为合取。任意规则集合 R 的放行集满足 ALLOW(R ∪ {r}) ⊆ ALLOW(R)——添加规则只能收缩放行范围，不能扩大。该性质是公理 A4 单调收缩性在语言层的表达。

P4.2 的实现含义是：EBL 不提供"例外"「优先级覆盖」或「后规则胜出」等语义。需要放宽时，正确做法是修改被违反的那条规则本身并留下变更记录，而非叠加一条更宽松的规则。这一设计使规则集的实际效力可由静态分析确定，而无需模拟求值顺序。

由性质六直接引出一个问题：既然规则只能收缩，那么什么规则不可被任何后续规则收缩到失效，又由谁规定？这是宪法的职责。

4.3 Constitution

4.3.1 为什么边界语言需要宪法

P 与 K 的区分在公理 A4 中已经确立，本节说明其在语言层的实现方式。

若一门策略语言不区分二者，则语言的全部表达能力都可用于修改任意规则，包括那些用于约束修改行为本身的规则。此时安全性等价于配置正确性，而配置正确性依赖于每一次变更都不出错——这是一个不可验证的前提。管理员权限、配置系统漏洞、供应链污染中的任何一项，都足以使其失效。

定义 D4.3.1（宪法 / Constitution K） 在 EBL 中具有特殊地位的规则集合，满足：不可由 P 层规则关闭、削弱或旁路；其变更须经由与常规策略不同的路径；且其内容同时定义 EBL 的语言能力边界。

4.3.2 宪法的十条原则

一份完整宪法须经长期设计与形式化验证。以下十条由第 1 至第 3 章的结论直接推出，构成最小集合。

表 4-2　EBL 宪法条款及其公理依据

十条中，C1 至 C3 约束语言与运行时的形态，C4 至 C8 约束判定的语义，C9 约束资源行为，C10 约束二者的关系。C10 是使前九条成立的元条款——没有 C10，其余九条均可被一条业务规则关闭。

4.3.3 宪法先于语法

通用语言的设计顺序通常是先定义语法与语义，再讨论安全限制，限制以静态检查或运行时沙箱的形式附加于语言之上。EBL 采用相反顺序：先确定宪法，再由宪法决定语言可以具备哪些构造。

该顺序的后果是具体的。因 C9 要求必然终止，语言不提供无界循环与任意递归，只提供对已声明集合的有界遍历；因 C2 要求无副作用，语言不提供外部调用构造；因 C3 要求确定性，语言不提供随机数、当前时间的隐式读取（时间须作为显式输入 t）与未声明变量访问；因 C4 要求四态保留，语言的条件求值不返回布尔值，而返回带状态的三值或多值结果；因 C10 要求不可覆盖，语言不提供规则优先级与例外语法。

由此，"该语言不能做某事"不是实现层面的限制，而是语法层面不存在对应构造。这一区别在安全上是实质性的：静态检查可被绕过或配置放宽，不存在的语法构造不能被使用。

4.3.4 宪法是 Runtime 的验证标准

宪法的第二重身份是 Runtime 实现的一致性规范。多个 Runtime 实现（不同硬件平台、不同语言、不同厂商）须对同一规则与同一输入产生同一结论，否则规则的语义随部署环境漂移，跨系统的安全命题不再成立。

因此宪法须配套一组一致性测试：对每一条 C 款，给出可执行的检验用例——例如针对 C4，构造一份 EXPIRED 证据并验证任何实现均不产生 ALLOW；针对 C10，构造一条试图放宽固定限制的业务规则并验证其被拒绝加载而非被静默忽略。

〔补〕关于拒绝加载与静默忽略的区别。 C10 的实现有两种可能：一是加载阶段拒绝违规规则并报错，二是运行阶段忽略其放宽效果。二者在放行结果上等价，在运维后果上不等价——静默忽略会使规则作者相信规则已生效，从而在其他环节据此作出错误假设。本书主张前者：违反宪法的规则不应被部署，而非被部署后不起作用。

4.4 Runtime

题记：Runtime 不创造信任，它只验证证明。

4.4.1 裁决与执行的分离

Runtime 是判定函数 Γ 的实现。其首要架构性质是：Runtime 裁决，但不执行。

分离的理由由公理 A6 给出，但在 Runtime 这一层有更具体的含义。若同一组件既求值规则又发起动作，则该组件的任何缺陷——逻辑错误、内存破坏、被注入的控制流——都可能在绕过求值的情况下直接触发动作。分离之后，即使 Runtime 被完全攻陷，其可造成的最大损害是输出一个错误的 d = ALLOW；而该输出仍须经由持有 cap 的边界执行，边界可对其施加独立的固定限制（宪法 C2 与 A10 的组合）。

这一结构可概括为职责的双重限定：Runtime 是裁判，不是运动员——它不参与生成候选执行，不修正参数，不补全缺失字段，不在裁决过程中改变世界状态。

4.4.2 输入封闭

Γ 的封闭性要求 Runtime 只读取参数中显式声明的输入。违反该性质的常见形式包括：读取当前系统时间而非接收 t 作为输入；在求值中查询外部服务获取"最新状态"；访问未在规则中声明的上下文字段；依赖进程内的缓存或历史裁决结果。

图 4-2　Runtime 的输入封闭与输出结构

#mermaid-svg-Sysg9SGLwvfJd4eN{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;fill:#333;}@keyframes edge-animation-frame{from{stroke-dashoffset:0;}}@keyframes dash{to{stroke-dashoffset:0;}}#mermaid-svg-Sysg9SGLwvfJd4eN .edge-animation-slow{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 50s linear infinite;stroke-linecap:round;}#mermaid-svg-Sysg9SGLwvfJd4eN .edge-animation-fast{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 20s linear infinite;stroke-linecap:round;}#mermaid-svg-Sysg9SGLwvfJd4eN .error-icon{fill:#552222;}#mermaid-svg-Sysg9SGLwvfJd4eN .error-text{fill:#552222;stroke:#552222;}#mermaid-svg-Sysg9SGLwvfJd4eN .edge-thickness-normal{stroke-width:1px;}#mermaid-svg-Sysg9SGLwvfJd4eN .edge-thickness-thick{stroke-width:3.5px;}#mermaid-svg-Sysg9SGLwvfJd4eN .edge-pattern-solid{stroke-dasharray:0;}#mermaid-svg-Sysg9SGLwvfJd4eN .edge-thickness-invisible{stroke-width:0;fill:none;}#mermaid-svg-Sysg9SGLwvfJd4eN .edge-pattern-dashed{stroke-dasharray:3;}#mermaid-svg-Sysg9SGLwvfJd4eN .edge-pattern-dotted{stroke-dasharray:2;}#mermaid-svg-Sysg9SGLwvfJd4eN .marker{fill:#333333;stroke:#333333;}#mermaid-svg-Sysg9SGLwvfJd4eN .marker.cross{stroke:#333333;}#mermaid-svg-Sysg9SGLwvfJd4eN svg{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;}#mermaid-svg-Sysg9SGLwvfJd4eN p{margin:0;}#mermaid-svg-Sysg9SGLwvfJd4eN .label{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;color:#333;}#mermaid-svg-Sysg9SGLwvfJd4eN .cluster-label text{fill:#333;}#mermaid-svg-Sysg9SGLwvfJd4eN .cluster-label span{color:#333;}#mermaid-svg-Sysg9SGLwvfJd4eN .cluster-label span p{background-color:transparent;}#mermaid-svg-Sysg9SGLwvfJd4eN .label text,#mermaid-svg-Sysg9SGLwvfJd4eN span{fill:#333;color:#333;}#mermaid-svg-Sysg9SGLwvfJd4eN .node rect,#mermaid-svg-Sysg9SGLwvfJd4eN .node circle,#mermaid-svg-Sysg9SGLwvfJd4eN .node ellipse,#mermaid-svg-Sysg9SGLwvfJd4eN .node polygon,#mermaid-svg-Sysg9SGLwvfJd4eN .node path{fill:#ECECFF;stroke:#9370DB;stroke-width:1px;}#mermaid-svg-Sysg9SGLwvfJd4eN .rough-node .label text,#mermaid-svg-Sysg9SGLwvfJd4eN .node .label text,#mermaid-svg-Sysg9SGLwvfJd4eN .image-shape .label,#mermaid-svg-Sysg9SGLwvfJd4eN .icon-shape .label{text-anchor:middle;}#mermaid-svg-Sysg9SGLwvfJd4eN .node .katex path{fill:#000;stroke:#000;stroke-width:1px;}#mermaid-svg-Sysg9SGLwvfJd4eN .rough-node .label,#mermaid-svg-Sysg9SGLwvfJd4eN .node .label,#mermaid-svg-Sysg9SGLwvfJd4eN .image-shape .label,#mermaid-svg-Sysg9SGLwvfJd4eN .icon-shape .label{text-align:center;}#mermaid-svg-Sysg9SGLwvfJd4eN .node.clickable{cursor:pointer;}#mermaid-svg-Sysg9SGLwvfJd4eN .root .anchor path{fill:#333333!important;stroke-width:0;stroke:#333333;}#mermaid-svg-Sysg9SGLwvfJd4eN .arrowheadPath{fill:#333333;}#mermaid-svg-Sysg9SGLwvfJd4eN .edgePath .path{stroke:#333333;stroke-width:2.0px;}#mermaid-svg-Sysg9SGLwvfJd4eN .flowchart-link{stroke:#333333;fill:none;}#mermaid-svg-Sysg9SGLwvfJd4eN .edgeLabel{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-Sysg9SGLwvfJd4eN .edgeLabel p{background-color:rgba(232,232,232, 0.8);}#mermaid-svg-Sysg9SGLwvfJd4eN .edgeLabel rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-Sysg9SGLwvfJd4eN .labelBkg{background-color:rgba(232, 232, 232, 0.5);}#mermaid-svg-Sysg9SGLwvfJd4eN .cluster rect{fill:#ffffde;stroke:#aaaa33;stroke-width:1px;}#mermaid-svg-Sysg9SGLwvfJd4eN .cluster text{fill:#333;}#mermaid-svg-Sysg9SGLwvfJd4eN .cluster span{color:#333;}#mermaid-svg-Sysg9SGLwvfJd4eN div.mermaidTooltip{position:absolute;text-align:center;max-width:200px;padding:2px;font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:12px;background:hsl(80, 100%, 96.2745098039%);border:1px solid #aaaa33;border-radius:2px;pointer-events:none;z-index:100;}#mermaid-svg-Sysg9SGLwvfJd4eN .flowchartTitleText{text-anchor:middle;font-size:18px;fill:#333;}#mermaid-svg-Sysg9SGLwvfJd4eN rect.text{fill:none;stroke-width:0;}#mermaid-svg-Sysg9SGLwvfJd4eN .icon-shape,#mermaid-svg-Sysg9SGLwvfJd4eN .image-shape{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-Sysg9SGLwvfJd4eN .icon-shape p,#mermaid-svg-Sysg9SGLwvfJd4eN .image-shape p{background-color:rgba(232,232,232, 0.8);padding:2px;}#mermaid-svg-Sysg9SGLwvfJd4eN .icon-shape .label rect,#mermaid-svg-Sysg9SGLwvfJd4eN .image-shape .label rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-Sysg9SGLwvfJd4eN .label-icon{display:inline-block;height:1em;overflow:visible;vertical-align:-0.125em;}#mermaid-svg-Sysg9SGLwvfJd4eN .node .label-icon path{fill:currentColor;stroke:revert;stroke-width:revert;}#mermaid-svg-Sysg9SGLwvfJd4eN :root{–mermaid-font-family:\”trebuchet ms\”,verdana,arial,sans-serif;}

禁止

输出

d ∈ {ALLOW, DENY, SAFE_MODE}

π：证据图 + 求值路径 + 规则版本

Runtime

规则求值无副作用・有界步骤

显式输入（封闭集）

I

x

P

K

Ev

Ctx

t

外部服务 / 系统时钟 / 隐式缓存

封闭性的直接收益是可重放：给定同一输入集，任何时刻、任何实现均可重新求值并得到同一结论。若 Runtime 读取了输入集之外的数据，π 便不足以复现裁决，审计失去依据。

由封闭性还可推出对隐式权力的排除。Runtime 不应持有任何"在特殊情况下可以放行"的内建能力：没有内置的管理员例外，没有调试模式下的旁路，没有超时后的默认通过。任何此类能力都构成一条不在规则集中、因而不可被静态分析发现的放行路径。

4.4.3 输出结构

Runtime 的输出不是布尔值。依据宪法 C4 与 C5，输出须包含决策 d 与判定证明 π，且在非放行的情形下须指明失败语义（MISSING / UNKNOWN / EXPIRED / CONFLICT）与失效位置。

命题 P4.3（输出的可操作性） 若 Runtime 的非放行输出不指明失效位置与失败语义，则调用方无法区分应当补充证据、修复验证通道、重新签发还是等待独立裁定。此时拒绝不可操作，系统将趋向于通过关闭检查而非解决问题来恢复可用性。

P4.3 与 P3.3 是同一论证在不同层次的表述：可解释性是边界的存活条件。Runtime 的输出结构是该条件在实现层的承担者。

4.4.4 资源约束

宪法 C9 要求策略必然终止且资源可计算。Runtime 须据此对每次求值施加可预先计算的上界：最大求值步骤、最大内存、最大嵌套深度、最大证据数量、最大规则复杂度。超出上界时，正确行为不是延长等待，而是按 SAFE_MODE 处置——资源耗尽是一种系统无法完成证明的状态，依 A8 不产生 ALLOW。

该约束同时构成一条抗拒绝服务的性质：由于上界可预先计算，攻击者无法通过构造复杂输入使边界陷入不可预测的长时间求值，从而无法以延迟为手段制造可用性压力（威胁类 X8）。

4.4.5 可移植性与语义不漂移

执行边界会部署于差异极大的环境：服务端进程、可信执行环境、独立协处理器、微控制器。Runtime 因此须可移植。但可移植性带来一项风险：同一规则在不同实现上产生不同结论，即语义漂移。

命题 P4.4（跨实现一致性） 若两个 Runtime 实现对同一 (I, x, P, K, Ev, Ctx, t) 产生不同的 d，则以该规则集为基础的安全命题在部署环境的并集上不成立。

因此宪法须配套一致性测试套件（4.3.4），且实现须声明其所遵循的宪法版本。语义的权威来源是宪法与测试套件，而非任何一个具体实现——包括参考实现。

4.4.6 Runtime 不创造信任

一项容易产生的误解是把 Runtime 视为信任的来源：“经过 Runtime 裁决"因而"是安全的”。该表述倒置了因果。Runtime 不生产信任，它只检验上游提交的证据是否构成完整证明。若证据本身不可靠，Runtime 的 ALLOW 与其可靠性完全相同。

这一认识决定了系统的改进方向：提高边界安全性的手段，不是让 Runtime 更聪明，而是让进入 Runtime 的证据更可验证、让 cap 的独占更彻底。

4.5 Evidence 与 Proof

第 2.5 节确立了证据在控制理论层面的四项语义要求。本节处理其在语言层的落地形式，以及判定证明作为一种可交付工件的结构。

4.5.1 证据的类型化

EBL 中的证据是带类型的结构，而非字符串或布尔值。类型的作用是使"这份证据能够证明什么"成为可静态检查的性质：一份身份证明不能被用于证成设备状态，一份余额快照不能被用于证成审批完成。

定义 D4.5.1（证据类型 / Evidence Type） 一个证据类型规定：其可证成的条件集合、必需的元数据字段、来源凭据的验证方式、时间语义（时点型或区间型），以及与其他类型之间的独立性关系。

类型化的工程后果是错误前移。缺少类型时，"证据是否适用于该条件"只能在求值时判断，且判断逻辑分散在各条规则中；具备类型后，该问题在规则加载阶段即可确定，不适用的引用被拒绝加载（与 4.3.4 中〔补〕所述的处置一致）。

4.5.2 证明图

判定证明 π 的结构是一张有向图（图 2-4）：叶节点是证据，中间节点是条件与规则求值，根节点是决策。图结构而非线性日志，是因为一项条件可能由多份证据共同证成，一份证据也可能参与多项条件。

π 至少须承载六类信息：成立的规则及其版本、参与的证据及其状态、绑定关系（I ↔ x ↔ Approval）、被满足的固定约束、求值路径、以及每一份证据在判定时刻 t 的时间状态。

4.5.3 重放的三个层次

"π 可被重放"是一个需要分层理解的性质，不同层次所需的保留数据与所能验证的结论不同。

表 4-3　判定证明的重放层次

多数系统无须保留全部三层。可行的工程折中是：默认保留一致性重放所需的最小集，对高风险类别的执行保留真实性与时点重放所需的完整数据。该选择应由宪法而非业务策略规定，否则保留级别会随可用性压力被逐步降低。

工程约定 E4.2（证明保留） 证明的保留级别按执行类别在宪法中固定，不由 P 层调整。代价是存储成本上升与隐私暴露面扩大，须以类别划分而非一律最高级别来控制。

4.5.4 证明不是数据仓库

Proof 的目的是使裁决可被重新检验，不是使系统持有全部历史数据。将两者混同会产生两类问题：存储与隐私成本随执行量线性增长；以及大量与裁决无关的数据被纳入证明，使证明本身难以审计。

判据是明确的：一项数据是否进入 π，取决于它是否参与了本次判定。 参与判定的数据必须进入，未参与的数据不应进入——后者属于日志的职责范围（表 2-3）。

4.6 最小理论模型与非目标

4.6.1 六类对象

在不进入具体语法设计的前提下，EBL 的理论模型可归结为六类对象及其关系。

图 4-3　EBL 的六类对象

#mermaid-svg-Io24ioUmmF4NOgVj{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;fill:#333;}@keyframes edge-animation-frame{from{stroke-dashoffset:0;}}@keyframes dash{to{stroke-dashoffset:0;}}#mermaid-svg-Io24ioUmmF4NOgVj .edge-animation-slow{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 50s linear infinite;stroke-linecap:round;}#mermaid-svg-Io24ioUmmF4NOgVj .edge-animation-fast{stroke-dasharray:9,5!important;stroke-dashoffset:900;animation:dash 20s linear infinite;stroke-linecap:round;}#mermaid-svg-Io24ioUmmF4NOgVj .error-icon{fill:#552222;}#mermaid-svg-Io24ioUmmF4NOgVj .error-text{fill:#552222;stroke:#552222;}#mermaid-svg-Io24ioUmmF4NOgVj .edge-thickness-normal{stroke-width:1px;}#mermaid-svg-Io24ioUmmF4NOgVj .edge-thickness-thick{stroke-width:3.5px;}#mermaid-svg-Io24ioUmmF4NOgVj .edge-pattern-solid{stroke-dasharray:0;}#mermaid-svg-Io24ioUmmF4NOgVj .edge-thickness-invisible{stroke-width:0;fill:none;}#mermaid-svg-Io24ioUmmF4NOgVj .edge-pattern-dashed{stroke-dasharray:3;}#mermaid-svg-Io24ioUmmF4NOgVj .edge-pattern-dotted{stroke-dasharray:2;}#mermaid-svg-Io24ioUmmF4NOgVj .marker{fill:#333333;stroke:#333333;}#mermaid-svg-Io24ioUmmF4NOgVj .marker.cross{stroke:#333333;}#mermaid-svg-Io24ioUmmF4NOgVj svg{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:16px;}#mermaid-svg-Io24ioUmmF4NOgVj p{margin:0;}#mermaid-svg-Io24ioUmmF4NOgVj .label{font-family:\”trebuchet ms\”,verdana,arial,sans-serif;color:#333;}#mermaid-svg-Io24ioUmmF4NOgVj .cluster-label text{fill:#333;}#mermaid-svg-Io24ioUmmF4NOgVj .cluster-label span{color:#333;}#mermaid-svg-Io24ioUmmF4NOgVj .cluster-label span p{background-color:transparent;}#mermaid-svg-Io24ioUmmF4NOgVj .label text,#mermaid-svg-Io24ioUmmF4NOgVj span{fill:#333;color:#333;}#mermaid-svg-Io24ioUmmF4NOgVj .node rect,#mermaid-svg-Io24ioUmmF4NOgVj .node circle,#mermaid-svg-Io24ioUmmF4NOgVj .node ellipse,#mermaid-svg-Io24ioUmmF4NOgVj .node polygon,#mermaid-svg-Io24ioUmmF4NOgVj .node path{fill:#ECECFF;stroke:#9370DB;stroke-width:1px;}#mermaid-svg-Io24ioUmmF4NOgVj .rough-node .label text,#mermaid-svg-Io24ioUmmF4NOgVj .node .label text,#mermaid-svg-Io24ioUmmF4NOgVj .image-shape .label,#mermaid-svg-Io24ioUmmF4NOgVj .icon-shape .label{text-anchor:middle;}#mermaid-svg-Io24ioUmmF4NOgVj .node .katex path{fill:#000;stroke:#000;stroke-width:1px;}#mermaid-svg-Io24ioUmmF4NOgVj .rough-node .label,#mermaid-svg-Io24ioUmmF4NOgVj .node .label,#mermaid-svg-Io24ioUmmF4NOgVj .image-shape .label,#mermaid-svg-Io24ioUmmF4NOgVj .icon-shape .label{text-align:center;}#mermaid-svg-Io24ioUmmF4NOgVj .node.clickable{cursor:pointer;}#mermaid-svg-Io24ioUmmF4NOgVj .root .anchor path{fill:#333333!important;stroke-width:0;stroke:#333333;}#mermaid-svg-Io24ioUmmF4NOgVj .arrowheadPath{fill:#333333;}#mermaid-svg-Io24ioUmmF4NOgVj .edgePath .path{stroke:#333333;stroke-width:2.0px;}#mermaid-svg-Io24ioUmmF4NOgVj .flowchart-link{stroke:#333333;fill:none;}#mermaid-svg-Io24ioUmmF4NOgVj .edgeLabel{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-Io24ioUmmF4NOgVj .edgeLabel p{background-color:rgba(232,232,232, 0.8);}#mermaid-svg-Io24ioUmmF4NOgVj .edgeLabel rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-Io24ioUmmF4NOgVj .labelBkg{background-color:rgba(232, 232, 232, 0.5);}#mermaid-svg-Io24ioUmmF4NOgVj .cluster rect{fill:#ffffde;stroke:#aaaa33;stroke-width:1px;}#mermaid-svg-Io24ioUmmF4NOgVj .cluster text{fill:#333;}#mermaid-svg-Io24ioUmmF4NOgVj .cluster span{color:#333;}#mermaid-svg-Io24ioUmmF4NOgVj div.mermaidTooltip{position:absolute;text-align:center;max-width:200px;padding:2px;font-family:\”trebuchet ms\”,verdana,arial,sans-serif;font-size:12px;background:hsl(80, 100%, 96.2745098039%);border:1px solid #aaaa33;border-radius:2px;pointer-events:none;z-index:100;}#mermaid-svg-Io24ioUmmF4NOgVj .flowchartTitleText{text-anchor:middle;font-size:18px;fill:#333;}#mermaid-svg-Io24ioUmmF4NOgVj rect.text{fill:none;stroke-width:0;}#mermaid-svg-Io24ioUmmF4NOgVj .icon-shape,#mermaid-svg-Io24ioUmmF4NOgVj .image-shape{background-color:rgba(232,232,232, 0.8);text-align:center;}#mermaid-svg-Io24ioUmmF4NOgVj .icon-shape p,#mermaid-svg-Io24ioUmmF4NOgVj .image-shape p{background-color:rgba(232,232,232, 0.8);padding:2px;}#mermaid-svg-Io24ioUmmF4NOgVj .icon-shape .label rect,#mermaid-svg-Io24ioUmmF4NOgVj .image-shape .label rect{opacity:0.5;background-color:rgba(232,232,232, 0.8);fill:rgba(232,232,232, 0.8);}#mermaid-svg-Io24ioUmmF4NOgVj .label-icon{display:inline-block;height:1em;overflow:visible;vertical-align:-0.125em;}#mermaid-svg-Io24ioUmmF4NOgVj .node .label-icon path{fill:currentColor;stroke:revert;stroke-width:revert;}#mermaid-svg-Io24ioUmmF4NOgVj :root{–mermaid-font-family:\”trebuchet ms\”,verdana,arial,sans-serif;}

Intent目标与不可变约束 I.inv

Candidate Execution即将进入现实的精确动作

Policy业务必要条件

Constitution不可关闭的固定底线

Evidence可验证事实

Decision ProofALLOW 或失败语义及其理由

RuntimeΓ

模型中刻意不包含"执行动作"这一对象。执行不属于 EBL 的职责范围——EBL 只决定候选执行是否获得跨越边界的资格，动作的实施由持有 cap 的边界与下游系统完成。

4.6.2 非目标

明确 EBL 不是什么，与明确它是什么同等重要，因为每一项误置的期待都会引入一类要求语言扩张能力的压力，而能力扩张与 4.1 所立的五项要求直接冲突。

表 4-4　EBL 的非目标

4.6.3 与既有系统的关系

EBL 不取代现有系统，它在既有系统之上增加一层共同语言。身份系统继续提供身份信息，审批系统继续组织成员表达同意，业务系统继续生成候选执行，AI 继续理解目标与规划方案，硬件继续控制密钥与设备能力。EBL 所增加的，是把这些分散系统的输出组织成一个可被最终边界验证的证明。

这一定位决定了采用成本的形态：EBL 不要求各系统改变内部实现，只要求它们在进入边界时，将关键事实与关系转换为可验证的证据形式。这是一项接口层的要求，而非架构层的替换。

附录

关于参考实现的说明 本部分的参考架构与案例来源于真实工程实践，经过抽象与简化，目的是说明理论如何落地，而非描述某一商业产品的完整实现。文中出现的 Bletchley SaaS 与 Enigma 执行边界为该实践中的组件名称，本书将其作为参考实现引用；具体的协议字段、密钥派生过程、固件状态机与生产参数不在本书范围内。

附录 A　端到端案例推演

本附录以一个简化案例，展示人的意图如何经过 AI 应用、协同治理层、EBL、Runtime 与独立硬件边界，最终转化为一次现实执行。案例的设计目的是使前三章的结论与第 4 章的机制形成一次可检验的闭环，因此第一次提交被设计为失败——失败并非源于攻击或明显错误，而源于一份已经过期的状态证据。

A.1 场景与意图对象

某企业使用 AI Agent 协助管理远程工业设备 DEVICE-042。维护负责人向 Agent 提交意图：在今日维护窗口内使该设备进入维护模式并停止主动力模块，操作须由两名相互独立的维护成员确认，且设备须处于无人运行状态。

该自然语言表述不是执行命令。依据公理 A1 与定义 D2.2.1，它首先被固化为可验证的意图对象：

Intent ID: INT-2027-0042
Target: DEVICE-042
Action: ENTER_MAINTENANCE_MODE
I.inv:
– main_drive must stop
– device must be unoccupied
– two independent approvals required
– execution must occur within maintenance window

规范化后计算 intent_hash。此后的审批、证据、候选执行与最终设备命令，均须绑定该值（A3）。

A.2 候选执行

Agent 依据意图生成候选执行对象：

Candidate ID: CAND-042-01
Device: DEVICE-042
Command: mode = maintenance
main_drive = stop
Intent Hash: H(INT-2027-0042)

此时该对象不能被发送至设备。AI 的职责在此终止于"提出候选"——依据公理 A6 与定义 D2.3.1，生成方不持有放行权。候选对象随后提交至协同治理层，由其展示意图与最终设备命令、收集审批、获取设备证据、加载对应策略并构造裁决输入。

A.3 EBL 策略与 AST

该操作对应的边界策略可抽象表述为：

require candidate.intent_hash == intent.hash
require candidate.device_id == intent.target
require candidate.command.mode == maintenance
require candidate.command.main_drive == stop
require approval.count >= 2
require approval.independent_domains >= 2
require evidence.device_identity.valid == true
require evidence.device_occupancy.state == unoccupied
require evidence.device_occupancy.age <= 30 seconds
require evidence.maintenance_window.active == true

该策略不访问网络，不重新查询设备，不补充证据，不修改候选对象——它只声明候选执行须满足的条件集合。这些限制不是实现约定，而是宪法 C1、C2、C9 在语法层的结果（4.3.3）。

策略解析后形成抽象语法树：

AND
├── BIND(candidate.intent_hash, intent.hash)
├── EQ(candidate.device_id, intent.target)
├── EQ(candidate.command.mode, maintenance)
├── EQ(candidate.command.main_drive, stop)
├── GTE(count(valid_approvals), 2)
├── GTE(count(independent_domains), 2)
├── VALID(device_identity_evidence)
├── EQ(device_occupancy.state, unoccupied)
├── LTE(device_occupancy.age, 30s)
└── EQ(maintenance_window.active, true)

AST 的价值不在于增加表达复杂度，而在于消除文本歧义并支持静态验证。加载前，验证器检查策略是否必然终止、是否引用未声明证据、是否包含外部副作用、是否超出资源上界、是否试图覆盖宪法、是否对四态作出显式处理。任一项不通过，规则被拒绝加载而非部署后忽略（4.3.4）。

A.4 第一次裁决：EXPIRED

治理层收集到的审批输入：

Approval A: MAINTAINER-01 │ Trust Domain: TEAM-A │ Bound: H(INT-2027-0042) │ valid
Approval B: MAINTAINER-02 │ Trust Domain: TEAM-B │ Bound: H(INT-2027-0042) │ valid

两名审批者属于不同信任域，因而满足关系独立性要求（P2.5）。注意此处成立的依据不是数量为二，而是信任域为二。

设备身份证据验证通过：

Device Identity Evidence:
Subject: DEVICE-042 │ Firmware Measurement: accepted
Device Signature: valid │ Status: VALID

设备占用状态证据显示无人运行：

Device Occupancy Evidence:
Subject: DEVICE-042 │ State: unoccupied
Observed At: 10:00:00 │ Maximum Age: 30s

而 Runtime 的判定时刻为 t = 10:00:47。该证据已存在四十七秒，超出其声明的有效期。它曾经成立，但不能证明设备当前仍处于无人运行状态。依据公理 A8，其状态为 EXPIRED 而非 TRUE：

Decision: DENY
Failed Rule: evidence.device_occupancy.age <= 30 seconds
Failure Semantics: EXPIRED

A.5 Fail Secure

此刻的处境值得逐项确认：审批已获得且独立性成立，候选对象未发现错误，设备身份验证通过，维护窗口仍然有效。唯一不成立的是一份状态证据的时效。

Runtime 不因"多数条件已满足"而放行。硬件边界未收到有效的 ALLOW 证明，因此不释放设备控制能力，候选执行保持阻塞，执行模块未收到任何命令。

这正是 Fail Secure 的含义（3.4）。系统没有推测设备可能仍然无人，没有沿用缓存状态，没有因维护窗口即将结束而降低标准，也没有允许管理员临时将证据有效期改为无限——最后一项被宪法 C10 排除，而非依赖运维纪律。

A.6 证据更新与第二次裁决

治理层请求状态采集模块重新生成证据：

Device Occupancy Evidence:
Subject: DEVICE-042 │ State: unoccupied
Observed At: 10:01:02 │ Maximum Age: 30s │ Device Signature: valid

新证据与设备标识、当前设备会话、当前意图、当前候选对象与当前时间窗口完成绑定。第一次失败的裁决记录不被修改或删除，它保留在证据存储中——依据 3.3.2，失败记录承载的是恢复路径信息，删除它等于删除运维依据。

Runtime 以相同策略与更新后的证据重新求值 AST，各项条件均成立，产生 d = ALLOW。但 ALLOW 不是孤立的布尔值，它同时产生判定证明：

ALLOW(
candidate = H(CAND-042-01),
intent = H(INT-2027-0042),
policy = H(POLICY-MAINTENANCE-V1),
constitution = V1,
evidence_set = H(EVIDENCE-SET-02),
runtime = V1.0,
evaluated_at = 10:01:05,
decision_proof = H(PROOF-042-02)
)

A.7 硬件边界与执行

判定证明随候选执行进入独立硬件边界。边界不接受来自上层的 allow = true 断言——依据公理 A7，上层提交的是证据而非结论。边界至少独立验证：Runtime 身份、策略哈希、候选对象哈希、意图绑定、证明完整性、防重放计数器、当前设备状态、以及固化于边界内的硬性限制。

全部成立后，边界释放一次受限执行能力，命令送达执行模块：

DEVICE-042 │ ENTER_MAINTENANCE_MODE │ MAIN_DRIVE_STOP

硬件记录结果并生成设备签名证据，完整证据链闭合：

Intent → Candidate Execution → Policy → Approval → Evidence Set
→ Runtime Decision Proof → Hardware Release → Execution Result Evidence

A.8 案例结论

第一次提交没有遭遇攻击，AI 没有出错，审批成员没有作恶。系统只是持有了一份过期四十七秒的状态证据。在传统自动化设计中，这类情形通常由缓存或默认值消解，执行照常发生；而在本书的框架下，过期意味着系统无法证明当前事实仍然成立，因而不构成放行依据。

案例覆盖的结论对应如下：

附录 B　参考架构与硬件边界

B.1 分层参考架构

执行控制不要求所有系统采用相同硬件，但要求明确区分理解、协调、裁决与执行四类能力，并使它们分属不同信任域（A6）。

图 B-1　执行边界的分层参考架构

┌──────────────────────────────┐
│ AI Application / Agent │ 理解目标、生成候选执行
│ Intent Generation │
│ Candidate Planning │
└──────────────┬───────────────┘
│
┌──────────────▼───────────────┐
│ Bletchley SaaS │ 协同治理：审批、策略、证据收集
│ Workflow Coordination │
│ Approval / Policy / Evidence │
└──────────────┬───────────────┘
│ mTLS / gRPC
┌──────────────▼───────────────┐
│ Linux Coordination Domain │ 网络、界面、数据组织
│ Network / UI / Data Exchange │ 对 Final Veto 而言不可信
└──────────────┬───────────────┘
│ Authenticated Channel
┌──────────────▼───────────────┐
│ Arbiter Domain │ 独立 MCU
│ Independent MCU │ EBL Runtime、策略求值
│ EBL Runtime / Policy Check │ 证据与证明链验证
└──────────────┬───────────────┘
│ Restricted Protocol
┌──────────────▼───────────────┐
│ Security Execution Domain │ 独立 MCU
│ Final Payload Verification │ 最终对象校验、防重放、Safe Mode
└──────────────┬───────────────┘
│
┌──────────────▼───────────────┐
│ Secure Element / Capability │ cap 独占：密钥释放、设备动作
│ Final Execution Evidence │
└──────────────────────────────┘

图中的重点不是器件选型，而是信任关系。上层的 AI 与 SaaS 可以理解业务、协调审批、收集证据并生成候选执行，但不能直接获得最终执行能力；Linux 域承担网络、界面与数据组织，但不被视为最终裁决者；Arbiter 域承担规则求值与证明验证；Security 域承担最终对象校验、防重放与能力释放。判据仍是 2.4.3 的那一条：任何单一上层组件被攻陷，都不应直接产生现实执行。

实现注记。 上述各域在参考实现中分别对应通用应用处理器、独立微控制器与安全元件等器件类别。具体型号属于实现选择而非架构要求，本书不列出；替换器件不改变架构成立与否，改变信任域划分则会。

B.2 TEE 与独立 MCU

可信执行环境能够隔离敏感代码，降低通用操作系统被攻陷后的风险，是一种有效的实现手段。但 TEE 通常与主处理器共享启动链、更新路径、电源与时钟、芯片供应链、部分外设及管理权限——这些共享项构成共因失效路径（2.4.5），使 A6 所要求的独立性在故障域上不完全成立。

因此本书将 TEE 定位为可选实现而非核心机制。对高风险系统，采用独立 MCU 或独立安全控制器，将 Final Veto 从通用操作系统中物理分离，其价值不在于计算更安全，而在于：上层系统无法通过普通软件调用绕过它（A10）。

B.3 带外确认与显示绑定

部分高风险执行需要本地或带外确认。此类确认若仅展示抽象描述（如"是否批准该操作"），则确认者所同意的是一段描述而非最终对象，违反 A3。

有效的带外确认须展示最终执行对象的关键字段：目标对象、动作类型、控制参数或金额、意图标识、风险级别、有效时间、最终对象摘要。其真正作用不是增加一个按钮，而是建立一条独立于上层界面的显示绑定——当上层 UI 被篡改时，边界仍能展示它实际准备放行的对象。

B.4 固件锁与底线固化

若硬件边界可被普通管理员随时重新配置，则它不构成稳定的 Final Veto。参考架构因此须包含：安全启动、固件签名、防回滚、调试端口锁定、读出保护、固定安全参数、受控升级流程、设备身份与固件测量证据。

并非所有规则都需固化。业务策略 P 应当可更新，宪法 K 所规定的固定底线不应通过常规远程配置关闭（A4、E2.4）。可变化的是业务范围，不应轻易变化的是：什么情况下系统永远不产生 ALLOW。

B.5 边界不是单个芯片

物理信任边界不等于某一颗安全芯片。它是一组须同时成立的关系：密钥或执行能力不可被上层直接取得；最终对象在边界内重新验证；Runtime 结果可被独立验证；证据与候选对象完成绑定；失败时默认拒绝；固件与设备身份可证明；执行结果留下设备证据。

因此工程上需要设计的不是"最安全的芯片"，而是：从上层意图到最终能力释放之间，是否存在一条不可绕过的控制链。这一问题的答案由架构给出，不由器件给出。

附录 C　公理索引・定义索引・失败矩阵

C.1 公理索引

表 C-1　公理速查

常被引用的派生命题：Signing ≠ Final Veto（P2.3）；密钥保护 ≠ 执行保护（P2.3）；计数 ≠ 独立性（P2.5）；局部正确 ≠ 整体正确（P1.1）。

C.2 定义索引

C.3 失败矩阵

表 C-2　证据状态与条件求值结果

FALSE 与其余四种非放行状态的区别是实质性的：FALSE 表示系统已完成证明且结论为拒绝，其余四种表示系统无法完成证明。前者的恢复途径是修改请求，后者的恢复途径是修复证据。

〔补〕关于验证失败的归类。 一份签名不匹配或来源凭据无效的证据，在放行判定上与 UNKNOWN 等价——两者均不参与 π。但在告警语义上二者应予区分：验证失败通常是攻击指示器（威胁类 X4），而无法验证通常是通道故障（X8）。本书将其在 σ(e) 中归入 UNKNOWN 以保持四态的最小性，同时建议实现在证明中保留 verification_failed 标记供监测使用。

全书结论 没有完整证明，就没有 ALLOW。