reL4项目总结 #

2 微内核架构的设计原则 #

2.1 最小化内核原则 #

这是微内核的基本原则，也是它之所以被称为“微”内核的原因，即在内核中只保留最必要的内容。

最小化内核原则带来了诸多安全方面的优势，内核中的代码数量少更有利于进行形式化验证等安全性验证，即使不通过形式化验证等安全性验证，也可以减少内核中出现bug的概率，有利于保证系统的安全。

最小化内核原则也能一定程度上提升性能。在微内核架构中，IPC性能是其重要的性能瓶颈之一，而内核中过长的系统调用链会带来IPC性能的进一步下降。因此，缩短内核中的调用链长度，对于性能提升具有重要的影响。这也是以Mach为代表的微内核所带来的教训之一，在以L4为代表的后续微内核设计中，都尽量的遵循该原则以提升性能。

2.2 策略与机制分离原则 #

在最小化内核原则的基础上，选择什么内容放在内核中，什么内容放在用户态，成为一个关键性的问题，这就需要遵循策略与机制的分离原则。

以中断为例，中断触发的时候切换到内核态，并保存上下文，这是硬件的机制，但是在中断触发之后做什么操作，则属于中断处理的策略。对于前者，由于不得不读写内核态才能写入的寄存器，因此必须放在内核态执行，而后者则既可以像宏内核一样，放在内核中进行直接处理，也可以选择通过通信的方式，发送消息到用户态进行处理，即微内核的处理方式。

因此，微内核实现最小化内核原则的方式，就是将只有必须放到内核态执行的操作，放在内核态；而其他的并非必须的操作，尽可能的放在用户态去。为了在用户态的策略能够调用内核态实现的机制，就必须在系统调用中接口，给出相应的机制调用接口；同时也需要改写操作的方式，将在宏内核中实现的策略和机制混合的代码，分离为在内核态的代码和用户态的机制，再设计合适的策略和机制衔接的机制。

2.3 实施细粒度的控制 #

基于微内核架构的最小化内核原则及策略和机制分离的原则，内核中存在的数据结构及其操作，均是最小化的数据结构和基本元操作。这就允许并要求微内核具有细粒度控制的原则。

这种细粒度的控制，一方面表现为，对内核中存在的数据结构的细粒度操作。通过典型的如capability等机制，对每个内核对象进行管理。每个内核对象的操作必须显式的声明并通过权限的验证才可以进一步地执行。

另一方面也表现为，对用户态的每个进程（线程）都会进行各类资源和权限的控制，例如CPU时间/内存空间的限制或者是否能够访问某个syscall，访问磁盘设备等资源。

相比于宏内核而言，更细粒度的系统控制是微内核安全性保障的一个重要体现。

2.4 系统服务解耦原则 #

微内核尽可能地将内核服务放置于用户态，其中一个重要的出发点就是希望通过地址空间的隔离，将敏感的内核态操作机制和与内核机制无关的策略相区分。但是一个完整系统的实现，除了内核态的机制外，同样依赖于各类系统服务，它们在微内核下被置于用户态中。如果用户态的所有服务都放在同一个用户态进程中，虽然实现了策略和机制的分离，但是由于缺少模块间的隔离，一个系统服务模块的崩溃会引起崩溃的扩散。因此，在微内核中，也往往需要遵循系统服务解藕原则。

系统服务解藕原则要求每个系统服务（如设备驱动、文件系统）作为独立用户态进程运行，通过明确的接口（如消息传递）与内核或其他服务交互。

系统服务解藕原则使得微内核能够通过地址空间的隔离，让系统服务之间彼此隔离并只能通过进程间通信通过特定的接口进行交互。这一方面使得系统服务模块的崩溃不会扩散，另一方面在某个系统服务崩溃发生之后，一个经过良好设计的微内核系统不需要重启整个系统，只需要重启该服务即可。

而良好的系统服务解藕，给出了清晰的系统服务组件之间的接口，这也使得系统可以动态地加载或者卸载某个系统服务模块，或者更换同一个系统服务模块接口的不同实现。提高系统的灵活性。

这种模块化组件化的思想在软件工程的设计中也并不鲜见，例如在宏内核中也有模块化的特性，但是通过地址空间隔离进行模块间的隔离是微内核所特有的。

3 seL4内核概述 #

3.1 seL4微内核总体架构 #

基于第2章所述的微内核的各项原则，seL4实现了一个微内核必要的各个要素。seL4内核提供了一个内核所需的内存、进程、中断、IPC等各项基本要素的机制，并通过capability等设计，实施细粒度的内核对象管理。

3.2 基于capability的内核对象抽象 #

在一个操作系统内核中,几乎所有的操作都是在不断地跟各类内核对象进行交互。但是直接使用内核对象的地址访问该内核对象存在安全问题,因此出现了使用句柄(handler)等方式访问内核对象的设计,seL4也同样采用了这样的设计思路。不同的是,seL4作为一个微内核,可以通过精巧的设计,将内核对象数量限定为有限的若干种,并通过抽象,将内核对象相关的重要信息封装在一个称为capability的,固定为128bits大小的句柄中。

seL4通过capability机制对内核对象进行统一的抽象,并通过一个集合了所有的capability的cspace对内核中的所有内核对象进行管理。

对于cspace的结构,可以类比于页表。在cspace的顶层,包含了2^redix个slot构成的array用于存放capability,每个slot大小128bits,和capability大小一样。在顶层cspace中的某些slot,也可以存放一些cnode,即用于表示二级或者更深级数的cspace的capability。

cspace通过一个cptr来指定某个slot,并找到其中存放的capability。这个cptr类似于页表中的虚拟地址,用于描述slot的地址。但是正如前面所述,这不是一个真实的内核对象的地址。这个cptr会通过guard bits和redix进行层级切分。其中guard bits是用于判断是否跟当前的cspace相符的一个判定,而redix正如前文所述,用于指明该层的slot array中包含多少个slots。

