HAVENLON RESEARCH

AI 執行工程論綱

從執行縫隙、執行控制、對抗性完整到執行邊界語言

一套研究人類與機器意圖如何進入真實執行,以及當系統中的任何一環可能失效、偏移或遭到攻擊時,如何仍然守住執行邊界的系統性框架。

正式版66 分鐘閱讀
線上閱讀下載 Markdown
目錄

AI 執行工程論綱

Theses on AI Execution Engineering


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


本書提出一門尚未成立的工程學的十條公理、若干定義與命題。

這些理論並非來自純粹抽象推演,而是從近兩年的軟件、協議、Runtime、Evidence 與硬件邊界實踐中逐步總結出來的。

它面向評判而非接受:指出某條公理不必要,或指出一個違反它而仍然成立的系統,都是對本書的有效反駁。


序言 一門尚未存在的工程學

過去數十年,軟件工程的核心目標是讓計算正確發生。編程語言、算法、數據庫、網絡協議與操作系統的演進,圍繞穩定性、效率與可靠性展開;構建於其上的安全體系——身份認證、權限控制、訪問管理、加密通信與系統防護——同樣服務於一個未曾改變的目標:保證數字世界中的計算按預期完成。這一範式支撐了互聯網時代的全部基礎設施,也塑造了今天絕大多數信息系統的形態。

該範式成立的隱含前提是:軟件提供能力,人類作出執行決定。無論轉賬、簽署合同、啟動設備還是批准業務流程,最終將一個數字結論轉化為現實動作的主體始終是人。軟件在這條路徑上承擔計算職責,不承擔執行職責。

這一前提正在失效。越來越多的 AI 系統不再僅生成內容,而是理解目標、規劃任務、調用工具、編排流程,並通過接口與設備影響現實。從企業工作流到工業控制,從數字資產到機器人系統,AI 正在成為現實執行鏈中的一個環節,而非鏈外的信息處理工具。由此,一個此前不必單獨提出的問題變得必須回答:一個數字意圖,需要滿足哪些條件,才有資格進入現實世界。

問題的性質與計算正確性不同。計算錯誤通常表現為程序崩潰、數據異常或服務中斷,其後果限於數字域且多數可回滾;執行錯誤則表現為資金被錯誤轉移、設備被錯誤啟動、權限被錯誤授予,其後果發生於現實且往往不可撤銷。需要被保護的對象,因此從程序本身擴展為從意圖到現實結果之間的整條執行路徑。

傳統軟件工程未系統回答這一問題,傳統安全工程也未回答——後者的保護域是身份、權限與訪問,其判定對象是"誰可以訪問什麼",而非"這一個具體動作是否有資格發生"。兩者之間存在一片無人認領的區域,本書稱之為執行縫隙。

本書提出 AI 執行工程(AI Execution Engineering) 這一工程視角,用以處理該區域的問題。它不替代軟件工程,也不是安全工程的延伸,其對象是另一類長期缺乏系統研究的問題:數字系統如何安全、可驗證、可追溯地影響現實世界。

圍繞這一對象,本書建立四個相互銜接的理論部件,構成一條完整的邏輯鏈——發現問題,建立控制,證明控制有效,將理論轉化為可運行的工程規則:

  • Execution Gap(執行縫隙):界定數字意圖進入現實過程中長期存在而未被單獨治理的風險區間。
  • Execution Control(執行控制):建立獨立於業務系統的裁決機制,使現實動作處於可約束、可證明的邊界之內。
  • Adversarial Completeness(對抗性完整):在惡意攻擊、異常狀態與未知條件下,論證控制能力是否仍然成立。
  • EBL(Execution Boundary Language):將上述結論形式化為可驗證、可執行、可審計的規則,使邊界能夠被工程實現。

本書的體裁是論綱,不是導論。這一區分是實質性的:導論面向已經存在的學科,任務是引導入門;論綱面向尚未成立的學科,任務是提出一組可被檢驗、也可被推翻的起點。因此本書的寫法是給出十條公理、若干定義與命題,並明確標註哪些結論是推導所得、哪些只是工程選擇。讀者被期待的姿態不是接受,而是評判——指出某條公理不必要,或指出某個系統在違反它的情況下依然成立,都是對本書的有效反駁。

書中不迴避未完成的部分。語言尚需設計,Runtime 尚需驗證,硬件邊界尚未形成標準,不同行業將產生不同實現。但問題已經出現,且不會隨著模型能力提升而自行消失。相反的關係更接近事實:AI 越智能、執行越自動、工具越豐富,現實世界越需要一條不會被智能本身繞過的邊界。

未來十年需要建立的,不只是更強的模型、更好的 Agent 與更高效的自動化。在這些能力之下,還須存在另一層基礎設施。它不負責讓系統做更多事情,而負責守住哪些事情仍然不能發生;它不替代人的判斷,而確保人的意圖不會在進入現實之前被無聲改寫;它不依賴任何永遠可信的主體,而要求關鍵執行由證據、規則與邊界共同證明。

這就是本書所討論的工程學。



第 0 章 術語、符號與閱讀約定

