Nitro 把隔離拆成可證明的數學

AWS split Nitro’s isolation logic into a tiny Rust kernel and proved VM isolation with machine-checked math.

我看雲端安全系統看久了，最怕的不是 bug，最怕的是那種「應該沒事啦」的架構。隔離邏輯跟排程、驅動、產品特化、AWS 自家 hook 全黏在一起，然後有人拍拍胸口說 VM 會被隔開。拜託，我真的看過太多這種故事。不是團隊不認真，是東西一大包之後，你根本沒辦法乾淨地推理哪一段在管邊界、哪一段只是順手做事。每次改動都像在賭，這種安全軟體我很難放心。

這次讓我停下來看的，是 Amazon Science 這篇 EC2’s formally verified ‘isolation engine’ provides mathematical assurance of virtual-machine isolation。作者是 Dominic Mulligan 跟 Nathan Chong。文中最刺眼的不是雲端宣傳，而是他們真的把隔離邏輯拆出去，縮成一個小核心，再用機器檢查的數學去證明它。Amazon 還說模型和證明總共是 330,000 行，Nitro Isolation Engine 是第一個部署在商業雲環境的 formally verified hypervisor。這個數字我不會拿來灌水，但它很能說明一件事：這不是玩具。

別拿整個 hypervisor 去做證明，那是在自找麻煩

“Splitting the ‘separation kernel’ off from the rest of the Nitro security system … enabled its formal verification.”

翻譯一下就是：他們沒有硬著頭皮去證明整個 hypervisor，而是先承認一件事，整包系統太肥，根本不適合直接做形式驗證。這個判斷很老實，也很重要。因為一旦你的系統同時混著隔離政策、裝置處理、排程、遷移、AWS 特化邏輯，你證明的就不再是 kernel，而是一個超大應用程式，只是它剛好跑在 VM 底下。

Amazon 的文章裡寫得很清楚：原本的 Nitro Hypervisor 同時管隔離、驅動、AWS-specific 功能，這種架構一看就知道會把 proof target 撐爆。後來他們把真正重要的那塊，也就是 VM 分離這件事，抽成獨立元件 Nitro Isolation Engine。這才是他們能下手證明的目標。

我自己做系統設計時也常看到這種爛局。你叫團隊「把安全性證明出來」，大家最後都會偷偷縮小範圍，只挑一個 invariant、一條 data flow、一個邊界。Amazon 只是把這件事明講出來，不再假裝整包都能一起證。這差很多。前者是 proof plan，後者是祈禱。

實操上我會這樣做：先找出那個一出錯就會變成資安事故的子系統，再把其他東西從它身上剝掉。如果你怎麼切都切不小，通常不是你不會證明，是你的架構根本不配被證明。這句話很難聽，但常常是真的。

• 把 enforcement 跟 policy 分開。
• 把 proof target 壓到最小。
• 讓其他模組請求核心幫忙，不要自己碰安全邊界。

這裡也順便點到 separation kernel 的老派價值。John Rushby 在 1981 年提出這個詞，講的就是一個最小 OS 元件，專門把系統切成彼此隔離的 compartment。Amazon 只是把這個老觀念搬到雲端，場景更大、程式碼更髒，但原理沒變。

Rust 不是魔法，少用它才是重點

Amazon 說 Nitro Isolation Engine 是用 Rust 寫的，但不是整個語言都拿來用，而是挑了適合形式推理的子集。這點我很有感。很多團隊嘴上說想用 Rust 是因為「比較安全」，結果一上手就把所有 feature 都打開，最後 proof story 還是卡死。

重點不是「Rust 讓一切可驗證」。重點是「把語言限制到可推理」。這兩句差很多。Amazon 還把 Rust 的核心子集形式化成 μRust，收進開源的 AutoCorrode。這代表他們不是只在口頭上說「我們用了安全語言」，而是真的替程式碼建立一個 proof-friendly 的語意模型。

我很喜歡這種做法，因為它承認一個很多人不想面對的事實：驗證工作有一半是在處理語言本身，不是在處理邏輯。語言太多 sharp edge，你的 proof 就會一直追著 aliasing、undefined behavior、編譯器假設跑。到那時候，難的不是 theorem prover，是你的 programming model 根本不乾淨。

實操寫法很直接：如果你想驗證某個子系統，先定義 safe subset，再寫 code。不要先從語言手冊開始讀。先從這個子系統實際需要哪些操作開始，然後把其他功能禁掉。很煩，對，沒錯；但這通常才是能落地的方法。

• 先寫 subset 規格，再寫實作。
• 資料結構越普通越好。
• unsafe escape hatch 要少，而且要明顯。