例如一个32位的cptr,如果第一层的guard占用了4个bits,redix占用了8个bits。那么最高的12个bits会被用于访问最顶层的slot array,该array具有2^8=256个slots。如果这个cptr最高的4位为0,剩余的低20位都是0,在最高4位后面跟着的8位所指出的那个slot处存放着查找到的目标slot,如果该slot不是一个cnode的capability,那么就认为找到了。如果并非如此,即可以向下查找,那么就查看第二层的guard bits和redix。如果同样是4个bits的guard和8个bits的redix,会继续匹配剩余20位中最高4位表示的guard是否都为0,再之后的8位用于查找slot,最后的20-12=8位如果为0,且该slot不为cnode,就认为找到了,如果不是就继续。以此类推。

除了通过cspace来进行capability的管理之外,seL4也维护了capability之间的关系,除了创建,销毁之外,还有Mint(从某个capability继承全部或者部分权限),Copy,Move,Revoke(不仅删除自己,还删除所有派生出去的capapbility)等更为复杂的capability操作。

capability系统让seL4对所有内核对象有了非常灵活的管理。

3.3 seL4的内存管理 #

3.3.1 虚拟内存的管理 #

在支持虚拟内存的硬件架构上，操作系统可以开启分页或者分段或者段页式的虚拟内存机制，从而实现远超物理内存限制的地址空间，以及通过地址空间来隔离不同进程，提升安全性。seL4需要为用户态提供相应的机制。

seL4所基于的硬件架构，均支持多级的分页内存机制，因此，seL4提供了相应的统一多级页表的支持。

在名称上，seL4系统中的物理内存页被称为frame，而虚拟内存所需要的页表项和页表，包括page Directory，page table等。这些都被描述为不同类型的capability。当然，由于seL4支持多个架构，因此他们的页表项pte的相应属性都有一些架构相关的内容。

除了页表之外，seL4还提供了多地址空间asid的支持。包括了asid pool和asid control两个capability。

page fault的处理，也是传统内核中必要的一部分内容。在seL4中，则会传递给进程设定的fault handler的endpoint进行处理。

3.3.2 内核所需要的内存分配 #

对于seL4而言，在系统启动之后，除了预先分配给内核的内存空间，剩余物理内存空间都交给了root-task。微内核在内核中只保留机制，而让策略放在用户态的设计哲学，决定了需要用户态的root-task来确定内存分配的策略。而内核在运行过程中需要不断地创建新的内核对象，因此需要提供相应的机制以供用户态的策略可以申请内核对象。

在seL4中，将未被分配出去的内存空间，也被当成一种特殊的capability，也就是untyped capability。untyped capability用于表示一段未被分配出去的内存空间，并可以通过该capability唯一的系统调用来将其type为其他的内核对象。

每个untyped的内存在申请的时候并不是一口气全部分配出去的，而是按照申请的内存大小向上对齐的2的整数次幂进行分配。此时，剩余的未分配的untyped的内存仍然会被记录，以便下一次进行再分配。

3.4 seL4的IPC #

3.4.1 快速IPC #

在以Mach为代表的传统的微内核实现中，IPC的性能是微内核性能的瓶颈。在宏内核下两个不同内核模块之间的交互，在微内核下会转变为两个用户态进程（线程）之间的通信，需要进入内核，切换地址空间并传递消息，再切换回来，这其中有巨大的开销。因此，以L4微内核为代表的一系列微内核都通过寄存器传递参数等方式，用于实现快速IPC。

在seL4中，使用消息寄存器进行参数的传递。在不同架构下，寄存器数量大相径庭，因此，seL4也会给定不同的消息寄存器的数量，同时，其他的寄存器也会用做capability传递等用途。

在消息传递的过程中，也有可能出现消息数量大于该架构下可用的消息寄存器数量的情况。在这种情况下，才会采用内存拷贝的方式进行消息的传递。

同时，在seL4的syscall中，也针对于IPC做了特殊的设计，向内核发起系统调用的实现，统一被放在一个Sys_Call的系统调用号中，并进行进一步的分发和处理，而其他的系统调用号都被用于实现各类的IPC。在seL4中也更进一步的实现了fastpath机制，在fastpath中会经过一定的判定，如果满足判定条件，就可以快速跳转到对应的进程，否则进入slowpath的处理。这样的设计大大减少了传统内核中IPC机制需要经历的syscall分发等步骤。

3.4.2 endpoint和notification消息传递 #

在seL4中，IPC机制并不直接将消息传递给对应的目标进程，而是同样通过capability机制进行传递，这是为了避免类似于DDOS的攻击而采用的一种安全策略。在seL4下的微内核的用户态模型类似于client/server的消息通信模型，这导致了，系统服务的进程可能遭受DDOS的类似攻击。

seL4提供了两种capability，一个是用于同步消息传递的endpoint，另一个是用于异步消息传递的notification。对于同步的endpoint capability，可以传递较为复杂的信息。而notification则只能传递一个u32的简短信息。

另外，seL4还提供了一个badge机制用于区分同一个endpoint capability派生出来的另一个endpoint。这可以让server用于区分来自不同的client的消息。

3.5 seL4调度与执行模型 #

seL4中的用户态任务都是在tcb结构体中体现的，当然对应于该tcb结构体，也有相应的tcb capability用于管理该结构体。为了进行任务调度，seL4还维护了一个调度队列的数据结构，用于管理这些tcb。

seL4内核中，也使用了一个简单的单内核栈的设计。

在传统的Linux为代表的宏内核中，每个进程除了各自用户空间的用户栈之外，在内核空间也有一个对应的内核栈，当在某个进程的用户态运行时，发生了陷入或者中断等事件，就进行栈空间的切换，并将内核栈每次都固定的指向栈底。内核会保证在返回到该用户态之前，内核栈空间中的内容都被清空或者无效，从而进入内核时指针指向栈底是安全的。另外，在两个进程之间切换的时候，实质上是两个内核栈指明的运行过程之间的切换。

而seL4采用的单内核栈的设计，同样在陷入或者中断等事件发生时，进行栈空间的切换，并指向固定的栈位置。为此，需要在每个进入并离开内核的路径上，都在完成内核处理过程之后，在最上层的函数中，调用schedule选择新进程并调用activateThread激活该进程并最终使用restore_user_context返回到对应的用户态。