本章不含論證,僅供查閱。首次閱讀可跳過 0.3,在正文遇到術語時回查。

0.1 論斷類型與編號約定

本書對所有獨立成立的論斷標註類型。讀者可據此判斷一項陳述的效力來源,以及反駁它需要付出什麼。

類型記號效力來源如何反駁
公理An不加證明,作為體系起點舉出一個該公理不成立而執行控制仍成立的系統
定義D章.序約定指出定義包含不可判定的屬性
命題P章.序由公理與定義推出指出推導缺環
推論C章.序命題的直接結果同上
工程約定E章.序設計選擇,非邏輯必然提出代價更低的替代選擇

工程約定這一類型的存在是刻意的。一門新學科最易犯的錯誤,是把自身的設計偏好偽裝成必然性。凡本書無法從公理推出、而確實作出了取捨之處,一律標為 E 並寫明代價。

各章節前以引文格式出現的單句為題記,屬修辭性表述,不承擔論證責任。正文中帶〔補〕標記的段落,為原始論證之外補充的內容。

0.2 符號表

表 0-1 全書符號約定

符號讀法含義
IIntent意圖對象
I.invinvariants意圖中不可變的關鍵約束集合
xCandidate Execution候選執行對象,進入現實的精確動作
PPolicy可編程業務策略集合
KConstitution固定安全底線集合,不可被 P 關閉
EvEvidence Set證據集合,e ∈ Ev
σ(e)status證據狀態,值域見公理 A8
CtxContext系統狀態與環境
ttime判定時刻
ΓGamma判定函數,Runtime 的抽象
dDecision決策,d ∈ {ALLOW, DENY, SAFE_MODE}
πProof判定證明,可重放
capcapability現實動作所需的必要能力
⊨滿足Ev ⊨ c 表示證據集合證成條件 c

判定函數的完整形式:

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

0.3 術語表

按主題分組。每條給出中文術語、英文對應與工程定義。定義中不含形容詞性描述——若刪去修飾後定義不再成立,說明該定義依賴修辭而非屬性。

問題域

術語英文定義
AI 執行工程AI Execution Engineering研究數字系統如何安全、可驗證、可追溯地影響現實世界的工程領域
執行縫隙Execution Gap意圖形成後至現實動作發生前,缺乏端到端責任主體與統一驗證的路徑區間
現實動作Real-World Action效果發生於數字系統之外、且不能由系統自身完全回滾的動作
執行鏈Execution Chain從意圖產生到現實動作發生所經過的全部組件與轉換的序列
責任缺失Accountability Void執行鏈上不存在對最終結果負端到端責任的單一主體的狀態
錯誤半徑Blast Radius一次錯誤執行所影響的現實對象數量與不可撤銷程度

控制機制

術語英文定義
執行控制Execution Control在現實動作發生前,對意圖、最終執行對象、條件、證據及其綁定關係進行獨立裁決,僅在完整條件被證明成立時釋放執行能力的機制(D2.1.1)
意圖Intent表達期望發生什麼、並攜帶不可變約束集 I.inv 的可驗證對象
候選執行Candidate Execution已完全具化、尚未獲得跨越邊界能力的精確動作對象
意圖綁定Intent Binding候選執行與原始意圖不可變約束之間的可驗證對應關係
最終否決權Final Veto由獨立於候選執行生成方的組件持有的、不可繞過且不可被覆蓋的拒絕能力(D2.3.1)
判定函數Decision Function Γ接收意圖、候選執行、策略、憲法、證據、上下文與時刻,輸出決策與判定證明的確定性函數
控制鏈Control Chain逐級建立可驗證關係而非逐級傳遞結論的執行路徑結構(圖 2-1)
重裁決Re-adjudication因 x、Ev 或 Ctx 變化而使既有判定失效、須重新求值的過程(A9)

邊界與能力

術語英文定義
執行邊界Execution Boundary候選執行須獲得放行才能跨越、且跨越後動作即進入現實的單向控制點
物理信任邊界Physical Trust Boundary由硬件獨佔必要能力所構成、上層軟件越權無法穿越的執行邊界
必要能力Necessary Capability cap現實動作發生所不可缺少的一項能力,邊界通過獨佔它使否決生效(A10)
信任域Trust Domain共享同一攻陷後果的組件集合;域內任一組件被攻陷視同全域失效
共因故障Common-Cause Failure因共享供電、時鐘或通道而使判定組件與被判定系統同時失效的故障模式
憲法Constitution K任何可編程策略都不能關閉、削弱或旁路的固定安全底線集合
策略Policy P表達候選執行須滿足的業務條件、可由授權方修改的規則集合
Owner ≠ God—系統所有者擁有配置權但不擁有關閉底線權的設計原則

證據與證明

