鸿蒙操作系统用的微内核到底是什么？( 三 ) _鸿蒙

由于第二代微内核在内核中省去了关于安全性检查等步骤，把所有关于安全检查功能的实现都交给系统服务自己去实现，这导致系统服务的通信接口直接暴露给用户态，任何进程都可能无限制地请求系统服务，系统服务不得不花费额外的代价来区分请求是否合法，容易造成拒绝服务攻击。
比如正常的文件服务应该是从虚拟文件系统服务->文件系统服务->磁盘驱动服务这个流程来完成的，但是如果攻击者如果绕过虚拟文件系统服务，直接无限制地请求攻击者本身没有权限访问的文件系统服务，使文件系统服务长期处于满载状态，让其他进程无法通过正常的虚拟文件系统得到文件系统服务。为了增强安全性，且不过分影响性能，人们开始研发第三代微内核。
seL4 是在第二代内核 L4 的基础上发展而来的。seL4 不仅仅继承了 L4 内核家族的高性能特性，还具备基于端点（enndpoint）的 IPC 机制。
这种 IPC 机制最大的特点是使用了能力空间的概念，进程在使用 IPC 请求系统服务时必须具备相对应的能力，进程持有不可伪造的令牌来表示拥有请求某种服务的能力。令牌可以被复制，可以被转移，还可以通过 IPC 进行传输。令牌其实是一个指向存在于内核空间内核对象的指针，所以普通进程并不能修改自身以及其他进程的权限分配，但是内核可以对令牌指定的权限进行控制，从而保证了用户态不能绕过能力空间这个机制对系统服务造成滥用。
seL4 还是第一个完全通过形式化验证的内核，通俗说形式化验证就是在数学软件的帮助下使用数学语言自动化地推导检查系统的每一个运行状态。seL4 形式化验证相关论文。
其他的微内核系统：Fuchsia、Minix
Fuchsia 是 google 开发的一款全新操作系统，试图覆盖手机、平板甚至笔记本等一系列领域。Google 为该系统配备了 Vulkan 图形接口、3D 桌面渲染 Scenic、Flutter 应用开发框架，还有一个称为 zircon 的微内核。
zircon 内核是从高通平台的一个 Bootloader 项目：Little Kernel发展而来。zircon内核属于微内核设计，只提供 IPC、进程管理、地址空间管理功能。zircon 区别于以进程或者以文件为核心的设计，zircon 是以内存为核心来设计的，内存在 zircon 中是以对象的方式存在，可以通过 channel 通信机制传递虚拟内存对象（Virtual memory object）的句柄，进程拿到句柄后可以把这块内存映射到自己的空间。
Minix 系统则由荷兰阿姆斯特丹的 Vrije 大学的 Andrew S.Tanenbaum 教授所开发。
该系统最大的特点是可以故障隔离，自动重启失败的服务。
Minix 使用分层设计，最底层的微内核提供中断处理、进程管理、进程通信等服务，这一层运行在内核态；中间层提供轮回服务（Reincarnation Server）、文件服务、进程管理、X 图形服务以及驱动等，这一层运行在用户态，最上层为用户进程。
其中轮回服务负责在中间层的服务出现崩溃时重启这些服务，从而保证服务的自我修复。Minix 由于其自我修复特性被英特尔管理引擎（ME）所选用，该管理引擎主要负责管理英特尔芯片的内部模块。