Amazon 這次最值得抄的，不是 Rust 這個名字，而是「先收斂語言，再談證明」的態度。程式碼的意義變小了，證明才有機會變得可做。

規格要白紙黑字，不能靠大家默契

Amazon 把驗證拆成兩塊：specifications 跟 proofs。這聽起來像廢話，直到你真的開始寫 spec，才會發現自己以前的安全敘述到底有多少是靠默契撐著。

他們證明的性質分成四類：confidentiality、integrity、functional correctness，還有 absence of runtime errors。這個切法我覺得很合理，因為 VM 隔離本來就不是「程式沒 crash」而已。真正重要的是，別的 VM 不能偷看你的東西，也不能亂改你的狀態。

也就是說，這個 engine 不只是「寫得比較安全」，而是有 machine-checked 的理由去說：guest memory 重新使用前會被清掉、只有授權過的資訊流可以發生、實作行為符合規格。這跟「我們有 review 過」不是同一個層級的句子。

我以前看過太多 code review 裡的「secure」其實只是「我們沒看到明顯問題」。那真的不算安全敘述。形式化規格的好處，就是逼你把「authorized」「reuse」「guest state」這些詞講清楚，不能再靠大家腦補。過程很痛，因為它會把模糊地帶全翻出來；但那也正是 bug 常躲的地方。

實操上，我會先用白話把性質寫乾淨，完全不要行銷腔。接著把每條性質變成可檢查的條件。你如果說不出什麼情況算違反，那你其實還沒有 spec。

想看這套東西背後的工具鏈，可以直接看 Isabelle/HOL、AWS Nitro，還有前面那篇 Amazon Science 文章。你選什麼 formal language，會直接影響你能說出什麼樣的保證。

他們證明的是邊界，不是整個雲

我覺得 Amazon 這次最成熟的地方，是 scope 夠清楚。Nitro Isolation Engine 不是整個雲，它是 VM 隔離的 enforcement point。Nitro Hypervisor 仍然管 policy，像 VM 建立、資源分配、遷移、排程這些事，但它被 deprivilege 了，碰 guest state 前得先問 engine。

這種架構很乾淨。policy layer 可以很吵、很複雜、很產品導向；enforcement layer 則維持小、可審、適合證明。對客戶來說，這也給了一個具體的信任錨點：真正守 VM 邊界的那個元件，才是被數學處理過的地方。

我看過太多團隊把這條線搞糊。嘴上說整個平台都安全，但實際上 enforcement logic 散在一堆服務裡。出事後大家只會互踢皮球，因為沒人知道哪一層才是最後決策者。Amazon 的做法至少避免了這種亂象。

實操寫法是：如果你有一條安全邊界，就只允許一個元件做最後裁決。其他模組只能提 request，不能直接碰受保護狀態。這樣測試比較好寫，audit 比較好看，證明也比較有機會成立。

• policy 放外層。
• enforcement 放核心。
• 所有狀態變更都要穿過同一個核心。

另外一個我在意的細節，是 Amazon 說 Nitro Isolation Engine 對 Graviton5 使用者是 always-on。這表示它不是 demo mode，也不是某個特殊開關，而是實際 production path。這很重要，因為 proof work 很容易在 paper 裡看起來很漂亮，真正在流量下能不能站住腳，才是另一回事。

330,000 行不是炫耀，是成本帳單

Amazon 說 Isabelle/HOL 的模型和證明總共 330,000 行，規模跟 seL4 差不多。這個數字如果拿來當噱頭，我覺得很無聊；但如果拿來當成本帳單，我反而覺得誠實。因為它告訴你：要對一個真的有用的系統做嚴格保證，本來就不會是幾十行定理那麼輕鬆。

這裡提到 seL4 很合理，因為 seL4 長年就是大家講 proof-based OS 時最常拿來當例子的專案。Amazon 等於是在說：我們現在把這種等級的形式化工作，搬進商業雲 hypervisor，而且還是跑在 production hardware 上。

這件事真正的意思，不是 proof 要維持微型，而是你要把「需要被證明的那一小塊」維持得夠小。證明本身可以很大，但 proof target 必須夠小，否則就會直接爆掉。這是完全不同的工程折衷。

我看過很多人低估 proof size，因為他們腦中以為 theorem 就是一小段漂亮文字。不是。工業級 verification 是工程資產，要命名、要結構、要維護。這種東西不是研究展示品。你如果對這件事不舒服，我反而覺得正常，因為安全聲明本來就不該輕飄飄。

實操上不要問「我們能不能週末做完證明？」要問的是「系統裡哪一塊值得這個等級的 rigor？」先定義範圍，再把 proof 當正式工程排進去，不要把它當學術表演。