術語英文定義
證據Evidence帶類型、來源、主體綁定與時效的可驗證事實對象
證據鏈Evidence Chain多項證據之間的引用與依賴關係所構成的結構
證明圖Proof Graph由證據與規則求值節點構成、用以證成某一決策的有向圖
判定證明Decision Proof π記錄裁決所依據的證據圖與規則求值路徑、可被重放的結構
有效期Validity Window證據被視為成立的時間區間,超出後狀態轉為 EXPIRED
主體綁定Subject Binding證據與其所描述對象之間的可驗證對應關係
關係獨立性Relational Independence多個證據來源之間不存在共同依賴的性質,構成多方證明有效的前提

失敗語義

術語英文定義
VALID—證據已驗證且在有效期內,可參與判定證明
UNKNOWN—證據已提交但無法驗證
MISSING—判定所需的證據未提交
EXPIRED—證據曾成立,當前已超出有效期
CONFLICT—存在與之矛盾的同類證據
安全模式Safe Mode系統無法完成證明時進入的、僅保留最小必要能力的降級狀態
保守失敗Fail Secure系統在故障或不可判定狀態下默認不釋放執行能力的架構屬性
開放失敗Fail Open系統在故障狀態下默認放行的架構屬性,本書視為執行控制的反模式

語言與運行時

術語英文定義
EBLExecution Boundary Language用於表達執行邊界規則的領域語言,非圖靈完備,表達能力受憲法約束
RuntimeExecution Boundary Runtime執行 Γ 的確定性組件,負責裁決而不負責執行
裁決執行分離Adjudication–Execution Separation判定組件與動作執行組件不得為同一主體的架構原則(A6)
語義漂移Semantic Drift同一規則在不同 Runtime 實現上產生不同判定結果的現象
抽象語法樹ASTEBL 規則經解析後的內部結構表示,是可驗證性的載體

對抗分析

術語英文定義
對抗性完整Adversarial Completeness系統在明確定義的威脅模型下,其關鍵安全命題仍然成立的性質
安全命題Security Proposition以可證偽形式陳述的安全斷言,區別於"具備某項安全功能"的描述
不變量Invariant在任何輸入與狀態下均須保持為真的系統性質
失敗矩陣Failure Matrix枚舉關鍵失敗方式及其對應處置與殘餘風險的表格
殘餘風險Residual Risk在既定威脅模型與機制下仍未被覆蓋的風險
EX-STRIDE—面向執行鏈的威脅分類法,替代面向數據與身份的傳統 STRIDE(表 3-1)

第 1 章 執行縫隙 Execution Gap

題記:每一步都合法,最終結果仍然可能是錯的。


1.1 傳統安全的保護域:節點而非路徑

現代安全體系由四類機制構成,它們分別把守執行路徑上的不同位置。身份機制保護主體入口,回答"誰進入了系統";權限機制保護能力邊界,回答"誰獲得了什麼資格";認證機制保護通信來源,回答"這個請求來自何處";審批機制保護組織決策,回答"誰表達了同意"。四者在各自的問題域內成熟且有效,其價值不因 AI 的出現而降低。

問題不在於任一機制的有效性,而在於它們的組織方式。這四類機制通常由不同團隊、按不同標準、在不同時期分散建設:身份系統只負責身份,權限系統只負責訪問,審批系統只負責流程,簽名系統只負責簽名,執行系統只負責把收到的命令轉化為結果。每個系統都完整履行了自身職責,但沒有任何一個系統對整條路徑負責。

表 1-1 傳統安全機制的保護域

機制保護對象回答的問題不回答的問題
身份主體入口誰進入了系統進入後要做的事是否與其聲明一致
權限能力邊界誰有資格做這類操作這一次操作是否應當發生
認證通信來源請求來自何處請求內容是否仍與原始意圖一致
審批決策過程誰表達了同意同意的對象與執行的對象是否為同一個
簽名數據完整性某密鑰是否簽署了這段數據這段數據是否應當被簽署

上表最後一列構成一個共同的空白:沒有任何一列回答"最終發生的現實結果,為什麼可以被認為是最初意圖的合法延續"。 該問題不屬於其中任何一個機制的職責,因而在架構上無人認領。

由此產生一種在實踐中常見、在設計上卻未被預期的局面:用戶身份真實,權限配置正確,審批流程通過,數字簽名有效,接口調用成功,設備按指令運行——而最終發生的事情,仍然可能不是用戶希望發生的事情。這不是某個節點失守的結果,而是節點之間缺乏連續約束的結果。

命題 P1.1(局部正確的非傳遞性) 執行鏈上每個組件均滿足其自身規格,不蘊含鏈的端到端結果符合原始意圖。因此"所有組件分別正確 ⇒ 整體結果正確"不是有效推論。

P1.1 是本書全部後續論證的起點。若該推論成立,執行控制便無必要;正因其不成立,才需要一個以整條路徑而非單個節點為對象的機制。


1.2 AI 引入的結構性變化

AI 並非第一種能夠自動執行任務的軟件。腳本、工作流引擎、規則系統、自動化平臺與工業控制系統早已承擔大量無人干預的操作,自動化本身並不新鮮。真正的變化在於路徑的確定時刻:傳統自動化沿預先定義的路徑運行,路徑在部署時確定,運行時不變;AI 系統則在運行過程中解釋目標、選擇路徑並生成動作,路徑在運行時才被確定。

