蔚来Sky天枢操作系统详解，seL4微内核

2024年7月蔚来科技日上，蔚来正式推出Sky.OS即天枢操作系统。

图片来源：蔚来

蔚来宣称这是蔚来历时4年研发、投入超过23,000人/月、面向AI打造的汽车智能底座，对全生命周期的用户体验与企业的体系化效率提升，将发挥重要作用。

图片来源：蔚来

SkyOS·天枢以“1+4+N”的技术架构，实现这七大特性。

“1”是指多场景优化、高性能、高可靠的虚拟机监视器 SkyOS-H，用来管理和调度整车的异构大算力资源，为各个系统提供安全隔离的运行环境。相比行业通用方案，SkyOS-H 实时任务时延缩短 50%，多线程吞吐量提升 40%，虚拟磁盘吞吐提升 15%。

• 轻量、强可靠性、强实时性的 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（安卓）这样的宏内核系统还是不可或缺。这就好比没有电脑的时代，一家公司，所有人都在一间办公室工作，并且每个人的工作都有关联，都在一个办公室，效率自然就很高，但是一个人感冒了，容易全部都传染感冒，这就是宏内核。微内核是一家公司，只保留最低限度的工作人员，只能干部分工作，并且每个人一间办公室，大部分工作人员都转移到外地，这样安全性很高，但效率很低。不过可以提高单个人的办公效率就能解决问题。

图片来源：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支持用户模式的VMM，即虚拟机监控，用于虚拟机时会挑系统底层硬件，EL2只用于ARM系统，Root-Ring-0用于x86系统，HS用于RISC-V系统。

来源：蔚来

图片来源：蔚来

从中不难看出，天枢系统是一个虚拟机之上四个小型操作系统，严格地说与天枢关联最密切的是SkyOS-M，SkyOS-C是一个改造过的安卓。

来源：蔚来