SeL4 微核心已針對 AArch64 架構完成正式安全證明，標誌著經過驗證作業系統的重要里程碑。此成就將該核心的數學保證擴展至驅動多數現代行動與嵌入式裝置的硬體平台，為在普及的 ARM 架構上建構安全軟體堆疊提供了經數學證明的基礎。

這項驗證對於極度重視硬體層級安全性的嵌入式系統、汽車和軍事領域的高保證應用至關重要。目前的證明範圍涵蓋單核心、非 MCS（混合關鍵性系統）配置，雖然涵蓋了許多使用情境，但排除了 MCS 變體中發現的多核心排程複雜性。

事件背景

SeL4 是部署最廣泛的微核心之一，以其小型信任計算基礎而聞名。正式驗證涉及透過數學證明，確認核心的 C 語言實作與抽象規格相符，確保核心邏輯中沒有程式錯誤。AArch64 是 ARM 架構的 64 位元執行狀態，在智慧手機和伺服器中佔據主導地位。

社群觀察

社群成員指出該證明僅限於單核心、非 MCS 配置的限制，並對潛在的側通道定時攻擊提出擔憂。其他人則強調了汽車超管理程式中的現有部署，並呼籲整合原生 SeL4/Linux 以提升安全性主張。