這一差別使得"部署時審查路徑"這一傳統安全手段失去覆蓋能力。審查者在部署時能看到的是能力集合,而非將被實際組合出的路徑。以下九個維度分別說明該變化如何在執行鏈的不同位置擴大縫隙。

表 1-2 AI 系統對執行鏈各維度的擴張

#維度傳統自動化AI 系統對執行鏈的後果
1目標解釋無解釋環節,指令即路徑自然語言目標由模型解釋為結構化請求解釋空間擴大,意圖與請求間出現語義損耗
2路徑規劃路徑預定義運行時規劃多步方案行動空間擴大,實際路徑不可在部署時枚舉
3工具連接接口固定、數量有限通過 MCP 等協議動態發現與接入工具連接空間擴大,能力邊界隨環境變化
4參數生成參數由上游系統計算參數由模型生成生成空間擴大,關鍵字段可能無上游來源
5流程編排步驟與依賴固定動態編排、條件分支由模型決定傳播空間擴大,單點誤解可跨步驟傳播
6多主體協作單一執行主體多 Agent 分工與相互調用責任空間擴大,無單一主體可歸因
7執行速度受人工節奏約束毫秒級連續執行反應距離縮短,人工介入窗口消失
8執行規模單次操作批量、併發、持續執行錯誤半徑擴大,單次誤解影響大量對象
9上下文輸入輸入受控且結構化檢索內容、工具返回、外部文檔均進入上下文攻擊面擴大,輸入通道成為控制通道

