把虛擬機隔離證明成數學定理——EC2 的形式化驗證引擎

隔離兩台共處一機的虛擬機，是雲端最底層、也最不能出錯的承諾。AWS 在 2026 年 6 月 10 日公開的這篇文章（作者 Dominic Mulligan、Nathan Chong）講的不是又一個 hypervisor 加固，而是一個結構上的轉向：他們把 Nitro Hypervisor 裡「whose sole job is isolating virtual machines (VMs) from each other」的那一塊單獨切出來，命名為 Nitro Isolation Engine，再對它做完整的形式化驗證。文章自稱這是第一個部署在商用雲、機密性與完整性都有機器可檢證明的 hypervisor。整套 Isabelle/HOL「model and proof comprise 330,000 lines of machine-checked mathematics」——規模上對標 seL4，差別是它已經在 Graviton5 上 always-on 出貨。

為什麼非得先縮小不可，文章只用一句話點破整個方法論的關鍵：通用 hypervisor 功能繁多，「that complexity makes proving correctness much more difficult」——複雜度本身就是證明的敵人。它接著給出對策：「distilling the hypervisor's critical isolation logic into a minimal component, the Nitro Isolation Engine, makes it small enough to verify and audit。」把關鍵的隔離邏輯蒸餾成一個最小元件，這個「最小」不是修辭，而是讓「驗證」這個動作在數學上由不可能變成可能的前提。值得注意原文這句話的受詞是兩個動詞：verify 與 audit。縮小不只把機器證明變得可行，也讓「人逐行審查」重新變得可能——一個幾萬行、功能交織的元件，連人工複查都無從下手，遑論機器窮盡。先把要證的對象砍到一個職責單一的核心，剩下的每一步才有機會被逐條檢查。

底下幾節依序拆開這台引擎：先看為什麼要把它縮小（separation kernel 的 policy/mechanism 分離），再看用什麼語言寫才證得動（μRust），接著是兩條互補的證明路線——功能性質走 separation logic 加 weakest-precondition，機密性走 noninterference——最後談這份證明的邊界在哪裡。先從一個互動小工具開始，因為整篇最反直覺的概念是 noninterference，而它最好用「動手撥一下」來理解。

拖動滑桿改變 VM-A 的祕密值，看 observer 投影是否變化 · 1 個祕密變數

VM-A secret = 42

兩個 state 只在 observer 看不到的 high 部分不同；step 之後 observer 能看到的投影一個 bit 都沒變。observer 因此無法從這步推回祕密值——indistinguishable before、indistinguishable after。

把要證的東西縮小：separation kernel 的 policy／mechanism 分離

形式化驗證最大的敵人是程式碼的尺寸——要證的狀態空間隨著功能膨脹，幾萬行的通用 hypervisor 在數學上幾乎無法窮盡。AWS 的第一步因此不是「證 hypervisor」，而是「把 hypervisor 裡真正需要被信任的那一小塊切出來」。這一塊就是 Nitro Isolation Engine，文章對它的定義一句話帶過卻很關鍵：它是 Nitro Hypervisor 的一個元件，唯一職責就是把 VM 彼此隔開。其餘所有事——要不要隔離、怎麼配資源、排哪台 VM——都不是它管的。

這個切法有個名字：separation kernel。文章引 John Rushby 在 1981 年提出的這個術語——「a minimal OS component that partitions a system into isolated compartments」，一個把系統劃分成彼此隔離的隔間的最小 OS 元件——並點出它的核心招式：「the key idea: separate policy from mechanism。」把決策與執行劈開，正是縮小證明範圍的那一刀。文章把 separation kernel 的特性講得很乾淨：「A separation kernel does not decide what to isolate, how to allocate resources, or which VMs to schedule: those decisions are made elsewhere. Instead, it focuses solely on enforcing isolation.」決策（policy）與執行（mechanism）被劈成兩半，被驗證的只有 mechanism 那一半。policy 那一半——VM 的建立、資源配置、遷移、排程——仍由 Nitro Hypervisor 處理，但它的權限被收掉了：「it is now deprivileged and must ask the Nitro Isolation Engine to perform any operation touching guest state.」