这种单内核的架构，也意味着不允许在内核态存在栈上的阻塞方法。具体来说，在宏内核中，如果某个进程A发起系统调用，例如申请磁盘读写操作，那么在执行到某个步骤的时候需要等待磁盘操作完成，这时候可以手动调用调度器切换到其他进程B，此时，进程A的内核栈中存放着它在内核中的执行步骤。

但是如果在单内核栈中，如果允许上述的步骤，进程A的运行栈帧之下一定存放了进程B的栈帧，此时回到进程B的用户态并再次进入内核态，就会破坏进程A的栈帧内容。

因此，在这样的设计下的每一次内核执行过程一定是串行而不允许在栈上保存内容并阻塞的，如有需要，需要显式的存放在堆上。这也决定了，所有的内核的路径都是确定的，其一定存在某一次调用路径的栈空间最大，因此seL4只需要一个确定的足够大的栈空间即可，而无需产生任何动态申请内核栈空间的操作。这一点和上述的内核固定内存分配有着密切的联系。

对于seL4的调度模型，在每个进入内核的路径中，都会在某些必要的时候将当前进程放置到调度队列中，而在离开内核的时候调用schedule函数查看目前应该选择的进程。除此之外，为了支持多个优先级，seL4为每个优先级都设置了一个相应的调度队列，在调度时，先通过一个bitmap，快速的找到存在可调度任务的最高优先级，随后在该优先级所代表的调度队列中，找到对应的tcb，这种通过bitmap和对应的队列进行调度的方法和Linux的调度方法有着一定的相似性。

3.6 seL4的中断和异常处理 #

中断和异常的硬件机制决定了中断和异常必须进入到内核态进行处理，但seL4作为一个微内核，也需要遵循微内核的最小化内核原则和策略与机制分离的原则，中断的机制不得不放在内核中，但是中断的处理策略则需要放在用户态。

seL4将中断和异常的处理和IPC的机制结合起来，除了一些内核本身需要用到的中断之外（比如需要时钟中断用于任务调度），额外地使用了notification机制，将该中断的消息传递给该notification，该notification可以绑定到某个tcb上，从而指定由该tcb所表示的进程来决定如何处理该中断。

当然如果某个中断并没有被注册相应的notification用于传递该中断消息，seL4也会进行相应的错误处理。

同样的，中断作为一个内核的机制，也应当存在对应的capability进行细粒度的权限管理。如果这个capability不能授予给某个tcb表示的进程，那么自然无法将notification绑定到该中断上。

另外，在中断的处理机制上，遵循策略与机制分离等原则，seL4的实现也有一些细节需要注意。

以aarch64架构为例，在qemu-arm-virt平台上实现的seL4会使用gicv2中断控制器。该中断控制器中设计的中断状态包括inactive（未触发），pending（触发但是未被cpu处理），active（触发并被cpu处理），pending and acitve四种，对于第四种状态，每个中断的标识位只有1位，但是在同一个中断上，最多可以允许同时有两次中断信号被使用，其中一个中断信号被cpu正在处理（即active），而此时另一个中断又正好已经到达却未被cpu处理。

最后一种状态相对复杂，seL4将其进行了简化。每次接到中断之后都会直接清除该中断的允许位，让他必须在用户态调用了AckIRQ的系统调用之后，才能够重新打开该中断的允许位，这又是一个策略和机制分离的重要体现，将对中断的确认放置到了用户态来进行。这也直接导致了，第四种状态的未被使用。

当然，这也带来了在用户态系统服务编写上，与宏内核所不同的地方。仍然以中断需要在用户态进行确认这一点为例，如果用户态需要实现一个高性能网卡的驱动，显然每次收到一个包就进入内核，这会带来巨大的性能开销。在持续有网络流量到达的情况下，可以将网卡寄存器mmio映射到用户态，采用类似于napi的机制，在收到一个网络数据包的到达中断之后，系统网络服务进程持续轮询网卡寄存器中指定的数据包，并在最后调用确认中断的系统调用，再开启网卡的中断。

这些细节上的设计，均体现了seL4微内核对微内核各个原则的遵循。

3.7 seL4安全验证与形式化证明 #

seL4内核的最大特点在于其使用形式化验证的方式，验证了内核的安全性。其形式化验证方案采用一种分层式的方法，从系统的模型设计出发，向下到C代码的实现，编译器从C代码到二进制代码的转换，以及在特定硬件模型下，如arm等弱内存模型的平台上的硬件行为等，多层次地验证了该内核的安全性。

当然，seL4本身也有其验证边界，并不等同于绝对的安全。一方面，硬件本身可能存在各类安全漏洞，如Spectre漏洞本身是依赖于硬件的分支预测和缓存策略中的漏洞实施侧信道攻击，这是seL4无法避免的。另一方面，由于其完成了严格证明的微内核本身只有一个简单的内核，而一个真正可用的微内核操作系统还包括各类放在用户态的系统服务，针对这部分的攻击，仍然可能存在安全隐患。

与Rust编写的内核不同，seL4本身的安全性，并不来源于编译器的静态检查，以指针解引用为例，它通过形式化证明的方式，证明内核中并不存在空指针解引用行为。而Rust编写的内核，在safe的边界中，本身并不允许裸指针的强制类型转换和解引用，这都被认为是unsafe的部分，不过，作为一个操作系统内核，使用一定数量的unsafe的操作是难以避免的。因此，使用Rust语言对safe的部分进行保证而使用形式化验证等方式进一步保证unsafe内容的内核，具有相当的研究价值。

3.8 本章小结 #

本章对seL4的实现及其对微内核原则的遵循进行了概述。详细地阐述了seL4微内核是如何遵循所具有的微内核通常所具备的原则，同时也通过一些细节性的例子，阐述seL4自身所具备的独特性设计。

4 基于Rust语言的reL4微内核操作系统 #

4.1 reL4微内核设计目标与整体架构 #