九個維度的共同結構是:每一項都增加了從意圖到動作之間的轉換次數或轉換自由度,而轉換正是關係斷裂發生的位置(見 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 執行鏈上的七處關係斷裂

圖中每條虛線代表一次未被驗證的轉換。執行控制的任務,即是把其中每一條虛線轉化為可驗證的實線關係。

合法路徑產生錯誤結果

執行縫隙最難處理之處在於,它不依賴任何違規行為。考察一條完全合法的路徑:用戶合法登錄,提出真實請求,AI 合法調用工具,Agent 使用被授權的接口,策略引擎正常返回允許,審批者完成確認,簽名系統生成有效簽名,執行端成功完成動作。從日誌看,八個步驟全部正常。但若第一步中模型誤解了執行對象,其後七個安全機制所保護的,是這一誤解沿鏈條順利傳播的過程。

命題 P1.3(合法路徑的失效) 合法主體、合法權限與合法流程的組合,不排除產生與原始意圖不符的現實結果。因此執行縫隙不能被歸類為訪問控制缺陷、模型安全缺陷或業務邏輯漏洞——它橫跨三者的邊界。

責任缺失

上述結構的組織成因是清晰的。現代系統按組件劃分責任:模型團隊負責模型能力,Agent 團隊負責任務編排,身份團隊負責認證,安全團隊負責權限,業務團隊負責審批,設備團隊負責執行,審計團隊負責留痕。每個團隊都能證明其組件符合設計要求,而現實結果不由任何單一組件產生,它由整條鏈共同產生。

若組織未定義獨立的執行控制責任,系統便默認接受 P1.1 所否定的那個推論。

命題 P1.4(端到端責任缺失) 在按組件劃分責任的組織結構中,若不設立以最終現實結果為對象的獨立責任主體,則執行鏈上不存在對該結果負責的主體。所有人負責一部分,等價於無人負責最終結果。

P1.4 是一項組織命題而非技術命題,但它決定技術方案能否落地:執行控制若不對應一個明確的責任主體,其部署將缺乏組織依據。


1.4 與相鄰學科的邊界

AI 執行工程不在真空中提出。它與若干成熟領域存在交集,但保護域不同。明確邊界的目的不是劃分地盤,而是說明為何既有領域的成果無法直接覆蓋本書所定義的問題。

表 1-3 相鄰領域的保護域與覆蓋邊界

領域保護對象核心判定與執行控制的交集未覆蓋之處
零信任架構 Zero Trust訪問關係每次訪問是否可信拒絕隱式信任、持續驗證判定對象是訪問請求,非最終執行對象;不處理意圖綁定
身份與訪問管理 IAM主體資格誰可以做什麼提供身份與權限證據資格是長期的,不判定單次動作是否應發生
形式化驗證程序性質實現是否符合規約提供不變量與證明方法驗證對象是代碼,規約本身是否符合意圖不在其內
系統可靠性工程 SRE服務可用性系統是否按預期運行故障模式、降級策略優化方向是可用性,與保守失敗存在方向衝突
功能安全 IEC 61508物理傷害風險失效是否導致危險狀態安全完整性等級、失效分析假設指令來源可信,不處理指令語義是否忠實於意圖
模型對齊模型行為輸出是否符合人類偏好降低誤解概率概率性改善,不構成邊界;本書將其置於邊界之上而非之內

其中與本書最接近的是功能安全與形式化驗證。兩者都建立了"證明而非聲明"的傳統,本書的對抗性完整(第 3 章)與判定證明(第 2.5 節)直接受其影響。差別在於判定對象:功能安全處理"設備失效是否導致危險",其輸入指令的正確性是前提而非結論;形式化驗證處理"實現是否符合規約",規約的正確性同樣是前提。AI 執行工程恰好處理這兩個被作為前提的部分——指令是否忠實於意圖,以及在無法證明時應當發生什麼。

與 SRE 的關係需要單獨說明,因為二者存在真實的方向衝突。SRE 以可用性為優化目標,故障時傾向於保持服務;執行控制以保守失敗為架構屬性,無法證明時拒絕放行。該衝突不可通過技術手段消解,只能通過明確劃分適用範圍來處理:對可回滾的數字操作,可用性優先合理;對不可撤銷的現實動作,保守失敗優先。這一劃分本身是工程約定,其論證見 3.4。


1.5 本章命題小結

編號命題
P1.1每個組件滿足自身規格,不蘊含端到端結果符合意圖
P1.2在運行時確定路徑的系統中,執行縫隙是結構常態,非集成缺陷
P1.3合法主體、合法權限、合法流程的組合不排除錯誤的現實結果
P1.4未設立以最終結果為對象的獨立責任主體,則無人對最終結果負責
D1.3.1執行縫隙的定義

四條命題共同確立了本書的問題域:需要被治理的對象不是任何單個節點,而是節點之間的轉換關係;需要被建立的機制不是更嚴格的組件規格,而是以最終執行對象為判定對象的獨立裁決。第 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 從意圖到現實的控制鏈

這條鏈與普通工作流的差別在於傳遞物的性質。工作流逐級傳遞結論:上一環節完成,下一環節據此繼續。控制鏈逐級建立可驗證關係:意圖定義目標與邊界,策略定義必要條件,審批綁定具體對象,證據證明條件當前成立,候選執行表達精確動作,最終裁決對全部關係一次性求值。任一關係不成立,鏈條不產生 ALLOW。

據此,一個完整的執行控制過程須回答五個問題,它們分別對應鏈上的環節與公理:

表 2-2 控制鏈的五項判定義務

問題鏈上環節公理
1意圖是什麼IntentA1
2最終對象是什麼Candidate ExecutionA2
3二者如何綁定Intent Binding / ApprovalA2、A3
4當前條件是否仍成立EvidenceA7、A8、A9
5誰擁有最後否決權Final VetoA5、A6、A10

本章其餘各節依次展開第 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 意圖綁定的驗證關係

綁定失敗的判定是逐項的,且不接受近似。原始意圖批准向賬戶 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 結果不可被上層組件覆蓋、重試或重新解釋;(c) 判定所依據的輸入包含最終執行對象本身,而非其上游描述。

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(c),不構成 Final Veto。 推論 C2.4:Final Veto 必須位於簽名或執行能力授予之前,並有權拒絕提供該能力。

(三)模型判斷:確定性缺陷。 AI 組件可有效參與異常發現、風險分析與方案比較,這類能力屬於上層判斷,價值明確。但 Final Veto 要求同一規則與同一輸入產生同一結果(Γ 的確定性性質,見 2.1)。基於概率輸出的組件其行為可被上下文改寫、被提示詞誘導、被措辭影響;在關鍵條件缺失時,它可能給出"酌情判斷",在證據衝突時,它可能通過語言層面的解釋消解矛盾。這兩種行為恰好違反公理 A8 所要求的保守閉合。因此,模型可以參與判斷,但不應持有最後邊界。

機制判定對象判定時點結果可否被覆蓋確定性是否滿足定義 2.3.1
審批業務描述流程中段可(後續重生成)高否(違反 a、c)
數字簽名字節序列執行前否高否(違反 c)
模型判斷自然語言語境任意可(重試/改寫提示)低否(違反 b)
Final Veto最終執行對象 + 證據集能力授予前否高是

表 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) 上層軟件不能繞過其裁決直接完成執行;(c) 邊界可獨立作出拒絕;(d) 關鍵規則不可由普通管理員關閉;(e) 關鍵密鑰或控制能力不向上層暴露;(f) 邊界能夠驗證對象、狀態與證據;(g) 裁決結果被獨立記錄。

"使用硬件"不等於具備物理信任邊界。一個可被遠程更新、完全接受主機命令、不作獨立狀態判斷的硬件模塊,在架構上仍是軟件系統的外接執行器,其信任域與上層同一,因而不滿足公理 A6。

命題 P2.3(密鑰保護不等於執行保護) 若硬件模塊僅對上層提交的 Payload 執行簽名,則其保護對象為密鑰而非執行。此類模塊降低密鑰洩露風險,但不降低錯誤執行風險。

由 P2.3 可知,硬件安全模塊、硬件錢包與安全芯片的既有部署,不自動構成執行邊界。使其構成邊界,須令其進一步回答:當前 Payload 是否與意圖綁定,是否與審批對象一致,必要證據是否完整,時間與狀態是否有效,是否觸發固定限制,是否存在否決條件。

2.4.3 必要能力

邊界的控制力來自其對某項必要能力 cap 的獨佔。可作為 cap 的能力包括:最終簽名密鑰、設備啟動信號、電源控制、執行令牌、關鍵通信通道、不可替代的授權證明、最終命令解密能力。