這一刀為什麼能讓證明變得可行，值得想清楚。policy 那一半的程式碼通常最龐雜、改得最頻繁——排程策略會調、資源配額會變、遷移邏輯會演化。如果這些都得跟著被重新證明，驗證工作會被功能迭代拖垮。把 policy 推到證明範圍之外、只證那個小而穩定的 mechanism，等於把「需要被信任、也需要被證明」的表面積壓到最小。換句話說，policy/mechanism 分離不只是架構美學，它直接決定了 330,000 行證明覆蓋得完還是覆蓋不完。

文章自己也把這層因果寫得很白：把職責收斂到「只 enforce 隔離」之後，「this clarity of purpose makes separation kernels much simpler to implement than full OS kernels.」——這種目標的純粹，讓 separation kernel 比完整的 OS kernel 容易實作。這句話的重量在於它把「容易驗證」往前推了一步：一個東西之所以好證，往往是因為它一開始就被設計得夠簡單；驗證不是事後硬加上去的一道工序，而是在「要不要塞進這個功能」的每個決策點就已被預先考慮。separation kernel 的單一職責，是先在實作層面把複雜度壓下來，證明工具才有施力的餘地。

這句「deprivileged」是整個架構的支點。在傳統 hypervisor 裡，管排程的那塊程式碼同時握有改寫 guest 記憶體的權力，於是它的任何 bug 都可能變成跨 VM 洩漏。Nitro 把這兩件事分開後，hypervisor 要碰 guest state 只能透過 Isolation Engine 的受控介面提出請求；可信任計算基（TCB）因此收縮到只剩 Isolation Engine 一個元件。下面的圖把這個 policy/mechanism 的責任邊界攤開，點任何一個方塊看它負責什麼、刻意不知道什麼。

click a layer

Nitro Hypervisor · policy

仍負責所有決策——VM 的建立、資源配置、遷移、排程。但它「is now deprivileged」：要碰 guest state，只能向 Isolation Engine 提出請求，自己沒有直接改寫 guest 記憶體的權力。

刻意不持有：直接觸碰 guest state 的特權。它的 bug 不再能直接變成跨 VM 洩漏。

Nitro Isolation Engine · mechanism

唯一職責是 enforce 隔離。它不決定要不要隔離、配多少資源、排哪台 VM——「those decisions are made elsewhere」。整個可信任計算基收縮到這一個元件，也只有這一個元件被 330,000 行 Isabelle/HOL 證明覆蓋。

刻意不負責：policy。決策邏輯留在上層，引擎只執行受控操作。

Guest VMs · 被隔離的對象

兩台共處一機的 guest。證明要保證的就是：A 的祕密不流向 B、B 不能竄改 A——「only authorized information flows can occur」。guest 之間沒有任何直接通道，所有跨界操作都必須過 Isolation Engine。

刻意不知道：彼此的存在。從 guest 的角度，它獨佔整台機器。

把 TCB 縮到一個職責單一的元件，是這整套工作能成立的前提。seL4 當年證的是一個微核心，這裡證的是一個更專一的 separation kernel——小到讓 330,000 行證明能把它的每條執行路徑都覆蓋。值得記住的是：縮小範圍不是偷工，而是讓「證明」這個動詞在工程上變得可能的唯一辦法。

μRust：先把語言砍到可推理的子集

就算元件夠小，Rust 本身對形式推理仍然太大。Rust 的 trait、dynamic dispatch、generic 單態化這些特性讓編譯器很強，卻也讓「對每一條程式路徑都給出數學規格」變得棘手——dynamic dispatch 意味著呼叫點背後可能是任意實作，推理時得把整個可能集合都納入。AWS 的選擇是先把語言縮小：他們形式化了 Rust 的一個 core subset，叫 μRust。