reL4项目源于李龙昊等（2023）的尝试，最初的目标是使用rust重写seL4内核。该内核最初只是逐步将sel4的C语言部分的代码部分去除，并将去除的代码改写成一个rust语言编写的静态链接库，和seL4的原生代码进行链接，逐步进行替换的过程，最终将整个内核都变成rust语言实现的。在本文工作开展之前，已经实现了riscv的分支，通过了seL4原生的不添加任何特性基本测例。

reL4微内核的总体设计目标为，使用Rust语言重构seL4。首先这要求重写的reL4是一个完整的Rust微内核，不应当通过二进制链接等方法将任何C代码及其编译结果引入内核。其次，需要能兼容seL4的所有二进制接口，但不要求内核内部实现跟seL4完全一致。

4.2 reL4对seL4核心机制的实现 #

4.2.1 能力（Capability）机制与内核对象管理 #

正如第3章对seL4的分析中指出的那样，capability机制是seL4中实现细粒度管理的核心部分。同时，该部分的实现也是reL4实现中的一个难点。对于pbf文件中声明的，不同类型的capability的按位解析为Rust数据结构和代码的工作，在后续章节4.4.2中具体描述，本部分对capability在reL4中的数据结构和代码设计部分进行描述。

在C语言实现的seL4中，每个capability占用128bit，并通过若干个bit用于指明其类型，其他的位域成员则通过位操作表示capability附带的各种信息，这些具体的信息所占用的位域大小和偏移等内容通过一个规范化的pbf文件来描述，并在编译期通过一些python脚本将其转化为对应的C代码文件并使用。

但是，Rust和C语言具有不同的类型系统。在C语言下，每个Cspace都被用于存放抽象的capability对象，并在具体的处理中，通过检查其中的类型位域，强制转换为对应的具体capability，而这样的强制类型转换，在Rust下，必然是一个unsafe的行为，因为这打破了其安全的类型系统限制。由于这些capability本身在大量的系统调用中作为参数和用户态进行交互，因此在考虑二进制兼容的情况下无法改写其数据结构的底层实现，这导致了难以避免的对capability的unsafe行为。

当然unsafe并不可怕，只要做好良好的封装即可。从实践的角度来说，所有的capability都只占用128bits,并且所有的操作都是对其中的位操作，这样的简单机制，让这种强制类型转换足够简单且容易被封装。

对于capability这套的设计机制，最开始的reL4使用一个plus_define_bitfield的宏进行处理，需要编程手动指明各类信息，包括每个capability所占用的bytes，在capability中每个字段占用的bit,对应的偏移，以及通过bit数和偏移量得到对应的数值之后，需要左/右移多少位以获得最终的值等内容。在经过这套宏定义转换之后，会生成对应名称的capability结构体和对应的capability中各个位域的读写操作。

除此之外，reL4针对抽象的capability类型，也实现了公用的cap_t的trait。

这套机制除了可以用于capability之外，也可以用于seL4其他类似的，在pbf文件中指明的结构体字段的解析。

但是它存在一个缺点，每增加一个capability,都需要手动指明上述信息，尤其是其中的bit偏移等内容，这是容易导致bug的重要问题。针对这个问题，reL4进一步地使用了如4.4.2节中描述的脚本，更自动化地进行了capability的从pbf文件到最终的reL4中的Rust代码的转换。

在该实现中，reL4封装了在抽象capability到具体的capability的unsafe转换，允许在检查了对应的capability的type字段是否和目标类型相匹配之后，进行强制的类型转换。

当然，这里也存在实质上的重复检查问题。在seL4的实现中，seL4内核中在任何需要做这样的强制类型转换的地方都进行了capability的类型检查，且经过了形式化验证。而reL4在很多行为和设计上参考了seL4,这导致了在上述的封装好的强制转换中的type检查，在此之前其实已经全覆盖的检查过了，这带来了一定的实质上的冗余运算。由于capability的强制类型转换众多，该重复检查会带来很大的性能损失，对此，我们使用debug_assert_eq等Rust中的宏，在只有debug的编译模式下才启用该检查。

4.2.2 进程间通信（IPC）机制 #

4.2.3 调度器与上下文切换 #

4.2.4 内存管理与虚拟内存子系统 #

4.2.5 中断处理与异常管理 #

4.3 reL4扩展特性支持 #

4.3.1 reL4的组件化设计与实现 #

组件化内核，顾名思义，就是使用组件化的方式来构造内核。它将操作系统的核心——内核，视为一项复杂的软件工程并使用组件化的思想进行编写。在这一过程中，我们打破了传统内核开发的界限，让各个组件独立开来编写，使得程序员能够如同编写普通程序般自如地编写内核模块，极大地提升了开发的灵活性与效率。

更为重要的是，一个经过精心定义与验证的组件，如同构建软件大厦的预制砖块，能够在多个项目或系统中灵活复用，极大地避免了重复劳动与资源浪费，真正实现了“一次编写，到处运行”的愿景。这种高度的可重用性，不仅提升了开发效率，还确保了代码质量的一致性与稳定性。

​ 在后续的维护阶段，组件化的优势同样显著。通过将系统划分为清晰界定的组件，开发者能够更加精准地定位问题所在，从而实施更加高效、精准的修复与升级策略。此外，由于组件间的松耦合设计，对某一组件的单独升级或改造几乎不会影响到系统的其他部分，这极大地降低了维护的复杂性与成本，确保了系统的持续稳定运行。

总之，组件化开发方式以其独特的优势，在大型软件工程的构建中发挥着不可替代的作用。

Rust语言本身具备良好的层次化模块系统，Rust的mod关键字用于定义模块，同时支持模块嵌套等操作，便于形成清晰的代码层级结构。Rust语言可以通过pub关键字来管理模块中相关数据和方法的可见性。通过在Cargo.toml文件中设置workspace等内容，可以方便的引入外部模块。另外，模块系统和文件系统具有一致性，对项目组织管理来说具有便捷性。

