微内核发展史和微内核seL4

### 背景庞大的UNIX家族
UNIX系统，1971年诞生于大名鼎鼎的贝尔实验室的一台PDP-11/24机器上，其后经过不断发展与传播，在80年代取得了巨大成功，UNIX被移植到众多的处理器架构，并在众多行业得到广泛使用，甚至成为行业标准影响至今。

#### UNIX以及类UNIX系统如Linux都是典型的宏内核设计
也就是把所有系统服务都放到内核里，因为系统服务代码之间存在大量数据交换和大量的服务请求，而在同一个代码段内进行函数调用(C语言)或跳转(汇编或者机器码时代)是最直接、最高效的方法，在同一片地址空间也方便数据交换，所以这样的宏内核设计是很自然的。

但是随着UNIX内核功能的拓展(文件系统、TCP/IP网络协议栈、进程管理、内存管理、驱动程序等)，UNIX内核代码也相应增加了很多，进而在可维护性.稳定性，安全性方面面临一些挑战。为了试图解决这些挑战，人们开始尝试使用微内核的思想来设计系统内核。

### 什么是微内核?

微内核设计的基本思想是简化内核功能，在内核之外的用户态尽可能多地实现系统服务，同时加入相互之间的安全保护。内核只提供最基础的服务，比如多进程调度、多进程通信（IPC)等。其中进程通信是作为连接应用与用户态系统服务的桥梁。

宏内核系统相关的服务基本都是放于内核态内核中，例如文件系统、设备驱动、虚拟内存管理、网络协议栈等；而微内核则把更多的系统服务（例如文件系统、POSIX服务、网络协议栈甚至外设驱动）放到用户态应用，形成一个个服务，等待其他应用的请求。而后来，为了在宏内核与微内核之间扬长避短，也发展出了中间的混合内核的形态，部分服务也会放置于内核中。

### 微内核的发展历史

微内核这个概念从提出开始就在不断地发展、完善进步之中，到目前为止可以分为三代。

### 第一代微内核：从无到有

第一代微内核的主要代表是Mach，该系统由卡内基-梅隆大学的Avie Tevanian和Richard Rashid主导开发。在Mach刚刚开始设计时，UNIX的发展正如日中天，所以Mach在设计时的一大目标就是兼容UNIX，但是与UNIX不同的是Mach尝试使用微内核架构去设计。Mach以IPC是作为所有系统服务与内核交换数据的基础机制，充分运用IPC、虚拟内存、多进程等特性将冗余的系统服务移出内核作为进程运行。

1986年，经过两年的开发，第一版的Mach发布后的第二年，Mach就发布了第2版，不过由于时间仓促，加之没有足够的人手与资金，所以此时Mach内核并不提供完全的系统服务。为了支撑系统上层运行，这一版的内核包含了大量4.3版本的BSD系统(UNIX的一个分支)代码提供系统服务，并且BSD系统服务运行在内核状态，这导致Mach内核的代码体积甚至大于常规UNIX内核。第一版和第二版的Mach主要做了如下工作：1. 验证了微内核的可行性；2. 在多处理器计算机上进行移植验证了微内核在多处理器计算机上的运行；3. 最后为了提高IPC的效率，Mach使用共享内存机制来完成IPC。而Mach的共享内存机制是在虚拟内存技术的支持下实现的，只有需要对内存进行写入时才进行复制。这么一处理比每次都复制一遍内存节省了内存使用同时又加快了IPC机制的处理时间，这个改进称为写时复制，并且在如今的通用操作系统如Linux中常常用到。

经过测试，Mach 2.5的效率最多比UNIX少25%，但是考虑到Mach带来的可靠性、可拓展性、安全性，这个效率损失尚可以接受。当然此时Mach内核还不算完全的微内核。而考虑到微内核可以更高效地利用多处理器计算机的处理器核心资源，人们期待着等Mach把系统服务都搬到内核之外后可以把运行效率损失降下来。同时Mach在微内核方面小小的尝试迅速吸引了大批公司与组织的注意，开放软件基金会(Open Software Foundation， OSF)宣布下一代系统OSF/1将基于Mach的内核， NeXTSTEP也将使用Mach2.5， 甚至IBM也打算利用Mach构建Workplace OS。苹果公司这个时候也出手了，苹果公司也从此基于Mach2.5打造其操作系统内核XNU，XNU的构成如下图所示，Mach作为内核的内环，外环右侧是苹果的驱动框架（I/O Kit），外环左侧是BSD的系统服务代码提供UNIX兼容的服务层，这三者共同协作向上层提供完整的系统服务。XNU广泛地使用在苹果公司的OSX，IOS等系统中。

