2024年7月蔚來科技日上，蔚來正式推出Sky.OS即天樞操作系統。

蔚來宣稱這是蔚來歷時4年研發、投入超過23,000人/月、面向AI打造的汽車智能底座，對全生命周期的用戶體驗與企業的體系化效率提升，將發揮重要作用。

SkyOS·天樞以“1+4+N”的技術架構，實現這七大特性。

“1”是指多場景優化、高性能、高可靠的虛擬機監視器 SkyOS-H，用來管理和調度整車的異構大算力資源，為各個系統提供安全隔離的運行環境。相比行業通用方案，SkyOS-H 實時任務時延縮短 50%，多線程吞吐量提升 40%，虛擬磁盤吞吐提升 15%。

“4”是指SkyOS的4個操作系統內核：

輕量、強可靠性、強實時性的 SkyOS-L，支持所有主流車載 MCU 芯片架構。相比行業通用方案，SkyOS-L 實時周期性信號準時送達率提升 30-40%；

基于微內核構建高安全、強可靠性、強實時性的 SkyOS-M，用于中央大腦，主要運行車控相關功能，包括車身、底盤懸架等的高階控制邏輯。SkyOS-M 的核心優勢是安全隔離，在受到同樣影響的情況下，SkyOS-M 的自恢復速度比 Linux 系統快 100 倍；

面向豐富應用場景高性能、實時性深度優化的 SkyOS-R，部署智能駕駛域的大部分功能。與Linux 發行版相比，SkyOS-R 在輕負載情況下實時性能高 113 倍，在高負載情況下實時性能高 20 倍，端到端通信延時小于 1ms，為智駕提供更高的實時性性能保障；

面向原生智能深度定制的SkyOS-C，承載絕大多數的智能座艙功能，實現低延時的車云一體化，充分利用云端更大的算力資源與模型，提供更加智能的座艙AI體驗。

“N”是指 SkyOS-中間件，是實現分層解耦、跨域融合的關鍵，也是支持全生命周期升級和信息安全保障的基礎。

天樞操作系統是基于德國seL4微內核的，2024年10月的seL4峰會上，蔚來技術副總裁曲寧做了演講，文檔如下https://sel4.systems/Foundation/Summit/2024/slides/software-defined.pdf。曲寧北大畢業后去卡梅隆大學深造，第一份工作是英偉達系統軟件工程師，然后跳槽到谷歌Linux核心隊伍，2018年進入百度，是百度CarOS首席工程師，阿波羅智能駕駛系統也有參與，2020年進入Waymo，負責深度學習Runtime團隊，2022年進入蔚來。

嚴格講seL4也不是德國的，它是一個跨國組織，頂級會員有四家，分別是地平線、蔚來、悉尼大學和高頻交易自營商Jump Trading。高級會員中知名的只有蘋果，一般會員基本都是大學，包括蘇黎世理工學院、堪薩斯州立大學、俄勒岡Lewis & Clark大學、RISC-V國際。此外需要說明，seL4也是Linux基金會的一員。

微內核與宏內核區別

圖片來源：seL4基金會

微內核是將服務轉移到進程上的一種內核模式。宏內核是一種傳統的內核結構，它將進程管理，內存管理等各項服務功能都放到內核中去。微內核只保留最低限度的服務，因此安全性極高，但無法細粒度運行，只能做一個增強模塊。Linux（安卓）這樣的宏內核系統還是不可或缺。這就好比沒有電腦的時代，一家公司，所有人都在一間辦公室工作，并且每個人的工作都有關聯，都在一個辦公室，效率自然就很高，但是一個人感冒了，容易全部都傳染感冒，這就是宏內核。微內核是一家公司，只保留最低限度的工作人員，只能干部分工作，并且每個人一間辦公室，大部分工作人員都轉移到外地，這樣安全性很高，但效率很低。不過可以提高單個人的辦公效率就能解決問題。

L4微內核家族樹

圖片來源：seL4基金會

第一代微內核是1986年卡內基-梅隆大學的Avie Tevanian和Richard Rashid主導開發的Mach，第二代即L3和L4，還有至今還很活躍的QNX系統使用的Neutrino內核。德國的計算機科學家Jochen Liedtke認為Mach的IPC效率低下的原因就是因為IPC部分不夠精簡，于是他開發了L3和L4微內核，對IPC部分進行了很徹底的精簡，這項特色保留至今。seL4是在第二代內核L4的基礎上發展而來的，澳大利亞國家信息與通訊技術部（NICTA）為軍方開發操作系統時注意到了完全開源免費的L4微內核，聯合新南威爾士大學對其進行了改造，secure embedded L4誕生，這時是2009年。seL4不僅繼承了L4內核家族的高性能特性，還具備基于端點(endpoint)的IPC機制。這種IPC機制最大的特點是使用了能力空間的概念，進程在使用IPC請求系統服務時必須具備相對應的能力，進程持有不可偽造的令牌來表示擁有請求某種服務的能力。令牌可以被復制，可以被轉移，還可以通過IPC進行傳輸。

越大的系統潛在的bug就越多。所以微內核在降低bug方面非常有優勢，seL4是世界上最小的內核之中的一個，總共9000行代碼。可是seL4的性能能夠與當今性能最好的微內核相比。作為微內核，seL4為應用程序提供少量的服務，如創建和管理虛擬內存地址空間的抽象，線程和進程間通信IPC。這么少的服務靠8700行C代碼完成。seL4是高性能的L4微內核家族的新產物，它具有操作系統所必需的服務，如線程，IPC，虛擬內存，中斷等。seL4的實現被證明是bug-free（沒有bug）的，比如不會出現緩沖區溢出，空指針異常等。還有一點就是，C代碼要轉換成能直接在硬件上運行的二進制代碼。seL4能夠確保這個轉換過程不出現錯誤，可靠。seL4是世界上第一個（到目前也是唯一一個）從很強程度上被證明是安全的OS。