Rust语言本身也具有各类适合于组件化的语言特性。比如所有权机制，有利于在语言层面实现各个模块之间清晰的边界，为不同的模块所拥有的堆对象提供清晰的所有权机制；再比如Trait机制，为不同具体实现但提供相同对外接口的不同组件，提供了灵活的语言机制。这些语言层面的设计，对实现项目的组件化提供了支持。

Rust社区提供了各类已经经过良好封装和迭代的crate包，并通过统一的Cargo包管理工具，以及Cargo.lock来锁定版本等各类包管理方法进行各种crate包管理。目前官方的crate.io社区非常活跃，已有19w+的各类crate包。依托于方便的层次化模块系统，和Cargo工具，可以便捷地使用成熟的已有模块而无需重复造轮子。

在reL4项目支持aarch64架构的过程中，我们首先使用组件化的思想，将原有的仅支持riscv的reL4内核先拆分成为多个组件化的模块，具体分为六个模块，分别为

• common：最底层的支持，提供各类reL4的基础数据结构，宏定义等内容。
• cspcae：提供了L4系列微内核所特有的capability的管理机制，维护了包含所有capability的表格，即cspace，包含了capability的插入删除和各类管理方法。
• vspace：提供了微内核的地址空间相关的操作。
• task：提供了微内核的任务管理相关基本操作。
• ipc：提供了微内核的进程间通信的相关操作。
• kernel：kernel作为整个项目最顶层的上层模块，在上述几个模块的基础上，对传入给kernel的syscall进行了解析。

另外，随着内核被拆分成为多个组件，而每个组件都放置在多个不同的github仓库中，按照组件化的思想每个组件单独维护，从而在多个仓库之间的协同工作引发了组件间的同步问题。为此，我们也创新地设计了大小仓库协同工作的协作范式。

一方面，我们承认使用组件化的思想，将组件拆分为不同仓库。另一方面，在多仓集成的开发环境和代码快速迭代的开发条件下，使用单个仓库，具有较高的开发效率。为此，我们同时维护一个大仓库和一个小仓库，并在进行git push等操作时进行同步，从而实现大小仓库协同开发的方案，同时具有组件化的可重用性和单一仓库的快速迭代优势。

我们使用git-subrepo工具，替代简单的git和submodule所存在的大小仓库同步不便的问题。该工具可以单独使用类似于git subrepo push sub-module-dir的命令，提交某个子仓库，也可以使用传统的git方式，push整个大仓库。

同时，为了自动化地便捷开发，我们在该工具的基础上改写了github的ci脚本，在触发了push的ci操作的时候，能够自动触发git subrepo的push操作，同步到多个子仓库中，并单独触发多个子仓库各自的ci，从而实现大小仓库的协同工作。

4.3.2 reL4的aarch64支持 #

在经过组件化改造之后的reL4的基础上，我们也实现了reL4的aarch64的支持。这涉及到多个不同的模块，每个模块下都有相应的arch文件夹和其他架构无关的代码，以提供不同的，具体来说如下：

common模块：第一，该模块需要提供各类基础数据结构的定义，其中包括ArchTCB中的定义，用于在上下文切换时候的寄存器的保存，由于aarch64和riscv64下的寄存器存在差异，因此需要为不同的架构提供不同的寄存器上下文保存区域。第二，包含了各类不同架构下的常量定义，第三，在进入内核的时候，会通过寄存器传递一些参数和信息，在不同架构下使用不同的寄存器进行参数的传递，同时，在不同架构下传递的信息内容也有不同，例如，向内核传递页表相关的操作请求，在不同架构下具有不同的含义。这些内容都需要分别维护

cspace模块：在cspace模块中，只有capability的管理，而在aarch64和riscv64两个架构下，具有不同的跟arch相关的capability，因此，在cspace模块下，需要为不同的arch实现公共的capability的操作处理。

vspace模块：在aarch64和riscv64架构下的页表项结构和虚拟内存管理具有非常明显的差异，因此，这个模块也有非常大的改动。第一，该模块提供了不同结构下的页表项的定义和相关页表操作的实现，也包括asid和刷新tlb等架构强相关内容。第二，在内核启动的时候，需要为内核映射相关区域的虚拟内存，这部分的处理也具有架构差异。

kernel模块：作为系统的顶层模块，必须处理架构相关内容。第一，在调用vspace的跟页表相关内容的基础上，同样需要增加其他的各类boot的代码。第二，在该模块主要负责对各类传入的syscall的解析，其中也包括跟架构相关的capability和message info的解析，这部分需要架构相关的处理。第三，aarch64使用Gic，具体来说是Gicv2，而riscv64使用plic作为外部中断控制器，在不启用其他外设的情况下，仍然需要时钟中断作为任务调度的基础，riscv64可以使用sbi直接提供中断，但是aarch64则必须启用Gic，这部分的处理具有差异，第四，对于从用户态进入内核的汇编代码，也有所不同，aarch64根据不同的el等级不同的sp和aarch64和aarch32的差别，以及中断原因是sync、irq、fiq或者SError等原因，构成四个大类共16个表项的中断向量表，而riscv则使用stvc寄存器存放中断向量并可选择向量模式还是单入口模式。而上下文保存的寄存器也各有不同，因此，这部分需要处理架构相关。

另外的ipc模块和task模块，由于组件化设计下良好的模块化抽象，没有单独的跟arch相关的代码，由此可见，组件化设计所具有的优势。

经过上述改造，reL4能够同时支持riscv64及aarch64两个不同的硬件架构。

4.3.2.1 Arm的SMC call的支持 #

4.3.2.2Arm的ptmr和pcnt的支持 #

4.3.3 reL4的mcs特性支持 #

4.3.3.1 reL4中MCS(mixed-criticality system)策略概述 #

reL4中的MCS特性，主要基于Lyons（2017）的论文，

4.3.3.2 reL4中实现MCS特性概述 #

为了实现reL4对MCS特性的支持，需要做如下更改：

首先需要更改pbf文件，添加相应的sched_context（后文简称为sc）的capability的描述。

