经过八年的开发，Muen 1.0项目发布，开发了Separation内核，并通过形式可靠性验证的数学方法确认了源代码不存在错误。该内核适用于 x86_64 架构，可用于需要更高级别的可靠性并保证无故障的关键任务系统。该项目的源代码是用Ada语言及其可验证方言SPARK 2014编写的。该代码在GPLv3许可证下分发。
分离内核是一个微内核，为相互隔离的组件提供执行环境，组件之间的交互受到给定规则的严格控制。隔离基于 Intel VT-x 虚拟化扩展的使用，并包括阻止秘密通信通道组织的安全机制。分区内核比其他微内核更加简约和静态，从而减少了可能导致失败的情况。
内核以 VMX 根模式运行，类似于虚拟机管理程序，所有其他组件以 VMX 非根模式运行，类似于来宾系统。使用 Intel VT-d DMA 扩展和中断重新映射对设备进行访问，从而可以实现 PCI 设备与 Muen 下运行的组件的安全绑定。
Muen 的功能包括支持多核系统、嵌套内存页面（EPT，扩展页表）、MSI（消息信号中断）和内存页面属性表（PAT，页面属性表）。 Muen 还提供基于 Intel VMX 抢占式计时器的固定循环调度程序、不影响性能的紧凑运行时、崩溃审核系统、基于规则的静态资源分配引擎、事件处理系统以及共享内存通道。运行组件内的通信。
它支持运行具有 64 位机器代码的组件、32 位或 64 位虚拟机、Ada 和 SPARK 64 语言的 2014 位应用程序、Linux 虚拟机以及基于 Muen 之上的 MirageOS 的独立“unikernels”。
Muen 1.0版本中提供的主要创新：
- 已发布包含内核（设备和架构）、系统（系统策略、Tau0 和工具包）和组件规范的文档，记录了该项目的各个方面。
- 添加了 Tau0（Muen System Composer）工具包，其中包括一组现成的经过验证的组件，用于构建系统映像和开发在 Muen 之上运行的标准服务。提供的组件包括AHCI驱动程序（SATA）、设备管理器（DM）、引导加载程序、系统管理器、虚拟终端等。
- muenblock Linux 驱动程序（在 Muen 共享内存之上运行的块设备的实现）已转换为使用 blockdev 2.0 API。
- 实现了用于管理本机组件生命周期的工具。
- 系统映像已转换为使用 SBS（签名块流）和 CSL（命令流加载器）来保护完整性。
- 已实施经过验证的 AHCI-DRV 驱动程序，该驱动程序以 SPARK 2014 语言编写，允许您将支持 ATA 接口或单个磁盘分区的驱动器连接到组件。
- 改进了 MirageOS 和 Solo5 项目的 unikernel 支持。
- Ada 语言工具包已针对 GNAT Community 2021 版本进行了更新。
- 持续集成系统已从Bochs模拟器转移到QEMU/KVM嵌套环境。
- Linux 组件映像使用 Linux 5.4.66 内核。
来源： opennet.ru