判據是單一的:若上層系統可繞開邊界直接完成執行,則該邊界是輔助組件而非邊界。公理 A10 的工程含義即在於此——邊界須成為執行鏈的必要節點,使得 d ≠ ALLOW ⇒ 動作不可發生。

圖 2-3 執行控制的分層與能力歸屬

圖中虛線是全章最重要的一條線:它標記了一條必須不存在的路徑。架構評審的核心問題不是"邊界是否存在",而是"該虛線是否真的不存在"。

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 證據與日誌的角色區別

日誌證據
回答的問題系統過去發生了什麼本次執行所依賴的關鍵事實是什麼
使用時點事後事前
參與裁決否是
缺失後果追溯困難無法產生 ALLOW

一次完整執行的證據集最終也應進入審計存儲,但只有在執行前參與判定的部分,才屬於執行控制的範疇。

2.5.3 四項語義要求

有效期。 證據描述的是某一時刻的事實,而非永久成立的命題。風控快照、設備狀態、餘額、授權範圍均隨時間變化。證據須攜帶有效期,超出後狀態轉為 EXPIRED,不再參與證明(公理 A8、A9)。

對象綁定。 證據須綁定其所描述的具體對象。"該賬戶已通過合規審查"若不綁定賬戶標識,則可被用於證成任意賬戶;"設備處於安全狀態"若不綁定設備標識與狀態快照時刻,則可被複用於其他設備或其他時刻。

衝突保留。 當多份同類證據相互矛盾時,系統不得通過選取其一、取多數或按來源優先級消解衝突。衝突本身是一項事實,須被保留並觸發 CONFLICT 狀態。將衝突消解為單一結論,等於用一次未經證明的裁量替代證據(公理 A7)。

關係獨立性。 多方確認常以數量表達——兩人批准、三人簽名、多數通過。數量不蘊含獨立性:三個賬戶可能由同一人控制,多個服務可能依賴同一憑證,多個審批者可能來自同一管理域,多個傳感器可能共享同一故障源。

命題 P2.5(計數不構成獨立性證明) 證據數量 n > 1 不蘊含這些證據的失效事件相互獨立。若不表達獨立性維度,多方確認在共因失效下退化為單方確認。

因此獨立性須作為一等語義被顯式表達,其維度至少包括:身份主體、設備、信任域、密鑰來源、組織角色、物理位置、故障路徑。

2.5.4 完整證明與 ALLOW

傳統策略系統廣泛使用缺省行為:字段缺失時採用默認配置,狀態未知時沿用上次結果,檢查失敗時為可用性繼續執行。在可回滾的業務場景中,這類設計有其合理性;在不可逆執行中,它直接違反公理 A8。

d = ALLOW 須由完整證明產生,即以下條件全部成立:每一項必要條件都有對應證據;每一份證據 σ(e) = VALID;每一份證據與對象綁定;證據間不存在未解決的衝突;最終對象與意圖及審批一致;未觸發任何固定否決條件。

這一要求區分了兩種性質相反的判斷。"系統未發現問題"是消極判斷,其成立依賴於檢查的完備性,而檢查的完備性無法自證;"系統已形成完整證明"是積極判斷,其成立由 π 顯式承載,可被重放與審計。執行控制只接受後者。

圖 2-4 判定證明的結構

證明圖中的任一節點失效——證據狀態非 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、A2、A3、A9判定的對象是什麼,何時失效
權威層A4、A5、A6誰有權說"不",誰無權撤銷它
證明層A7、A8什麼算作理由,理由不足時怎麼辦
實現層A10判定結論如何在物理上生效

四層構成一條閉合鏈:確定對象(對象層)→ 確定權威(權威層)→ 確定理由(證明層)→ 確定生效方式(實現層)。任何一層缺失,其餘三層的成果都不構成執行控制。 原稿反覆論證的"合法路徑也可以產生錯誤結果",其結構性原因正是現有系統通常只實現了其中一到兩層。

〔補〕公理集合的獨立性說明。 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":

編號安全命題
SP-1即使 SaaS 被完全攻陷,攻擊者仍不能繞過硬件邊界獲得最終執行能力
SP-2即使管理員擁有最高業務權限,也不能關閉固化於邊界內的安全底線
SP-3即使審批賬戶數量滿足要求,若其不具備關係獨立性,系統不產生 ALLOW
SP-4即使最終 Payload 攜帶合法簽名,若無法與意圖及審批對象綁定,執行被拒絕
SP-5即使狀態無法確認,系統也不將未知解釋為安全

表 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 威脅分類矩陣

