測試跨不過的那道極限
到此你已遇過系統程式設計師用來找臭蟲的每一件武器：在一次壞記憶體存取正發生時抓住它的 Valgrind 與消毒器、把上百萬隨機輸入丟向程式碼好絆倒它的模糊測試、在你執行之前就標出可疑模式的靜態分析。它們很棒，你也該全部用上。但它們共享一道天花板，由 Edsger Dijkstra 講得最尖銳：測試能顯示臭蟲的存在，卻永遠無法顯示它們的不存在。一個跑了十億個輸入、什麼也沒找到的模糊測試器，對第十億零一個輸入什麼也沒證明。對一般軟體那道天花板是可以忍受的。但對最底層的程式碼——每一個其他程式都信任的那個核心、那條系統呼叫路徑、心律調節器或飛機或硬體安全模組裡的程式碼——「我們測了很多、看起來沒事」是一個令人害怕的止步之處。
形式驗證跨過了那道天花板。你不是在某些輸入上執行程式碼，而是寫下一份「程式碼必須做什麼」的數學規格——每一個輸入、每一個狀態——然後建構一個由機器查核的證明，證明真實的程式碼對所有這些情況都滿足那份規格。那個證明不是一個通過的測試；它是一個邏輯論證，就和「質數有無限多個」的證明一次涵蓋了每一個質數、而非你恰好試過的那幾個是同一個意思。當一個證明走通了，你就以確定性、而非信心，排除了一整個類別的失敗。這就是形式驗證系統背後的想法，而本篇其餘部分會用史上出貨過的最著名例子把它變得具體。
seL4：一個被證明正確到組合語言的微核心
那個里程碑是 seL4，它的第一份正確性證明在 2009 年由澳洲 NICTA 的一個團隊完成。它是一個微核心——回想核心那級，一個微核心在特權模式裡幾乎什麼都不留。它做記憶體映射、執行緒與訊息傳遞，並把檔案系統、驅動程式與網路堆疊都推到普通的使用者行程裡去。那份極簡正是讓驗證成為可能的東西：一個像 Linux 那樣的單體核心有數千萬行，遠遠超出任何證明工作的能力，但 seL4 的核心大約是一萬行 C。小到一個英勇的團隊能對穿過它的每一條路徑都證明些什麼——而他們做到了。
究竟證明了什麼？有好幾層，而那份分層正是巧妙之處。首先有一份抽象的規格——一個對「每一個核心操作應該做什麼」的精確數學描述。然後有那份 C 程式碼。核心定理是一個精煉（refinement）證明：它顯示那份 C 實作從不做任何規格不允許的事——程式碼的每一個行為都是規格的一個被允許的行為。在那之上坐著一些你直接在乎的性質的證明：這個核心永遠不會對一個空指標或野指標解參考、永遠不會溢位一個緩衝區、永遠不會撞上未定義行為、永遠不會發生一個它無意造成的整數溢位。換句話說，填滿這整座階梯其餘部分的那一整群臭蟲——區段錯誤、記憶體洩漏、釋放後使用——被證明在這個核心裡對任何輸入都不可能發生。
然後他們又往下走了一層，那一部分令系統程式設計師驚嘆。一個 C 層次的證明仍信任編譯器——萬一 gcc 自己把正確的 C 誤譯成了錯誤的機器碼呢？所以 seL4 團隊也證明了一個二進位層次的精煉：那份真正編譯出來的機器碼、CPU 真正執行的那些位元組，忠實地實作了那份 C 語意。那就堵上了那道彷彿規則與激進最佳化原本可能藏進一個臭蟲的縫隙。那條鏈從抽象規格、到 C、到載入器擺進記憶體的那個二進位檔，毫不間斷地貫通——一個從意圖到指令的連續證明。
那個證明倚靠在什麼之上——以及作為骨幹的能力（capability）
若讓你以為 seL4 在某種絕對意義上沒有臭蟲，那會背叛這座階梯的誠實。那個證明有假設，而一個認真的工程師會學著把它們背出來。它假設硬體照它的模型所說的那樣運作——最初的證明並未涵蓋推測旁路，因為那些利用了模型根本沒描述的微架構行為。它假設那一小段手寫的組合語言（C 證明搆不到）是正確的，也假設那個證明輔助器本身是健全的。這些都沒讓那份成就變小；它讓它變得可被檢視。驗證的價值恰恰在於：被信任的那些假設被明確地寫了下來，一份簡短而可審視的清單，而不是隱含地散落在一萬行沒人能一次裝進腦袋的程式碼裡。
seL4 不只被驗證；它還是以能力為基礎的（capability-based），而這兩者美妙地相合。從單核（unikernel）那篇的鄰近處你也許已隱約感到這個想法，但這裡把它直說：在一個能力系統裡，一個執行緒能碰一項資源——一個記憶體框、一個端點、另一個執行緒——的唯一方法，是持有一個無法偽造的權標，一個能力，它指名那個物件以及它所允許的操作。沒有環境權限、沒有「我是 root 所以我什麼都能做」。一個執行緒能做的恰好是它的能力所說的、一件也不多。把這拿來和你早先學的使用者／核心與以 uid 為基礎的模型相比，在那裡一個行程的權力是「它是誰」的一個性質；在這裡權力是「它持有什麼權標」的一個性質，而權標能被精確地發出、收窄與撤銷。
為什麼這個配對如此要緊？因為能力讓隔離成為一件你能精確陳述、因而能證明的事。如果元件 A 不持有任何能搆到元件 B 記憶體的能力，那麼 A 可被證明地無法讀取或損毀 B——不是「我們找不到辦法」，而是「沒有辦法存在」。這讓 seL4 能承載強的完整性與機密性定理：資訊除了沿著能力明確授權的通道，無法在元件之間流動。那恰好是一個安全攸關或保安攸關的系統所想要的性質——一個被驗證的微核心去執行「一個盒子裡被攻陷的網路驅動程式無法搆到另一個盒子裡的飛控邏輯」，憑的是一個證明，而不是一份希望。
Rust-for-Linux：靠建構方式來轉移那份重擔
seL4 用一個高昂的代價買來了完全的確定性：一個極小的核心，加上數年的專家證明勞動。那個代價對 Linux 而言是付不起的——數千萬行、數千名貢獻者、每天都在演進。所以另一個前沿下了一個完全不同的賭注。與其在事後證明一個龐大的既有 C 程式碼庫正確，Rust-for-Linux 問的是：如果我們用一種「整類臭蟲靠建構方式就不可能發生」的語言來寫新的核心程式碼呢？它在 2022 年併入了主線 Linux 核心，讓驅動程式與模組能在 C 之旁用 Rust 來寫。動機是那個冰冷的統計：在大型 C 與 C++ 系統裡，大約三分之二的嚴重保安漏洞是記憶體安全臭蟲——正是這整座階梯教你去害怕的那一族。
Rust 是如何在沒有一個核心無法忍受的垃圾收集器或執行期的情況下，交付出那一點的？靠的是 Rust 那級的所有權與借用檢查器機制，完全在編譯期強制執行。那個核心想法是型別系統靜態地追蹤「誰擁有每一塊記憶體、誰被允許參照它」，並禁止那些會造成釋放後使用、重複釋放與資料競爭的模式——編譯器乾脆拒絕建構可能犯下這些錯的程式碼。關鍵是這是零成本的：那些檢查發生在編譯期間、並從執行中的二進位檔裡消失，使它和等價的 C 一樣精瘦。你付出的是編譯期的紀律與一道更陡的學習曲線，而不是執行期的速度——恰好是一個核心付得起的那筆交易。
兩種對信任的哲學
把 seL4 與 Rust-for-Linux 看成對同一個問題——我們如何停止信任程式設計師把它寫對了？——的兩個回答，放在一道光譜的兩端，會有幫助。seL4 把一個特定的小工件對著一份完整規格證明到完全正確，那是一份巨大的一次性努力，產出了一個核心曾承載過的最強保證，但只在一個小型專家團隊能管理的規模上。Rust-for-Linux 讓一整個語言自動地、為任何人寫的每一行，強制執行一個較窄的性質——記憶體與執行緒安全——它能擴展到數千名貢獻者，但保證的比一份完整的功能正確性證明少。對一點點的完全證明，相對於對一大堆的自動部分安全。
Two answers to 'stop trusting the programmer':
seL4 Rust-for-Linux
scope ~10k lines, 1 kernel every new line of kernel code
guarantee full functional memory + thread safety
correctness vs spec (a narrower property)
enforced by a hand-built proof the compiler, automatically
cost years of expert proof learning curve + fight-the-
effort, stays small compiler, scales wide
trusted base spec, HW model, compiler, unsafe blocks,
proof checker, asm the C it calls into
strongest-for-the-least vs. good-enough-for-the-most這兩者不是對手；它們是同一個直覺瞄準了不同的規模，而它們合起來勾勒出系統軟體正往哪裡去。這是為這整座階梯收尾的那場安全對控制的辯論的核心：數十年來 C 的答案是「給程式設計師完全的控制、並信任他們的紀律」，那既產出了史上最快的軟體，也產出了你研讀過的那本充滿溢位、被未定義行為纏祟的失敗目錄。前沿的答案是把控制留在它真正被需要的地方——這座階梯所建立其上的那份貼近金屬的力量——同時讓一台機器，一個證明查核器或一個編譯器，去擔保人類會弄錯的那些部分。不是更少的控制，而是你不再需要完全裝在自己腦袋裡的控制。