背景介绍 #
seL4 作为完成了形式化验证的内核，其安全性和可靠性得到了一定程度上的保证。在近年来安全问题频发的场景下，用 seL4 构建适配更多场景的内核的需求也逐渐强烈起来。目前该方面已有一定的工作成果，本文仅介绍其中两个特定方向：
以 seL4 作为 hypervisor，在其上构建 guest OS： Virtualization on seL4 中描述了 seL4 为了支持虚拟化而封装的库。在这些库的作用下，可以完成基本的虚拟化支持。但目前的虚拟化基本仍然是以硬编码来确定 guestOS 的种类与数量的，并不十分灵活。
以 seL4 为底层基座，在其上构建异构的内核： seL4 as Hypervisor 描述了这类应用场景，他们计划将 Linux 等内核作为任务运行在用户态，并将驱动等模块分离出来作为其他辅助任务运行。目前该文档中仅描述了运行单个内核的情况，但是理论上可以同时运行多个内核，适配更多场景。
在前述工作的基础上，我们结合组件化的背景，希望完成如下任务：