Ada 语言实现的高可靠 x86/64 分离内核 Muen

Ada 语言实现的高可靠 x86/64 分离内核 Muen

GPL
Ada 查看源码»
未知
2018-08-30
OJOIN

Muen 是 Ada 语言实现的高可靠分离内核(微内核)操作系统。

概述

Muen Separation Kernel是世界上第一个被正式证明在源代码级别不包含运行时错误的开源微内核。它是由瑞士应用科学大学Rapperswil(HSR)的网络解决方案研究所(INS)开发的。Muen专门设计来满足英特尔X86/64平台上高可靠性系统的挑战性需求。为了确保慕恩适用于高度关键的系统和先进的国家安全平台,HSR与德国的高安全专家安全网络公司密切合作。


实例体系结构

分离内核(SK)是一种专用的微内核,它为根据给定的安全策略专门通信、在其他方面彼此严格隔离的组件提供执行环境。隐藏的信道问题,在很大程度上被其他平台忽略,是由这些内核明确地解决的。SK通常比动态微内核更静态和更小,这最小化了内核失效的可能性,使得能够应用形式化验证技术和减轻隐蔽信道。

MUN使用英特尔的硬件辅助虚拟化技术VT-X作为核心机制来分离组件。内核在VMX根模式下执行,而用户组件(所谓的主体)运行在VMX非根模式中。硬件通过是通过英特尔的VT-D DMA和中断重映射技术实现的。这使得PCI设备能够安全地分配给受试者。

特征

内核

下面的列表概述了MUEN内核的最突出的特点:

  • 英特尔SX86/64架构中的SK 2014的最小SK

  • 完全可用的源代码和文档

  • 运行时错误不存在的证明

  • 多核载体

  • 嵌套分页(EPT)和内存分型(PAT)

  • 使用英特尔VMX抢占定时器的固定循环调度

  • 根据系统策略静态分配资源

  • 使用英特尔VT-D(DMAR和IR)的PCI设备通过

  • PCI配置空间仿真

  • 支持消息信号中断(MSI)

  • 最小零占用运行时间(RTS)

  • 事件机制

  • 用于主题间通信的共享存储信道

  • 碰撞审计

  • 支持64位原生和32/64位虚拟机主体

  • 原生64位 Ada 主题

  • 原生64位火花2014受试者

  • Linux 32/64位虚拟机

  • GENODE X86Y64基HW系统[基因型]

  • Windows 32位虚拟机

  • MiRaGOS单内核[ MiGaReOS]

Muen通过使用运行在Genode的base-hw内核之上的强隔离VM主题中的完全去特权的VirtualBox[vbox]变体,支持Microsoft Windows的硬件加速虚拟化。请参阅GeNODE OS框架版本16.08 [ GeoDeEx-Mue]的发布说明,以了解更多关于这个令人兴奋的特性的信息。

组件

MUEN平台包括实现公共服务的可重用组件:

  • 在SCAP 2014中编写的设备管理器

  • 星火2014编写的主题监视器(SM)

  • 用星火2014编写的主题加载程序(SL)

  • SimeServer主题写在星火2014

  • 用艾达2012编写的Debug服务器主题

  • 艾达2012编写的PS/2驱动程序主题

  • 艾达2012编写的虚拟终端(VT)主题

此外,[muenfs]和[muennet]Linux内核模块提供基于主题间存储器通道的虚拟文件系统和网络接口驱动程序。

的码云指数为
超过 的项目
加载中

评论(1)

超级大黑猫
超级大黑猫
这翻译的真差。。。。

暂无资讯

暂无问答

暂无博客

返回顶部
顶部