微内核介绍及值得关注的微内核系统列表( 三 )_今年有不少和微内核相关的新闻：6月28

“HURD”是一个间接递归缩写，来自“HIRD of Unix Replacing Daemons”，其中“HIRD”表示“HURD of Interfaces Representing Depth”。

seL4

seL4 Logo

2009年，Data61/CSIRO实现了对于其L4内核的形式化证明，并创造出世界上第一个此类的实用操作系统seL4。他们在2013年进一步证明了内核的信息流安全性，使得该系统成为最安全的操作系统之一。

Escape

Escape 是一个类Unix操作系统，可运行在 x86，x86_64，ECO32 和 MMIX 上。这是一个完全重新实现的系统，几乎没有使用第三方组件。为了符合Unix哲学，Escape使用虚拟文件系统来提供驱动和服务，这两者都对于用户来说看作是文件系统或者文件。

Huawei 鸿蒙 OS

由于使用被隔离的微内核设计，鸿蒙 OS 无法被取得 root 权限，在根本上有着更高的安全性。该系统同时使用形式化验证（Formal Verification）的方式，以更可靠地找出漏洞。虽然是个轻量的系统，鸿蒙 OS 提供了不少性能上的增进。首先，是一个名为「决定性延迟引擎（Deterministic Latency Engine）」的功能，让系统依据当下的资源用量分析，预测出更好的资源分配成式。鸿蒙 OS 并且有着更快速的跨程序通讯，让微内核和文件系统、网络、驱动程序、软件等之间，有着更快的通讯速度。