編號攻擊類受損環節典型來源違反公理失敗語義緩解機制
X1意圖偽造I提示詞注入、被汙染的檢索內容A1UNKNOWN意圖對象簽名、來源證據
X2意圖漂移I → x模型誤解、多跳轉換中約束丟失A2CONFLICTI.inv 逐跳校驗
X3對象替換x審批後參數重寫、Payload 重新生成A3、A9CONFLICThash(x) 綁定、重裁決
X4證據偽造Ev偽造合規結論、冒用來源憑據A7UNKNOWN簽名、主體綁定
X5證據失效Ev使用過期風控快照、複用舊狀態A8、A9EXPIRED有效期強制、重採集
X6權限越權P / K管理員關閉規則、配置提權A4—憲法固化於硬件域
X7邊界繞過cap設備拆解、密鑰導出、旁路通道A6、A10—獨佔必要能力、防拆、熔絲
X8可用性脅迫Γ驗證服務不可達迫使降級放行A8MISSINGFail Secure 架構屬性
X9供應鏈汙染全鏈固件交付前替換、依賴投毒A6UNKNOWN出廠證明、遠程認證
X10組合攻擊跨環節X1+X5、X6+X8 等聯合利用多條混合不變量測試、跨環節對抗演練

矩陣的使用方式是逐列而非逐行:對一個具體系統,逐一檢查每個環節是否存在未被覆蓋的攻擊類,而非枚舉已知攻擊手法。手法會更新,環節不會。

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 證據狀態轉移

CONFLICT 單獨指向 SAFE_MODE 而非 DENY,是因為矛盾證據意味著系統對當前狀態的認知本身不可靠。此時不僅本次執行不應放行,同類執行的判定前提也已存疑,故須進入受限狀態而非僅拒絕單次請求。

3.3.2 不可壓縮性

一種常見實現將上述四態映射為布爾值:σ(e) = VALID 記為 true,其餘記為 false。該映射在放行判定上無損——四種狀態均不產生 ALLOW——但在恢復路徑上有損。

表 3-3 四態對應的處置差異

狀態系統所處境況恢復動作責任方
MISSING缺少輸入補充提交證據請求發起方
UNKNOWN無法驗證修復驗證通道、更換來源系統運維方
EXPIRED事實已過時重新採集、重新簽發證據簽發方
CONFLICT認知不一致獨立裁定、排查來源獨立第三方

命題 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 章的結論對錶達執行邊界規則的形式提出了具體要求。任何候選表達形式須同時滿足:

  1. 確定性——相同規則與相同輸入產生相同 (d, π)(Γ 的確定性性質)。
  2. 必然終止——裁決在有界步驟內完成,且最壞情況可預先計算(Final Veto 不能無限等待)。
  3. 可靜態分析——規則在部署前可被審查,其可達結論可被枚舉。
  4. 輸入封閉——規則不讀取未聲明的數據,裁決過程不產生副作用(A7 與裁決執行分離)。
  5. 可生成證明——求值過程可輸出 π 並被重放(A8)。

以這五項為判據,考察現有的五類表達形式。

表 4-1 現有表達形式與邊界語言要求的對照

形式能表達什麼主要缺口
JSON數據結構與取值只描述結構,不表達條件、關係與綁定;無求值語義,故無從生成證明
YAML同上,可讀性更好可讀性改善不改變表達能力;缺口與 JSON 相同
策略引擎(訪問控制類)主體、資源、動作三元組上的允許與拒絕判定對象是訪問請求而非最終執行對象;不表達意圖綁定與證據時效
通用編程語言任意可計算過程違反要求 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 邊界的單向性

