跳轉到

2009 seL4 微核心驗證：九千行 C 的終極審判#

案件編號：2009-SEL4。報案人：NICTA 與全世界用作業系統的人。案情：核心是所有安全的根，根一爛全爛。破案者：Klein、Elphinstone、Heiser 團隊。

案發現場#

作業系統核心是特權中的特權。它管理記憶體、排程、行程間通訊，一旦有 bug，沙箱、簽章、PCC 全都站在沙上。傳統核心動輒百萬行，測試覆蓋率再高也只能說「沒測到壞」，不能說「沒有壞」。

微核心（microkernel）主張把核心縮到最小：只留位址空間、執行緒、IPC，其餘丟到使用者態。L4 系微核心僅約 9000 行 C，正是形式驗證夠得著的獵物。但 9000 行 C 加並行、中斷、硬體，仍是巨獸。沒有先例證明：C 實作與高層規格等價。

2004–2009 年，澳洲 NICTA 的 L4.verified 團隊（Klein 領軍，約十餘人）立下軍令狀：用 Isabelle/HOL 證明 seL4 微核心的功能正確性，外加資訊流安全。這是當時最大膽的驗證豪賭。

偵查過程（含數學式/表格/理論）#

線索一：精化即層層無罪推定#

團隊不用「直接證 C 正確」，而用精化（refinement）搭三層階梯：

  1. 抽象規格 \(A\) ：數學化的 OS 狀態機，數百行 Isabelle，講「該做什麼」。
  2. 可執行規格 \(E\) ：確定性的 Haskell 原型，可跑可測，講「怎麼做」。
  3. C 實作 \(C\) ：真正的 9000 行 C，經嚴格子集與語意建模，講「跑什麼」。

正確性即兩步精化：

\[ A \sqsubseteq C \]

展開為 \(A \sqsubseteq E\) 與 \(E \sqsubseteq C\) 。符號 \(\sqsubseteq\) 意為「具體層的每個可觀察行為都是抽象層允許的」。證明用前向模擬：具體走一步，抽象走零步或多步跟上，精化關係保持。

表格：三層分工。

層 語言 规模 角色
\(A\) 抽象規格 Isabelle/HOL 約數百行 安全與功能定義
\(E\) 可執行規格 Haskell 約數千行 設計驗證、可測試
\(C\) 實作 C99 子集 約 9000 行 上線程式

線索二：Haskell 原型到 C 的取證鏈#

為何多此一舉經 Haskell？因為直接從抽象跳到 C，間隙太大，人類寫不出模擬關係。Haskell 原型是橋樑：它與 \(A\) 邏輯接近，又與 \(C\) 控制流同構。團隊先在 Haskell 上跑測試、修設計，再把 Haskell 翻譯成 Isabelle 的 Simpler-C 語意，逐函數證明對應。

規模 disclosed：C 約 9000 行，Isabelle 證明約 60 萬行（含函式庫與自動化）。人年約 20–30，驗證成本約為開發成本的十倍以上。但這是第一次：商用級核心的每個系統呼叫、中斷路徑，都有機器檢查的證據。

關鍵性質包括：功能正確（functional correctness）、完整性（integrity）、授權正當（authority confinement），以及後續的資訊流安全（infromation-flow noninterference）：高密級資料不洩向低密級，除非經授權通道。

線索三：資訊流安全的第二封印#

功能正確只說「做了規格的事」，沒說「沒做規格外的洩漏」。團隊進一步證明 noninterference：對任意兩初態，若低等級可觀察部分相等，則執行後仍相等。形式骨架為：若 \(s_1 \approx_L s_2\) 且 \(s_1 \rightarrow^* s_1'\) 、 \(s_2 \rightarrow^* s_2'\) 經同樣排程，則 \(s_1' \approx_L s_2'\) 。

這把 seL4 從「不會當機」推向「不會洩密」，成為高保障系統（Common Criteria EAL7、軍用分離核心）的罕見實例。

性質 公式意涵 價值
功能正確 \(A \sqsubseteq C\) 無崩潰、行為合規
完整性 寫入必經授權 隔離不被繞過
資訊流安全 低觀測等價保持 無隱通道洩密

結案報告#

案件告破。2009 年 SOSP 論文宣布：seL4 的 C 實作精化其抽象規格，60 萬行 Isabelle 證明已檢查。這是驗證史的珠峰：最大、最深、直達可執行 C。

遺產有三：

  1. 證明「大規模系統驗證可行」，催生 CertiKOS、Ironclad、Project Everest。
  2. seL4 開源並持續演進（多核、RISC-V、時間保護），成為研究與工業的共享證物庫。
  3. 方法論確立：抽象—原型—實作三層精化、自動化證明工程，後來者皆抄這份筆記。

從因果鏈看，seL4 上承 LCF 可信核心、Isabelle、Hoare 邏輯、PCC 與 CompCert，下啟高保障系統與 Rust/Iris 時代：核心已證，接著證驅動、證編譯器、證整個棧。

證據與工具#

證據 A：精化陳述，獨立成行。

\[ A \sqsubseteq C \]

其中 \(A\) 為抽象規格， \(C\) 為 C 實作， \(\sqsubseteq\) 為精化（具體行為皆抽象允許）。

證據 B：精化圖（文字版）。

A: a  ----->  a'
     |          |
     R          R
     |          |
C: c  --*-->  c'

\(R\) 為精化關係，C 走多步，A 走對應步，關係保持。

證據 C：Isabelle 定理風格示例。 theorem kernel_correct: "cRefines aSpec cImpl" ，底層展開為每個系統呼叫的 Hoare 三元組 \(\{P\} \, c \, \{Q\}\) 與不變式保持。

證據 D：延伸閱讀。Klein 等 2009 年〈seL4: Formal Verification of an OS Kernel〉（SOSP）；Klein 等 2014 年 JACM 長文；seL4 開源證明庫與《seL4 白皮書》資訊流安全章。