文章對 μRust 的定義同時講了它的能力與它的取捨：「μRust is a restricted subset of the Rust programming language that is expressive enough to write the Nitro Isolation Engine but amenable to formal reasoning because we deliberately excluded advanced Rust features, such as traits and dynamic dispatch.」表達力夠寫整個 Isolation Engine，但 trait 與 dynamic dispatch 被刻意排除。換句話說，引擎是用一個「故意比 Rust 笨一點」的 Rust 寫的——笨到每個呼叫點都是靜態確定的、每條路徑都能被符號化地走完。這跟 μRust 名字裡的 μ 是同一個意思：把語言收斂到一個能被完整建模的核心。

μRust 不是憑空造的語言，而是 Rust 的一個 core subset 的形式化——文章稱之為「formalization of a core subset of the Rust language, called μRust」。這個分寸拿捏很關鍵：它必須仍然是 Rust，工程師才能真的用它寫出整個 Isolation Engine、也才能享受 Rust 既有的記憶體安全保證；但它又必須比完整的 Rust 收斂，數學上的規格才寫得出來。「expressive enough to write the Nitro Isolation Engine but amenable to formal reasoning」這句話裡的 but，標的就是這條張力線——表達力與可推理性之間，他們選了一個能同時站住兩腳的點。

這個取捨值得一般 Rust 工程師留意：它說明了「可驗證」和「好用」之間真實存在張力。trait 與 dynamic dispatch 正是日常 Rust 抽象能力的來源，而它們恰恰是形式推理最難啃的部分——dynamic dispatch 意味著一個呼叫點背後的實際實作要到執行期才定，推理時無法在靜態階段把「這裡到底跑哪段程式」釘死，整個可能集合都得被攤進證明。把可驗證性擺第一，就得在語言層面先付出表達力的代價——這不是 Rust 的缺陷，而是「要證明」這件事對任何語言都會提出的要求。

separation logic 加 weakest-precondition：證功能與記憶體安全

語言收斂之後，第一條證明路線處理的是「功能性質」：程式做對了該做的事、而且不會踩到記憶體錯誤。文章列出的三個目標是 absence of runtime errors、memory safety、functional correctness。用的工具是兩件配套的東西——Separation Logic 與 weakest-precondition calculus。前者「for precisely capturing specifications」，後者是把規格推回到程式入口的演算法。

separation logic 之所以是這類證明的標準武器，文章一句話講明了它的本行：「a logic designed to reason about low-level pointer-manipulating programs」——一套專為推理低階指標操作程式而設計的邏輯。它天生擅長講「這塊記憶體歸我、那塊記憶體歸你、兩者不重疊」。它的核心連接詞把堆的兩個不相交部分接起來，讓「A 的操作不會動到 B 的記憶體」這種敘述可以被形式化地寫下、被推理。對一個職責是「把 VM 隔開」的引擎來說，這種「不相交」的語言剛好對味——隔離本質上就是一句記憶體分離的斷言。一個處理 guest 記憶體頁、指標滿天飛的引擎，正是 separation logic 最該被派上場的地方。

weakest-precondition 則是反向工作的。給定「執行完這段程式後，這個 postcondition 要成立」，它計算出「執行前最弱需要成立的 precondition 是什麼」，一路把規格從程式末端推回到入口。如果入口的條件能被滿足，整段程式的正確性就成立。但這裡的「正確」是一個比直覺更強的版本。文章把 contract 指定的目標明確界定為 total correctness：「in all states that satisfy the precondition, the program always terminates, and the resulting state satisfies the postcondition.」拆開看是兩件事綁在一起——在所有滿足 precondition 的 state 下，程式不只「算出對的結果」（結果 state 滿足 postcondition），還必須「一定會停下來」（always terminates）。partial correctness 只要求「如果停了，結果是對的」；total correctness 把「會停」也納進證明義務，等於把無窮迴圈、卡死這類失敗模式一併排除。

而 total correctness 真正划算的地方，是它一次帶出三個性質。文章接著說：「this total-correctness condition also means the program is memory safe and free of runtime errors.」一旦把 total correctness 證下來，memory safety 與 absence of runtime errors 不是另外再證的兩件事，而是同一個條件的副產品——三個性質被一次性鎖在一起。道理在於：要求程式在每條路徑上都正常終止並滿足 postcondition，等於把讀寫越界、解參空指標、觸發 runtime error 這些執行全部排除在外，因為它們要麼讓程式停不下來，要麼讓結果 state 違反規格。把這些接起來——用 separation logic 寫規格、用 weakest-precondition 推回去——就得到 memory safety 與 functional correctness 的機器可檢證明。下面這張表把兩條證明路線各自的工具與所證性質擺在一起對照。

