Muen是Ada语言实现的高可靠分离内核（微内核）操作系统。
概述
MuenSeparationKernel是世界上第一个被正式证明在源代码级别不包含运行时错误的开源微内核。它是由瑞士应用科学大学Rapperswil（HSR）的网络解决方案研究所（INS）开发的。Muen专门设计来满足英特尔X86／64平台上高可靠性系统的挑战性需求。为了确保慕恩适用于高度关键的系统和先进的国家安全平台，HSR与德国的高安全专家安全网络公司密切合作。
实例体系结构
分离内核(SK)是一种专用的微内核，它为根据给定的安全策略专门通信、在其他方面彼此严格隔离的组件提供执行环境。隐藏的信道问题，在很大程度上被其他平台忽略，是由这些内核明确地解决的。SK通常比动态微内核更静态和更小，这最小化了内核失效的可能性，使得能够应用形式化验证技术和减轻隐蔽信道。
MUN使用英特尔的硬件辅助虚拟化技术VT-X作为核心机制来分离组件。内核在VMX根模式下执行，而用户组件（所谓的主体）运行在VMX非根模式中。硬件通过是通过英特尔的VT-DDMA和中断重映射技术实现的。这使得PCI设备能够安全地分配给受试者。
特征
内核
下面的列表概述了MUEN内核的最突出的特点：
英特尔SX86／64架构中的SK2014的最小SK
完全可用的源代码和文档
运行时错误不存在的证明
多核载体
嵌套分页（EPT）和内存分型（PAT）
使用英特尔VMX抢占定时器的固定循环调度
根据系统策略静态分配资源
使用英特尔VT-D（DMAR和IR）的PCI设备通过
PCI配置空间仿真
支持消息信号中断（MSI）
最小零占用运行时间（RTS）
事件机制
用于主题间通信的共享存储信道
碰撞审计
支持64位原生和32/64位虚拟机主体
原生64位Ada主题
原生64位火花2014受试者
Linux32/64位虚拟机
GENODEX86Y64基HW系统[基因型]
Windows32位虚拟机
MiRaGOS单内核[MiGaReOS]
Muen通过使用运行在Genode的base-hw内核之上的强隔离VM主题中的完全去特权的VirtualBox[vbox]变体，支持MicrosoftWindows的硬件加速虚拟化。请参阅GeNODEOS框架版本16.08[GeoDeEx-Mue]的发布说明，以了解更多关于这个令人兴奋的特性的信息。
组件
MUEN平台包括实现公共服务的可重用组件：
在SCAP2014中编写的设备管理器
星火2014编写的主题监视器（SM）
用星火2014编写的主题加载程序（SL）
SimeServer主题写在星火2014
用艾达2012编写的Debug服务器主题
艾达2012编写的PS/2驱动程序主题
艾达2012编写的虚拟终端（VT）主题
此外，[muenfs]和[muennet]Linux内核模块提供基于主题间存储器通道的虚拟文件系统和网络接口驱动程序。
评论