圖中虛線標記的反向路徑不存在:現實動作一旦發生,邊界不再具備控制力。這決定了邊界必須位於動作之前而非之後,也決定了審計不能替代邊界(表 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 憲法條款及其公理依據

編號條款依據
C1EBL 面向現實執行裁決,非通用計算;任何語言能力須服務於邊界判斷P4.1
C2Runtime 只裁決,不執行外部動作:裁決過程中不得調用外部接口、修改數據、發送交易或控制設備A6
C3相同規則與相同輸入產生相同 (d, π);不得依賴隨機採樣、隱式網絡狀態、未聲明環境變量或模型臨場解釋Γ 確定性
C4UNKNOWN、MISSING、EXPIRED、CONFLICT 作為一等語義保留,不得自動轉為真,不得由默認值消解A8、P3.3
C5ALLOW 須由完整證明產生;π 須能指出成立的規則、使用的證據、綁定關係、被滿足的固定約束、策略版本與求值路徑A8
C6最終執行對象須與意圖、策略、審批、證據綁定;對象變化使既有證明失效A2、A3、A9
C7關係獨立性是一等語義,不得僅由數量推斷獨立性A7、P2.5
C8Evidence 是一等輸入,須攜帶來源、對象、時間、有效性、完整性與關聯關係;Runtime 依據證據而非上層聲明裁決A7
C9策略無副作用、必然終止、資源可計算;Runtime 須能限制最大步驟、內存、嵌套深度、證據數量與規則複雜度要求 2、3
C10可編程規則不得降低憲法規定的最低要求;P 可增加約束、縮小範圍、要求更多證據,不可反向A4、P4.2

十條中,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 的輸入封閉與輸出結構

封閉性的直接收益是可重放:給定同一輸入集,任何時刻、任何實現均可重新求值並得到同一結論。若 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 的六類對象

模型中刻意不包含"執行動作"這一對象。執行不屬於 EBL 的職責範圍——EBL 只決定候選執行是否獲得跨越邊界的資格,動作的實施由持有 cap 的邊界與下游系統完成。

4.6.2 非目標

明確 EBL 不是什麼,與明確它是什麼同等重要,因為每一項誤置的期待都會引入一類要求語言擴張能力的壓力,而能力擴張與 4.1 所立的五項要求直接衝突。

表 4-4 EBL 的非目標

EBL 不是理由
AI 編程語言它不生成行動,不描述任務,不參與規劃
工作流語言它不編排步驟,不表達流程狀態機,不處理長事務
權限語言它判定單次執行而非主體的長期資格(表 2-1)
通用規則引擎它非圖靈完備,不追求表達任意業務邏輯(P4.1)

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 沒有出錯,審批成員沒有作惡。系統只是持有了一份過期四十七秒的狀態證據。在傳統自動化設計中,這類情形通常由緩存或默認值消解,執行照常發生;而在本書的框架下,過期意味著系統無法證明當前事實仍然成立,因而不構成放行依據。

案例覆蓋的結論對應如下:

案例環節對應結論
自然語言意圖固化為意圖對象A1、D2.2.1
AI 只生成候選執行,不持有放行權A2、A6
審批綁定 hash(x) 而非業務描述A3
兩名審批者的獨立性由信任域而非數量證成P2.5
過期證據不轉為真A8
拒絕時返回失敗語義與失效位置P3.3、P4.3
失敗記錄被保留3.3.2
管理員不能臨時放寬有效期A4、C10
硬件獨立驗證而不採信上層結論A7、A10
ALLOW 附帶可重放證明A8、C5

附錄 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 公理速查

編號速記形式完整表述見
A1無可驗證意圖,則無裁決§2.6
A2Intent ≠ Execution§2.6、§2.2
A3Approval 綁定對象,而非描述§2.6、§2.3
A4Owner ≠ God:Policy 不能關閉 Constitution§2.6、§4.3
A5無否決能力,則無邊界§2.6、§2.3
A6生成方 ≠ 裁決方§2.6、§4.4
A7來源可信 ≠ 事實可證§2.6、§2.5
A8無完整證明,則無 ALLOW§2.6、§3.3
A9對象或狀態變化,證明即失效§2.6
A10無邊界放行,現實動作不可發生§2.6、§2.4

常被引用的派生命題:Signing ≠ Final Veto(P2.3);密鑰保護 ≠ 執行保護(P2.3);計數 ≠ 獨立性(P2.5);局部正確 ≠ 整體正確(P1.1)。

C.2 定義索引

術語編號一句話定義
Execution GapD1.3.1意圖至現實結果之間缺乏端到端執行約束的結構性空間
Execution ControlD2.1.1動作發生前對對象、條件、證據及其綁定進行獨立裁決的機制
Intent ObjectD2.2.1攜帶不可變約束 I.inv 的可驗證意圖結構
Intent BindingD2.2.2候選執行與意圖在 I.inv 每一項上一致的可驗證關係
Final VetoD2.3.1能力釋放前不可繞過、不可覆蓋的拒絕能力
Physical Trust BoundaryD2.4.1由獨立硬件域獨佔必要能力所構成的執行邊界
EvidenceD2.5.1攜帶類型、來源、主體綁定與時間語義的可驗證事實
Adversarial CompletenessD3.1.1在聲明的威脅與故障模型下關鍵約束仍成立的性質
Execution BoundaryD4.2.1規則與 cap 獨佔共同構成的單向控制點
ConstitutionD4.3.1不可由 P 關閉、並決定語言能力邊界的規則集合

C.3 失敗矩陣

表 C-2 證據狀態與條件求值結果

狀態含義可否滿足必要條件恢復動作
VALID已驗證且在有效期內是—
UNKNOWN無法完成驗證否修復驗證通道或更換來源
MISSING必要證據未提交否補充提交
EXPIRED曾成立,已超出有效期否重新採集或簽發
CONFLICT存在矛盾的同類證據否獨立裁定,進入 SAFE_MODE
FALSE條件由有效證據證明為不成立否變更候選執行或意圖

FALSE 與其餘四種非放行狀態的區別是實質性的:FALSE 表示系統已完成證明且結論為拒絕,其餘四種表示系統無法完成證明。前者的恢復途徑是修改請求,後者的恢復途徑是修復證據。

〔補〕關於驗證失敗的歸類。 一份簽名不匹配或來源憑據無效的證據,在放行判定上與 UNKNOWN 等價——兩者均不參與 π。但在告警語義上二者應予區分:驗證失敗通常是攻擊指示器(威脅類 X4),而無法驗證通常是通道故障(X8)。本書將其在 σ(e) 中歸入 UNKNOWN 以保持四態的最小性,同時建議實現在證明中保留 verification_failed 標記供監測使用。


全書結論 沒有完整證明,就沒有 ALLOW。

Havenlon 研究

《AI 執行工程論綱》構成了 Havenlon 執行控制架構與物理信任邊界的理論基礎。