兩條互補的證明路線——左半證「程式做對了」，右半證「祕密沒洩漏」。性質與技術名稱皆取自原文。

證明路線	所證性質	核心技術
功能驗證	absence of runtime errors	μRust 形式化 · separation logic 寫規格
功能驗證	memory safety	separation logic（堆的不相交斷言）
功能驗證	functional correctness	weakest-precondition calculus
機密 / 完整性	only authorized information flows can occur	noninterference · indistinguishability preservation

支撐這條路線的證明基礎設施，AWS 已經在 2025 年開源——文章把它定位為「a general-purpose proof infrastructure that we open-sourced in 2025 as the AutoCorrode library」。兩個字眼值得記住：general-purpose 與 open-sourced。把 μRust 程式接上 separation logic 與 weakest-precondition 的這套機械，不是只活在 Nitro 內部、用完即棄的一次性產物，而是被設計成可套用到其他驗證對象、且已經公開的通用基礎設施。對一個訴諸「機器可檢」的成果來說，工具公開本身就是可信度的一部分。

noninterference：為什麼「功能正確」還不夠

功能驗證證完，還缺一塊最關鍵的——機密性。這兩者的差別常被混淆：一段程式可以「完全正確」地完成規格，同時把一台 VM 的祕密悄悄寫進另一台看得到的位置。功能正確管的是「做對了該做的事」，機密性管的是「沒做不該被看到的事」，後者不蘊含於前者。所以文章用了一條完全不同的證明路線，目標一句話：「Only authorized information flows can occur。」

這條路線的形式工具是 noninterference，證明策略叫 indistinguishability preservation。文章先給它一個定位：「Noninterference is the idea of indistinguishability preservation that we use to make confidentiality and integrity mathematically precise.」——它的作用，是把「機密性」「完整性」這兩個本來模糊的字眼，變成數學上精確、可被機器檢查的命題。機密性與完整性在這裡是一體兩面：前者是「祕密不外流」，後者是「外界不能竄改」，但都能被收斂成同一句 information-flow 斷言——只有被授權的流動可以發生。

它的核心直覺，文章講得異常清楚，值得逐字讀：「if two states are indistinguishable to an observer before a step, they must remain indistinguishable afterward. The intuitive reason why this captures confidentiality is that the observer has learned nothing new because of the step.」翻成白話：取兩個只在「祕密」上不同、但在「observer 能看到的部分」完全相同的 state，讓引擎走一步；如果走完之後 observer 看到的部分還是相同，那 observer 就無從分辨剛才那一步背後的祕密是什麼——它什麼都沒學到。這個「學到 nothing new」是關鍵措辭：機密性不是「祕密被加密」或「祕密被藏好」，而是更強的「祕密的任何值都不會在 observer 可見的行為上留下差別」。文章開頭那個互動小工具示範的正是這件事：你撥動 VM-A 的祕密值，observer 投影恆等於兩邊一致。

要對「每一步」都成立才算數，而這正是建模深度開始咬人的地方。文章舉了 PSCI_CPU_ON 這個操作當例子——它「captures what happens when an executing guest virtual CPU tries to turn itself on (an erroneous request)」，也就是一個正在跑的 guest CPU 試圖開啟自己這種錯誤請求。這個例子選得好，是因為它走的是錯誤路徑而非快樂路徑：一個已經在跑的 virtual CPU 要求把自己打開，本身就矛盾。引擎的處理也被規格如實寫下——「the Nitro Isolation Engine sees that, to act as the caller, the virtual CPU must be turned on already, and it therefore returns a defined error code, AlreadyOn.」要能當 caller 發出請求，該 virtual CPU 顯然已是開著的，於是引擎回傳一個定義好的 error code AlreadyOn。注意這裡沒有 panic、沒有未定義行為，連錯誤都有明確的、被規格覆蓋的結果——這正是「absence of runtime errors」在一個具體操作上的樣子。

