蔚来Sky天枢操作系统详解

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微内核打造天枢系统，毫无疑问，蔚来的软件团队是国内所有乃至全球汽车厂家中最强的。