How to use Genode with different kernels
Linux is used as the default kernel platform of the Genode OS distribution. Hence, documentation about using Genode on Linux is provided with the introductory documentation that comes with the source distribution.
NOVA is a so called microhypervisor - a modern high-performance capability-based microkernel for the x86 architecture with special support for hardware-based virtualization and IOMMUs.
- Bare hardware
The so-called hw base platform allows for the execution of Genode directly on ARM-based hardware platforms without relying on a separate kernel. For running Genode directly on the Pandaboard, please refer to the Pandaboard-specific documentation.
- Muen separation kernel
Muen is an open-source separation kernel for 64-bit x86 platforms. It is implemented in the safe SPARK programming language, which is able to formally verify the absence of implementation bugs such as buffer overflows, integer-range violations, and exceptions. With Genode running on top of Muen, a dynamic microkernel-based system can be executed within the static boundaries of one Muen partition.
Fiasco.OC is a modernized version of the L4/Fiasco kernel as it emerged from the L4/Fiasco code base. However, its kernel interface diverged entirely from the classical L4 API, towards a modern capability-based object-oriented model. Fiasco.OC supports x86_32, x86_64 alongside many ARM-based platforms, facilitates the use of hardware-based virtualization, supports SMP, accounts kernel resources, and implements capability-based security.
L4ka::Pistachio is a BSD-licensed L4 microkernel developed in joint work of the University of Karlsruhe and the DiSy Group of the University of New South Wales. It is the reference implementation of the L4 API version x.2, which is also referred to as L4 version 4. L4ka::Pistachio supports the IA32 and PowerPC CPU architectures.
OKL4 is a microkernel that is available as commercial and Sleepycat-style licensed version. It is developed by Open Kernel Labs and deployed on mobile phones and other embedded devices.
L4/Fiasco is a GPL-licensed L4 microkernel developed at the University of Technology Dresden. This kernel is optimized for low interrupt latencies. It implements the L4v2 API and supports IA32, AMD64, and ARM.