The Muen Separation Kernel as Genode base platform Oct 02, 2015
Thanks to the close collaboration with Codelabs, Genode now supports the Muen separation kernel as base platform.
Separation kernels represent the most extreme form of kernel architectures with respect to software complexity. Such kernels are designed to partition the underlying hardware platform into a static set of domains. In contrast to a microkernel, no dynamic management of resources is performed at runtime. Resources like memory and CPU time are assigned to the domains at system- integration time. On the one hand, the rigidity of this approach limits its application areas. On the other hand, it allows the kernel to become even less complex than a microkernel, and thereby aid its thorough evaluation or even its formal verification. This, in turn, makes separation kernels attractive in application areas with high-assurance requirements.
Most separation kernels are proprietary software. However, with Muen, there exists an open-source separation kernel for the x86 architecture. Muen is developed by Codelabs in Switzerland. Apart from being open source, it is unique because it is implemented in the SPARK programming language, which guarantees the absence of implementation bugs like buffer overflows or integer overflows.
Thanks to the close collaboration between the Muen developers and our team, the assurance of the Muen separation kernel can now be combined with the rich component infrastructure provided by Genode. From Genode's perspective, Muen is another architecture for our custom base-hw kernel. In fact, with Genode on Muen, a microkernel-based system is running within the static boundaries of one Muen partition. This way, the component isolation enforced by the base-hw kernel and the static isolation boundaries enforced by Muen form two lines of defense for protecting security-critical system functions from untrusted code sandboxed within a Genode subsystem.
Genode Labs GmbH
Genode Labs GmbH