推動這道前沿的那個老憂慮
到了現在，你已經知道一個傳統作業系統是怎麼蓋起來的，你也知道它那個令人不安的祕密。核心在核心模式下運行，對整台機器握有完全的權力，而在主流系統上它無比龐大——數百萬行 C 程式碼、各種驅動程式、檔案系統、網路堆疊，全擠在同一塊特權位址空間裡。那正是你必須絕對信任的部分，因為它裡頭只要有一個臭蟲——一次緩衝區溢位、一個讓權限提升得逞的漏檢——就能攻陷整台電腦。資安界把那塊「必須被信任」的區域叫做可信計算基礎，而一個正常作業系統誠實的總結是：它的可信基礎大得根本不可能真正值得信任。
你以前見過這道張力一次，就是單體式核心對上微核心的辯論。單體式核心為了速度，把一切都塞進那一塊特權空間；微核心則把驅動程式與檔案系統推出去，變成普通的行程，只在裡頭留下一個極小的核心，背後的理論是：可信基礎裡的程式碼越少，能藏住災難的角落就越少。這篇導覽裡的前沿，承接的正是同一種直覺——把你必須信任的東西縮小、強化——並把它推向兩個極端。一個極端徹底丟掉核心與應用程式之間的劃分；另一個則在核心被數學證明正確之前，拒絕把它出貨。
單核映像：把作業系統縮進應用程式裡
先從那個激進的點子開始。單核映像，又叫函式庫作業系統（library operating system），問了一個離經叛道的問題：如果一台虛擬機只會跑一個應用程式，那何必還在它底下塞一整套通用作業系統？取而代之的，你只取出那一個應用程式真正會用到的作業系統零件——它那一小片網路堆疊、它需要的檔案存取、必要時的一個排程器——把它們當成普通函式庫連結進去，跟應用程式一起編譯成單一個微小的映像。沒有 shell、沒有第二支程式、沒有登入：那個映像就是應用程式，也是它這輩子唯一需要的作業系統，兩者熔成一體。
最令人吃驚的後果是，使用者／核心之間的劃分消失了。只有一個程式待在同一塊位址空間裡，所以沒有什麼東西需要被保護開來——也沒有什麼跨越邊界的系統呼叫要做。原本那場有守衛的、掉進核心的墜落，變成了同一個映像內一次普通的函式呼叫，這也是單核映像能跑得這麼快的原因之一。它們通常以毫秒為單位、直接在超管理器上開機，因為幾乎沒什麼要啟動的：沒有裝置探測、沒有使用者設定，就只有那一個映像跳動起來。而且因為映像只裝了那個應用程式需要的程式碼，攻擊面極小——根本就沒有多餘的 shell 或服務，可供入侵者濫用。
經驗證的核心：證明它，而不只是測試它
第二道前沿，從相反的方向進攻信任。測試只能顯示核心在你想得到要試的那些情況下能運作；它永遠無法顯示「不存在任何壞情況」。形式化驗證的目標更高：它替核心「應該做什麼」建一份精確的數學規格，再構造一份經機器檢查的證明，保證實際的實作，在每一種可能的輸入、每一條可能的路徑上，永遠吻合那份規格。不是「我們很用力地測過，沒找到臭蟲」，而是「我們用一套電腦會重新核對的邏輯，證明了這一整類臭蟲不可能發生」。
這裡的里程碑是 seL4，微核心家族的一員，它成了第一個帶有這種證明的通用作業系統核心。成果確實非凡：在所涵蓋的組態下，seL4 帶著一份保證，確保它的 C 實作吻合它的規格，而這又排除掉一整類一整類的故障——沒有緩衝區溢位、沒有空指標崩潰、也沒有那份證明所處理的那幾種權限提升。關鍵在於，這件事之所以辦得到，很大一部分是因為 seL4 是個微核心：它的可信計算基礎只有大約一萬行程式碼。證明一萬行正確，是一場英雄式的、橫跨數年的努力；而要證明一個一千萬行的單體式核心正確，在今天根本就不可行。
微核心為什麼正在捲土重來
請注意，單核映像與 seL4 都倚靠你在保護那幾階學過的同一個老點子：讓被信任的部分保持小。這正是為什麼幾十年前在主流效能之爭裡敗下陣來的微核心設計，正悄悄地復興。當年那項反對是具體而公允的。當你把驅動程式與檔案系統搬出核心、變成各自獨立的行程，這些零件就不能再直接互相呼叫了——它們必須透過行程間通訊對話，而過去每一條這樣的訊息，都意味著一趟跨越保護邊界的緩慢來回。單體式核心因為一切都在同一塊位址空間裡，只要呼叫一個函式，就把那筆成本省掉了。
有兩件事改變了這道盤算。第一，數十年細緻的工程，讓微核心的 IPC 比當年害它背上壞名聲的那些早期系統快得多，把效能差距縮小到許多系統都能輕鬆負擔的程度。第二，也更重要的是，我們願意付出代價去換的東西變了。對一支手機的安全飛地、一台飛機的控制器、或一台醫療裝置來說，犧牲一點點純粹的速度，換來一個可信基礎極小——而且就 seL4 的情況而言，還真的被證明正確——的核心，是微不足道的代價。當安全與可信凌駕於純粹吞吐量之上，微核心當年的弱點就成了一筆值得付的代價，而它當年的強項，恰恰成了你想要的東西。
為什麼這很難，又該擺在哪
我們值得直白地談談：為什麼經驗證的、極簡的核心，沒有就這麼到處都是。形式化驗證貴得驚人：seL4 的證明耗費了專家數人年的工夫，而證明的工作量遠遠超過被證明的那段程式碼本身的大小。這門技能稀有、證明在程式碼一變動時就很脆弱，而要把這套技術擴大到一個功能豐富、上百萬行、又不斷翻攪的核心，仍是一個尚未解決的研究問題。單核映像面對的是同一道牆較柔和的版本——它要求你放棄那個你一直倚賴的、舒適、通用、工具齊全的環境，換來只在狹窄、高價值的部署上才划得來的好處。
那麼這一切，把站在最後一階上的你，帶到了哪裡？不是帶到一個贏家面前。你研讀過的那些通用的、偏單體式的系統不會消失——它們以龐大換來能替每個人、在每種硬體上跑遍每件事。前沿揭示的，是那條過去沒走的路：在最講究信任的那些角落，我們如今知道怎麼蓋出小到可以理解、極簡到可以強化、而在最大膽的情況下還能對著一份規格被證明正確的作業系統。很久以前給了我們微核心的那同一個直覺——把你必須信任的東西縮小——在這道前沿，終於被推到它所能去到的最遠處。