早期高通的手機使用OKL4 內核，出貨量超過10億，而 OKL4 的前身 L4-embed，用在 Apple A7 處理器的一個安全協處理器上，地位可能有點像 Intel CPU 里跑的Minix。

SeL4是微內核，也是虛擬機。

SeL4虛擬機

圖片來源：seL4基金會

seL4支持用戶模式的VMM，即虛擬機監控，用于虛擬機時會挑系統底層硬件，EL2只用于ARM系統，Root-Ring-0用于x86系統，HS用于RISC-V系統。

來源：蔚來

天樞是全車輛域操作系統，主要是為了適應中央計算系統，需要高可靠性、低延遲和高帶寬，也需要芯片提供完整工具鏈支持，天樞打破了ECU的域邊界，對供應鏈整合也提出了很高的要求。

蔚來數字架構

圖片來源：蔚來

從中不難看出，天樞系統是一個虛擬機之上四個小型操作系統，嚴格地說與天樞關聯最密切的是SkyOS-M，SkyOS-C是一個改造過的安卓。

來源：蔚來

SkyOS設計了多層分級安全，包括4級監控，3級恢復，確保萬無一失，當然，這必然消耗CPU算力，需要強大的芯片支撐。

SkyOS-M架構

圖片來源：蔚來

上圖看起來非常復雜，全部使用了專業的軟件術語，讓人完全看不懂，要明白這個圖，需要把“lib”即庫，這個前綴去掉，blk是block，net自然指網絡，serial自然就是串行，dev就是devices，器件。Srv或sv就是service的縮寫。

底層（MCU抽象層）自然是MCU芯片廠家決定的，seL4處于抽象層之上，virtio 是guest 與host 之間通信的潤滑劑，提供了一套通用框架和標準接口或協議來完成兩者之間的交互過程，極大地解決了各種驅動程序和不同虛擬化解決方案之間的適配問題。這個應該還是需要底層芯片支持的，圖上也不難看出蔚來的底層MCU是NXP的S32G，存儲系統還是eMMC。LINFLEX是NXP的一個工具，用來配置UART端口，PL011也是UART關聯的。S32GPFE中的PFE即Packet Forwarding Engine ，這是NXP開發的即以太網加速模塊，模塊支持以太網包的轉發、修改、分類等功能，它基于已在NXP Layerscape系列處理器上驗證的解決方案，僅需使用CPU轉發33%的功耗，就可從主機CPU完全offload網絡轉發相關負載。

sel4之上是process 服務器，再上是Device服務器和驅動，再向上是四個模塊：時鐘、FS（可能是功能安全）、網絡和MISC。Libcore貫穿這三層。再向上是musl libc編譯的POSIX系統，是一個輕量級的 C 標準庫，它的設計目標是盡可能小而快，同時提供最高的代碼質量和安全性。musl libc的源代碼通常較短，編譯速度較快，沒有額外的依賴，因此非常適用于嵌入式系統和輕量級應用程序。POSIX是Portable Operating System Interface for Computer Environments 的縮寫，它是ISO C的延伸，POSIX的目的，是統一UNIX-like 的OS對外的接口，方便OS之上的應用在各種OS上移植運行，完整的POSIX標準有4000多頁，1000多個接口。POSIX與AUTOSAR關系密切，CP中的操作系統部分主要沿用OSEK，而AP的操作系統部分，則明確了是基于POSIX PSE51的。

PSE51并沒有定義進程間通訊IPC （inter process communication）， 因此并沒有直接的接口可以實現進程之間的交互。所以進程間通信需要有額外模塊支持，例如AUTOSAR AP提供的CM （communication management ）。抽象出來的ARA接口可以用于IPC，統一提供機器內和機器之間面向服務的通信。隨著面向服務架構（SOA）在汽車行業的流行，POSIX提供的標準接口也為以太網通訊和統一服務接口提供了良好基礎。

POSIX之上是第三方軟件，再向上才是應用層。

基于微內核的操作系統一般是第三方提供的，蔚來力求垂直集成，也做了。第三方的話，中興通訊也在做，2022年初，中興通訊的汽車操作系統GoldenOS微內核產品獲得了SGS頒發的ISO 26262 ASIL-D級汽車功能安全產品認證證書，中興通訊旗下產品——車用微內核操作系統ZTE Automotive OS V3.0正式通過POSIX規范PSE52實時控制器1003.13-2003系統認證，成為國內首家獲得此認證的企業。當然也可以委托第三方，微內核也有不少選擇，例如QNX的Neutrino或被Aptiv收購的風河（Vxworks混合內核），Linux基金會的微內核項目Zephyr。

微內核不能取代宏內核例如Linux這種大型系統，微內核的通訊成本很高，本來傳遞個地址就可以的事，現在要整個復制過去。所以復雜的功能還是離不開宏內核，如同座艙離不開安卓，ADAS也離不開Ubuntu，軟件定義汽車時代，必然要使用Linux這種大型系統。微內核主要用來做做虛擬機和增強功能安全，當然最底層的芯片是最關鍵的，所以蔚來也做了芯片。

能用比較小眾的seL4微內核打造天樞系統，毫無疑問，蔚來的軟件團隊是國內所有乃至全球汽車廠家中最強的。