其次，MCS特性主要用于对进程实时性的控制，因此，必须添加相应的时钟模块以提供较为精准的定时等操作。在riscv64下，时钟模块主要使用sbi来进行设置，但是在aarch64下，情况较为复杂，在不同的开发板中，具有不同的时钟模块和相应的操作，并通过设备树文件传递给内核，在原有的seL4下也针对不同的时钟模块提供了相应的支持，但对于不同板级的描述则主要通过cmake文件和h文件中的定义，手动解析相关内容，并静态编译到内核中，而非自动解析设备树的方式来确定板级时钟支持情况。

由于目标平台仅为简单的qemu，无需过于强调板级兼容，reL4在这方面的处理为，抽象了一个platform子模块，并设计了一个trait来描述时钟的行为

pub trait Timer_func {
    fn initTimer(self);
    fn getCurrentTime(self) -> ticks_t;
    fn setDeadline(self, deadline: ticks_t);
    fn resetTimer(self);
    fn ackDeadlineIRQ(self);
}

将时钟的行为简单抽象为这样的对外接口。并在时钟中断的处理过程中，使用这些trait，同时也为后续的板级兼容做更多的准备。

第三，需要增加基础数据结构sched_context的实现。sc是实现整个MCS特性的基础数据结构，它的主要实现方式为：

第四，增加reply的支持，修改相关的tcb，endpoint等结构体。

第五，增加timeout的消息传递支持

第六，修改调度器实现重填机制

4.3.4 reL4的smp特性支持 #

4.3.5 reL4的fpu特性支持 #

4.4 支持reL4构建的辅助工具实现 #

4.4.1 reL4的xtask构建脚本支持 #

4.4.2 reL4的pbf文件格式解析支持 #

4.4.3 reL4的集中配置脚本支持 #

4.5 本章小结 #

5 C to Rust：内核在不同语言间迁移的经验和教训 #

在reL4内核的实践中，为了支持seL4的所有测例和一些seL4下的特殊机制，我们大量参考了seL4的内核实现，并完成了从C代码到Rust代码的一个手工转换。同时，在整个转换过程中，我们也处理了涉及到make、Cmake、Python、git、github ci、dockerfile、C、asm、Rust、json、toml甚至包括seL4自己设计的pbf语言等多种构建语言、脚本语言和编程语言的复合工作。

除了内核编写过程中必须存在的对特殊寄存器读写和特权指令使用导致的unsafe以外，由于seL4的syscall接口设计本身跟面向用户态的库和seL4生态深度绑定，为了实现seL4内核进行syscall接口层面的二进制兼容，我们也不可避免地在内核中大量使用unsafe语句，其中最典型例子就是前文所说的对capability的unsafe的强制转换。既然在reL4中使用unsafe无可避免，如何进行合理的封装等操作，来尽量防止unsafe代码的不合理使用对内核安全性的影响，是将一个项目从C转为Rust的重要问题。

为此，我们也总结了一些将一定规模的、深刻关联到硬件底层的C代码项目转换为Rust项目的经验和教训。

5.1 Rust语言在reL4内核中的安全优势 #

此部分很重要。详细阐述你是如何利用Rust的内存安全（所有权、借用、生命周期）、并发安全性（无数据竞争）、零成本抽象、强大的类型系统、模式匹配以及宏等特性来设计和实现reL4的各个模块。对比传统C/C++语言在这些方面可能面临的问题，突出Rust的解决方案。

5.2 从seL4迁移到reL4的实践路径 #

虽然seL4是一个微内核，但他仍然是一个非常复杂的系统，如果完全从头开始构建兼容seL4内核的reL4而不加测试，无疑会引入各类bug。但是引入测试来验证代码的正确性，同样也存在实践路径的方案问题，每添加一行代码就检查是否跟seL4的内核行为一致，是非常昂贵的，而即使是以一个或若干个函数为单位的增量作检查，也需要引入足够的测例来检验功能正确性，甚至由于其本身是一个内核项目，会存在部分代码的难以单独测试性。

因此我们仿照忒修斯之船实行了一个逐步替换的方案。锚定所有的seL4相关仓库的版本之后，先将部分C代码转换为Rust代码并在C仓库中注释掉这部分代码，再将对应的Rust代码编译成为一个静态链接库，链接到对应的C代码，暴露给C代码的Rust接口函数，由于Rust编译器会对函数名做一定的处理，需要通过在Rust代码中声明#[ no_mangle ]，再通过ffi的方式进行链接。

在一步步地完成了所有函数的替换工作之后，对构建脚本和启动相关内容稍作调整，即可变成一个完整的独立的Rust内核。

在构建出完整的Rust内核之后，再进一步地对reL4内核进行代码质量的优化：控制其所有的unsafe代码的范围，并审计检查这些unsafe代码;使用更加符合Rust的语法来进一步重构代码;使用更进一步的组件化方法，对内核的基础模块进行拆解并促进组件化操作系统的发展等。

这样做有极大的开发和调试方面的优点。首先，只替换掉部分函数并且不大量地改动构建脚本，意味着具有一个较为完整的seL4内核支持，可以在一开始就进行完整的seL4内核测例测试，函数级的增量改动并测试，能够较为方便地进行重构过程中的代码错误定位。同时，这也兼顾了开发的效率和速度问题，使用github的ci功能，可以在每次提交更改的时候进行seL4内核测例的测试，可以快速地判断新增的增量代码是否有效。

5.3 从bug分析与修复来看待操作系统开发中如何正确使用Rust的unsafe #

正如本章第一节所述。Rust相比于C语言的代码具有内存安全方面的优势。但是在将seL4的C代码转换为Rust代码的过程中，也遇到过各类跟内存bug。这显然不是Rust语言本身设计的问题，而是程序员对于unsafe部分的处理存在失误所导致的。当然，尽管如此，这些bug的触发和修复过程，同样涉及到操作系统开发中各个方面的知识，因此，本节会给出具体的案例来说明，在操作系统开发中需要如何正确地对待Rust的unsafe。

6 reL4-Linux-kit用户态兼容层 #

6.1 reL4-linux-kit设计目标和原则 #

