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

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

SkyOS·天樞以“1+4+N”的技術(shù)架構(gòu)，實現(xiàn)這七大特性。

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

“4”是指SkyOS的4個操作系統(tǒng)內(nèi)核：

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

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

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

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

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

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

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

微內(nèi)核與宏內(nèi)核區(qū)別

圖片來源：seL4基金會

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

L4微內(nèi)核家族樹

圖片來源：seL4基金會

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

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

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

SeL4是微內(nèi)核，也是虛擬機。

SeL4虛擬機

圖片來源：seL4基金會

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

來源：蔚來

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

蔚來數(shù)字架構(gòu)

圖片來源：蔚來

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

來源：蔚來

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

SkyOS-M架構(gòu)

圖片來源：蔚來

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

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

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

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

POSIX之上是第三方軟件，再向上才是應(yīng)用層。

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

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

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