这个时候由于UNIX系统广泛使用带来的商业利益，此时BSD系统开发者与UNIX的拥有者AT&T陷入了法律大战，Mach使用的BSD相关代码有了法律风险。提升性能的期望和规避法律风险的需求推动着Mach 3.0的开发，Mach 3.0的开发目标主要是为了替换BSD系统服务，同时尽量多地将系统服务放到内核之外去运行，成为名副其实的微内核设计。经过众多开发者3年的努力，Mach 3.0于1990年发布，但是由于在系统服务之间完全使用IPC通信，而不是向宏内核那样直接进行函数调用，即便是多处理器机器上运行也性能损失惨重，Mach 3.0最多比UNIX损失 67% 运行效率，这导致Mach 3.0以及其所代表的第一代微内核设计被看衰。此后断断续续有在Mach的基础上对性能进行提升的尝试，但是均不太理想，至此Mach成为了微内核第一代先驱者。

### 第二代微内核：解决性能问题

第二代微内核的主要代表是L3和L4，以及QNX系统使用的Neutrino内核。前面第一代的微内核Mach由于效率问题虽然失败了，但是微内核的理念并没有被放弃，德国的计算机科学家Jochen Liedtke认为Mach的IPC效率低下的原因就是因为IPC部分不够精简，于是他开发了L3和L4微内核，对IPC部分进行了很彻底的精简：1. 内核的IPC机制只是单纯地传递信息，诸如安全权限检查这类的代码都省略掉，省略掉的功能全部由用户进程自己处理。如此一来IPC功能部分的代码执行时间大大缩短；2. IPC不使用内存传递消息，而使用寄存器传递消息，同时限制IPC每次传递的信息长度，这样省去了对内存的访问时间。L4微内核的IPC速度经过测试要比Mach快20倍，这个令人惊讶的优化效果吸引了众多的目光，使微内核的研究重新火热起来。后面L4内核又发展出了很多相关系统，比如Pistachio，L4/MIPS，与Fiasco等等，这些内核组成了L4的大家族。

第二代微内核的代表除了有L4内核，也还有其他微内核比如Exokernel、Rambler等，不过商业上最成功的则是目前黑莓公司旗下的QNX系统所使用的Neutrino内核（QNX，1980年诞生，最初以QUICK UNIX为名，后改为QNX；2004年QNX被Harman国际收购；2010年Harman国际下被黑莓收购，QNX成为黑莓旗下的资产），QNX主要为高可靠领域提供解决方案，比如交通、能源、医疗、航天航空等。

### 第三代微内核：主要重视安全问题等

在前面两代的基础上，第三代微内核蓬勃发展，许许多多微内核都被开发出来，主要代表有：seL4、Fiasco.OC、NOVA等。本来第一代微内核的设计隔离了使内核安全性降低的系统服务，让系统服务漏洞不会影响内核，进而提高了内核安全性，可以说是关上了破坏系统的门， 但是第二代系统却又给攻击者开了个窗户；由于第二代微内核在内核中省去了关于安全性检查等步骤，把所有关于安全检查功能的实现都交给系统服务自己去实现，这导致系统服务的通信接口直接暴露给用户态，任何进程都可能无限制地请求系统服务，系统服务不得不花费额外的代价来区分请求是否合法，容易造成拒绝服务攻击。比如正常的文件服务应该是从虚拟文件系统服务->文件系统服务->磁盘驱动服务这个流程来完成的，但是如果攻击者如果绕过虚拟文件系统服务，直接无限制地请求攻击者本身没有权限访问的文件系统服务，使文件系统服务长期处于满载状态，让其他进程无法通过正常的虚拟文件系统得到文件系统服务。为了增强安全性，且不过分影响性能，人们开始研发第三代微内核。