以seL4为代表的微内核完成了最小化的微内核的设计实现,但是一个完整的可用的微内核操作系统并不仅仅包含kernel,还需要各类用户态的各类系统服务组件的支持。

当然，seL4微内核项目并不只有一个内核，也包含了众多的用户态库的支持，现有的基于seL4项目的其他内核项目，也都或多或少实现了seL4微内核的用户态组件。但是，他们大多是基于C语言实现的，正如前面针对seL4的安全验证与形式化证明中分析的那样，即使seL4内核中完成了形式化证明，但是由于其验证边界仅仅为内核，在用户态的各类系统服务，同样需要通过严格的验证才能保证足够的安全性。而这对于基于C语言实现的整个系统而言同样是困难的。

相反的，基于Rust内存安全语言来实现微内核的用户态系统组件，可以更好的提升用户态的内存安全。另外，Rust语言发展到现在，也有一些seL4环境下的Rust库可以服用，比如rust-seL4项目，初步完成了对于seL4原生用户态库的Rust环境支持。因此reL4-linux-kit希望使用内存安全语言Rust,在已有的Rust编写的reL4微内核和相应的Rust库的基础上，编写若干同样基于Rust语言的用户态系统服务组件。

同时，虽然seL4微内核对基本的内核操作提供了支持，但是，其缺少一定的应用生态，这一定程度上制约了其发展，而seL4也往往被设计实现为一个特定场景下的专用操作系统的内核，而不是一个通用操作系统的内核。针对这一点，reL4-Linux-kit希望可以通过将syscall转变为IPC的技术，将通用操作系统（如Linux）的系统调用，发送到系统服务进程进行相应的处理，从而支持通用操作系统的syscall,提升reL4微内核系统的通用性。

当然，内核服务的所有组件都进行了拆解并进行通信必然带来一定的通信成本的开销，以鸿蒙微内核的实现作为参考，为了缓解IPC的通信代价，在某些时候，可以将灵活的将若干个内核模块组合起来，IPC的通信转为最常见的函数调用，降低模块间的通信。

最后，展望未来，基于微内核的权限隔离的功能，我们可以在seL4的基础上，支持互相隔离的多个宏内核的实现，提供云和serverless等新型需求的基础支持。

虽然我们试图实现一个支持Linux syscall的系统，但是，它和已有的其他支持Linux syscall的微内核实现方案也有本质性的差别。

以L4Linux为代表的技术路线，是将一个完整的Linux内核通过一些裁剪、改写等手段，直接作为一个用户态的进程运行在用户态，该方案的优点在于，兼容Linux意味着微内核具备了良好的通用性，但该方案的问题在于，Linux本身由于宏内核过于复杂带来的安全性问题，并没有因为使用了微内核作为基础而得到缓解，同时，把内核放在用户态反而还引入了更多的性能开销。与之相对的，reL4-Linux-kit一方面用Rust语言进行了从头开始的构建而非简单的拼接，同时实现了多个系统组件，设计了组件间的通信机制，而不是集中式的把他们塞到一个单独的内核进程中，是一个更为符合微内核原生生态且兼顾安全性的方案。

除此之外，hypervisor的方案，则是利用seL4提供的hypervisor的功能，在其之上再封装一个虚拟化层，在该虚拟化层中运行操作系统，而reL4-linux-kit试图在seL4二进制兼容的reL4内核上，则直接去除了这层虚拟化层的封装，试图提供更贴近底层的方案，这在一定程度上对性能的提升具有正面作用。

基于以上考量，我们提出了以下reL4-linux-kit的基本设计目标和原则：

• 使用reL4微内核作为基础内核，使用已有的成熟rust-seL4用户态库等模块提供的运行时支持
• 使用Rust语言从头编写若干系统服务组件
• 通过syscall转IPC技术，兼容现有的Linux用户态进程
• 可以灵活的在系统服务组件间转换IPC call和function call的使用，实现模块间灵活的拼合和拆分。

6.2 root-Task与用户态进程管理 #

root-task是内核启动后运行的第一个进程，需要承担整个系统服务中最重要的工作。

首先，root-task需要启动系统中的其他进程。在这一步，需要设计好配置文件，在root-task启动执行的时候，解析该配置文件，并根据该配置文件给出的系统配置信息，启动所需的相关进程。

其次，在微内核启动之后，整个内核把最大的权限的capability集合都交给了root-task。因此root-task在启动其他进程的时候，需要对权限的派生等工作进行管理，以保证其他进程都获取合理的权限。

第三，root-task需要为其他进程间的通信建立合适的端口。正如前文所述，整个系统被拆分为多个系统服务组件进程，在各个相互依赖的服务组件之间，linux用户态进程和服务组件之间，都需要频繁地进行通信。而在seL4下，进程间通信都需要通过内核获得对应的endpoint capability，因此，reL4-linux-kit被设计为root-task必须在创建各个进程时提供自己的endpoint,各个进程可以通过该endpoint向root-task查询并申请需要建立通信的目标进程的endpoint，并基于申请到的endpoint再进行进一步的通信。

第四，root-task需要为其他进程提供基本的错误处理功能。在以Linux为代表的宏内核中，当一个进程产生了错误，会被内核接管并按照一定的策略进行处理，但是在微内核下，相关的错误只会导致内核将一个错误消息发送到用户态预先定义好的fault handler的endpoint上。

6.3 Linux系统调用兼容层 #

6.3.1 Linux用户态程序的二进制兼容方案 #

6.3.2 函数转IPC的方案 #

6.4 用户态核心服务模块 #

6.4.1 文件系统 #

6.4.2 网络系统 #

6.4.3 驱动程序 #

4 实验评估 #

reL4内核及测例编译方法 #

reL4内核使用xtask进行构建配置的支持，同时，为了能够集成式地支持用户态的开发，我们也构建了reL4-cli工具，以进一步地简化用户态开发流程。在此将对目前各种情况下的测试编译方法进行说明。

reL4测试seL4原生测例 #

在reL4中进行seL4原生测例主要用于内核开发过程中通过各个测例，本项目维护了一个docker环境，来提供稳定的开发环境。