光是這個錯誤路徑的規格就相當複雜，文章的解釋是：「the complexity in the specification is a reflection of the depth of our modeling and the fact that several other error checks must already have been performed.」規格複雜不是因為寫得囉嗦，而是因為要走到這一步，前面已經必須通過好幾道 error check——模型把這些前置條件都如實納進來了。這句話反過來讀更有意思：規格的複雜度，是建模忠實度的副作用。一個偷懶的模型可以把這些 check 抽象掉、讓規格看起來乾淨，但那等於在證明裡偷偷假設「前面都沒出錯」；Nitro 把每一道 check 都顯式建進模型，於是 noninterference 必須對「連這個錯誤請求都被正確擋下」一併成立。每一個操作、包括每一條錯誤路徑，都得單獨扛起 indistinguishability 被保住的義務——這正是為什麼前面要把語言縮成 μRust、把元件縮成 separation kernel。

對讀者來說，這裡的 takeaway 是：noninterference 不是一句口號，而是一個要對引擎的每一個操作（包括所有錯誤路徑）逐一驗證 indistinguishability 被保住的義務。下圖把功能與機密兩條路線疊成一座證明階梯，從 μRust 的語言底座一路堆到 noninterference 的頂層性質。

這份證明保證了什麼、沒保證什麼

形式化驗證最容易被誤讀的地方，是把「證明了 X」聽成「整台機器無懈可擊」。文章在這點上相當誠實，邊界劃得很清楚，值得逐條記下來。

第一，被證的是 Nitro Isolation Engine，不包含被 deprivileged 的 hypervisor。policy 那一半留在證明範圍之外——這正是 separation kernel 設計的目的：把需要被信任的東西縮到最小，但「縮到最小」反過來說就是「最小之外的東西沒被證」。第二，並發程式碼的推理方法尚未在這篇展開：文章把「how we handle reasoning about concurrent code」連同 conformance testing 一起列為「we're excited to share in future posts」，意思是這次公開的成果裡，這部分的方法論還沒攤出來。第三，也是最容易被忽略的——形式化驗證證的是「模型符合規格」，它不涵蓋 side-channel 攻擊，也不涵蓋硬體層的漏洞。一個在數學上完美隔離的引擎，仍可能被 cache timing 之類的旁路洩漏資訊，因為那條通道根本不在被建模的狀態空間裡。下圖把「圈內已證」與「圈外未涵蓋」攤開對照。

放回脈絡看規模感：文章說它「comparable in scale to seL4, the landmark project that first demonstrated that realistic operating-system verification was feasible and was an inspiration for our own work.」seL4 是第一個證明「現實作業系統驗證可行」的里程碑，AWS 直接承認它是這項工作的 inspiration。把 330,000 行放到這個座標上才讀得出分量：這是與學界公認最硬的形式化驗證里程碑同一量級的工程。要注意原文只說「comparable in scale」，並沒有給出 seL4 的具體行數來逐項對照——它比的是量級。

真正的差別不在規模而在落地：「unlike seL4, the Nitro Isolation Engine is designed for a commercial cloud environment and ships on production hardware as an always-on feature for Graviton5 users.」seL4 證明了「可行」，但它本質上是研究與高保證場景的微核心；Nitro Isolation Engine 則從一開始就為商用雲設計、跑在量產硬體上、而且 always-on。always-on 是這份成果對普通使用者最直接的意義：不是一個要你去開的選項、也不是高階方案才有的加值，而是預設就在那裡、不需要任何操作的底層保證。具體說，Graviton5 的 M9g／M9gd 是第一批用上新 Nitro Isolation Engine 的 instance type——在這些機型上跑 EC2 的人，VM 隔離這條性質背後從此有一份機器可檢的數學證明撐著。

What this enables：把「VM 隔離」從一個靠測試與審查支撐的工程信心，變成一條有 330,000 行機器可檢數學撐著的性質——前提是你也記得它的邊界：證的是隔離引擎，不是整台機器，並發、side-channel、硬體漏洞都還在圈外等後續。