seL4是在第二代内核L4的基础上发展而来的。seL4不仅仅继承了L4内核家族的高性能特性，还具备基于端点(enndpoint)的IPC机制。这种IPC机制最大的特点是使用了能力空间的概念，进程在使用IPC请求系统服务时必须具备相对应的能力，进程持有不可伪造的令牌来表示拥有请求某种服务的能力。令牌可以被复制，可以被转移，还可以通过IPC进行传输。

### 开源微内核seL4
微内核
越大的系统潜在的bug就越多。所以微内核在降低bug方面非常有优势，seL4是世界上最小的内核之中的一个。可是seL4的性能能够与当今性能最好的微内核相比。
作为微内核，seL4为应用程序提供少量的服务。如创建和管理虚拟内存地址空间的抽象，线程和进程间通信IPC。这么少的服务靠8700行C代码搞定。seL4是高性能的L4微内核家族的新产物，它具有操作系统所必需的服务。如线程，IPC，虚拟内存，中断等。

形式验证
除了微内核。seL4还有一大特色是全然的形式验证。

seL4的实现总是严格满足上一抽象层内核行为的规约，它在不论什么情况下都不会崩溃以及运行不安全的操作，甚至能够精确的判断出seL4 在全部情况下的行为，这是了不起的。

研究发现经常使用的攻击方法对seL4无效，如恶意程序经常採用的缓存溢出漏洞。
使用面向过程语言Haskell实现了一个内核原型，用它来參与形式验证，最后依据它，用C语言又一次实现内核，作为终于内核。 顺便提一句。seL4有两仅仅team。kernel team和verification team，而连接这两个team的是 Haskell prototype。

在用C开发内核的过程中，seL4对使用C进行了例如以下限制：
1. 栈变量不得取引用，必要时以全局变量取代
2. 禁止函数指针
3. 不支持union

对seL4的formal verification（形式验证）分为两步：abstract specification（抽象规范）和executable specification（可运行规范）之间。executable specification和implementation（实现）之间。

有两个广泛的方法来进行formal verification： model checking（全自己主动）和交互式数学证明（interactive mathematical proof ）。后者须要手工操作。

seL4验证使用的形式数学证明来自Isabelle/HOL，属于后者。

详细来说seL4的形式验证步骤：
1. 写出IPC、syscall、调度等全部微内核对象（kernel object）的abstract specification（in Isabelle）
2. 写出如上对象的executable specification（in Haskell）。并证明其正确实现了第一步的abstract specification。利用状态机的原理，abstract specification的每一步状态转换。executable specification都产生唯一相应的状态转换。
3. 写C实现。

通过一个SML写的C-Isabelle转换器，和Haskabelle联合形式证明C代码和第二步的Haskell定义语义一致。

seL4的实现被证明是bug-free（没有bug）的。比方不会出现缓冲区溢出，空指针异常等。还有一点就是，C代码要转换成能直接在硬件上运行的二进制代码。seL4能够确保这个转换过程不出现错误，可靠。seL4是世界上第一个（到眼下也是唯一一个）从非常强程度上被证明是安全的OS。

seL4 is the first (and still only) protected-mode OS kernel with a sound and complete timeliness analysis. Among others this means that it has provable upper bounds on interrupt latencies (as well as latencies of any other kernel operations). It is therefore the only kernel with memory protection that can give you hard real-time guarantees. 从这段英文能够看出，seL4的硬实时性非常强。
实际上OS的verification（验证）早在40年前就開始了，而seL4是振奋人心的，一是它拥有非常强的属性（properties）：功能正确性（functional correctness），完整性（integrity）和机密性（confidentiality）。二是这些属性已经被形式验证到代码级别，先是C，如今又到了二进制。

相比于之前人们对于OS的验证，seL4做得更彻底，但正是借助前人的工作，seL4才干如此优秀。

转载：
>https://news.eda365.com/tech/qrskaifa/120011106431565.html
https://www.cnblogs.com/yjbjingcha/p/8367078.html