# 首先在本地环境中下载相关仓库
# 如果只运行不进行push，下面repo init的链接可以改成https://github.com/reL4team2/rel4-dev-repo.git，否则您需要具有该仓库的权限
mkdir rel4_dev && cd rel4_dev
repo init -u git@github.com:rel4team2/rel4-dev-repo.git --repo-url=https://mirrors.tuna.tsinghua.edu.cn/git/git-repo/
repo sync

# 拉取镜像并进入docker中（这里最后的点是上面定义的文件夹名的路径）
curl --proto '=https' --tlsv1.2 -sSf https://raw.githubusercontent.com/rel4team2/build-scripts/refs/heads/master/scripts/start_docker.sh | bash -s -- .
# 或者其实可以第二种方式构建（遇到curl的网络问题可以使用）
cat ./build-scripts/scripts/start_docker.sh | bash -s -- .
docker exec -u ${USER} -it rel4_dev bash

# 在docker中运行sel4-test测试
# -p参数指定platform，目前可选为spike（riscv64）和qemu-arm-virt（aarch64）
# -m参数指定MCS特性（混合关键系统）开启（on）与否（off）
# -s参数指定arm平台下的SMC特性开启（on）与否（off）
# --arm-ptmr参数开启arm平台下的KernelArmExportPCNTUser，默认关闭
# --arm-pcnt参数开启arm平台下的KernelArmExportPTMRUser，默认关闭
# --bin参数启用一个完整的rust内核，默认关闭并通过和原生seL4的C代码链接起来的方式构建以方便调试
# -N指定smp下使用的核心数量（需要在simulate的时候也增加--cpu-num参数），目前仅支持bin模式

cd rel4_kernel

# 参数根据上面的内容进行选择，以下仅为几个例子
cargo xtask build -p spike -m off -s on&& cd build && ./simulate && cd ..

# 使用smp的例子
cargo xtask build -p qemu-arm-virt -N 4 --bin && cd build && ./simulate --cpu-num 4 && cd ..

# 如果需要进行提交，exit命令离开docker，进入对应的文件夹进行提交

使用reL4-Linux-kit进行兼容Linux syscall的测例运行 #

为了让用户态快速地部署内核而无需跟运行内核测例一样，我们也实现了一个reL4-cli用于支持用户态reL4-Linux-kit的运行。 对于reL4-Linux-kit的使用，见该仓库的readme

# 下载该仓库代码，同样无需提交也可使用https的链接
git clone git@github.com:reL4team2/reL4-linux-kit.git

cd reL4-linux-kit

# 安装aarch64的musl gcc的工具链，如果已经安装请忽略
wget https://musl.cc/aarch64-linux-musl-cross.tgz
tar zxf aarch64-linux-musl-cross.tgz
export PATH=$PATH:`pwd`/aarch64-linux-musl-cross/bin

# 安装sel4-kernel-loader-add-payload
cargo install --git https://github.com/seL4/rust-sel4 --rev 1cd063a0f69b2d2045bfa224a36c9341619f0e9b sel4-kernel-loader-add-payload

# 下载seL4内核，如果需要使用reL4内核，见后文的reL4-cli使用
mkdir -p .env
wget -qO- https://github.com/yfblock/rel4-kernel-autobuild/releases/download/release-2025-03-26/seL4.tar.gz | gunzip | tar -xvf - -C .env --strip-components 1

#运行
tools/app-parser.py kernel-thread block-thread uart-thread
make disk_img
make run LOG=error

按照上述步骤即可正常运行，实际命令以该仓库readme为准

但是上述的代码是使用seL4作为内核来运行的，以下是使用reL4-cli构建的方式

# 安装reL4-cli工具
cargo install --git https://github.com/reL4team2/reL4-cli.git
# 在上述reL4-linux-kit的下载seL4内核的步骤，使用下面的命令替换以使用reL4，如果已经存在.env文件夹，需要清理
cd rel4-linux-kit
mkdir -p .env
rel4-cli install kernel --bin -P $(realpath .)/.env/seL4

对于reL4-cli工具的一些选项描述如下

Options:
  -p, --platform <PLATFORM>        The target platform to install [default: qemu-arm-virt]
  -m, --mcs                        Enable kernel mcs mode
      --nofastpath                 Disable fastpath
  -B, --bin                        Rel4 has two modes: - Binary mode (pure Rust) - Lib mode (integrates with seL4 kernel)
  -P, --sel4-prefix <SEL4_PREFIX>  [default: /workspace/.seL4]
  -h, --help                       Print help (see more with '--help')

具体选项请参考reL4-cli的help

使用特定的reL4内核和用户态程序进行构建运行 #

在使用reL4-cli工具时，其安装的reL4微内核是最新的主线分支的代码。但是如果需要进行代码调试，需要使用不在主线的代码，也可以在上述rel4-cli install kernel的步骤使用如下指令替换：

# 其中YOUR_REL4_INTEGRAL_PATH是本地的rel4_kernel仓库的路径
rel4-cli install kernel --bin --local ${YOUR_REL4_INTEGRAL_PATH}

即可在自定义的reL4内核上运行用户态测例。

reL4内核评测 #

reL4的原生seL4测例通过情况 #

在reL4内核添加相关feature之后，相关feature之间具有不同的组合，存在有的feature不能兼容，而有的feature需要同时出现等。原生的seL4的test依据不同的feature，在测试中也会给出不同的测试样例。在本章节，我们给出了reL4内核在我们的测试环境下，相关测例的通过和未通过的情况。

我们使用的测试环境为：

该表格的含义如下：纵轴为每个测例，横向为各个feature。如果某个测例需要相关feature。如测例1需要feature A和C，就会在测例1所在行的feature A和C所在格添加记录。在开启了feature A和C的情况下，如果这些测试可以正常通过，那么这些记录都会打上√，否则都会打上×（或者在备注中注明无法成功测试的原因）。

目前已经实现的feature所支持的测例均已成功运行。

reL4-linux-kit评测 #