如果你想往下挖，Amazon 文章有提到 white paper 跟 re:Invent 2025 的 talk。這些材料通常會把 scope、assumption、限制講得比 blog 更清楚。我如果要評估這種保證是不是我真的需要，我會先看那裡。

這篇真正值得學的是架構上的謙虛

我覺得整個故事最有價值的地方，不是他們用了 Isabelle/HOL，也不是因為 Rust，也不是 330,000 行這個數字，而是他們承認原本的系統太大，不能直接拿來驗證。所以他們先改架構，改到 proof 變得可能。

這種態度很少見。很多團隊把 formal verification 當成可以外掛的 badge，架構不動、複雜度不動、邊界不動，然後叫 theorem prover 幫忙蓋章。順序完全錯了。架構必須先配合。

Amazon 的 policy/enforcement split 就算你永遠不做 proof，也一樣有價值。它讓責任更清楚、耦合更少、審查目標更小。形式化驗證只是把這些好處變得更難裝沒看到而已。

實操上，我會這樣問團隊：當一個系統太複雜、太難推理時，不要只加測試。先問哪些東西可以拆開、降權、或收斂成更小的 trusted core。如果答案是「沒什麼能拆」，那通常就是問題本身。

而且對雲端客戶來說，真正該在意的不是 proof 本身，而是讓 proof 成立的那個架構。因為產品不是證明，產品是那個能被證明的系統設計。

可抄的模板

# 形式化驗證友善的安全核心模板（可直接改成你們的設計稿或 RFC）

## 1) 先定義邊界
- 用一句話寫出這個元件負責的安全性質。
- 範例："This component enforces isolation between tenants/VMs/processes."

## 2) 把 policy 跟 enforcement 分開
- Policy 決定要做什麼。
- Enforcement 決定能不能做，並且真的執行狀態變更。
- Enforcement core 必須是唯一能碰敏感狀態的地方。

## 3) 把 trusted core 壓到最小
- 把跟安全邊界無關的東西搬出去：
  - scheduling
  - device drivers
  - feature flags
  - product-specific glue
- 留下的只應該是「沒它就沒有安全保證」的程式。

## 4) 限制實作語言子集
- 先定義 safe subset。
- 禁掉會讓推理變難的語言特性，除非真的必要。
- 優先選簡單資料結構與明確狀態轉移。

## 5) 寫出可機器檢查的 spec
每條性質都要寫：
- 必須永遠成立的事
- 什麼算違反
- 作用範圍有哪些 state / input
- proof 可以接受哪些 assumptions

## 6) 至少證明四類性質
- Confidentiality：沒有未授權資訊流
- Integrity：沒有未授權狀態修改
- Functional correctness：實作符合 spec
- Safety：沒有 runtime error、沒有 memory unsafety

## 7) 讓外層系統只提 request，不直接裁決
- 外層可以建立、排程、分配、遷移。
- 但它不能自己碰受保護狀態。
- 每個敏感動作都要經過 core 的 allow/deny 或由 core 直接執行。

## 8) 把 proof 當工程資產
- 清楚寫 scope。
- 清楚寫 assumptions。
- 清楚寫沒證明什麼。
- 把 proof 當需要維護的 artefact，不是一次性展示品。

## 9) 架構草圖
[Policy layer]
- VM creation
- Resource allocation
- Scheduling
- Migration
- Product-specific features

        |
        v

[Verification boundary]
- Authorization check
- State transition
- Guest-memory scrubbing
- Isolation enforcement
- Error handling

        |
        v

[Protected state]
- Guest memory
- VM metadata
- Isolation metadata
- Device access state

## 10) Spec 起手式
- The enforcement core never allows two tenants to observe each other’s protected state.
- Any reused guest memory is scrubbed before reassignment.
- Every state transition is authorized by the core.
- The implementation never performs an out-of-bounds access.
- The implementation never dereferences invalid memory.

## 11) Review checklist
- Proof target 能不能用一段話講完？
- Outer system 壞掉會不會直接破壞 isolation？
- 每個敏感轉移是不是都走同一個 core？
- runtime / memory safety 有沒有算進主張裡？
- assumptions 有沒有寫出來，而不是默認大家懂？

## 12) 給團隊的 prompt
"找出最小的子系統。只要把它證明對了，就能對安全邊界有信心。把其他東西都移出 proof target。接著定義要證明的性質、允許的語言子集，以及我們願意接受的 assumptions。"

我會抄 Amazon 的不是規模，是紀律：先把安全邊界拆出來，然後逼實作去配合 proof，而不是反過來。這才是一般團隊真的用得到的地方。

來源主要來自 Amazon Science 這篇文章：amazon.science。我上面的大方向解讀、拆解順序跟模板整理是我自己的整理；技術事實與數字則以原文為準。