GeezerVisonThe World Wide Web, restored to 800 pixels of glory. | |||||||||||||||||||||||||||||||||||||||||||
| Home|About|Gaming cabinet|Archives|How it works|Starter sites | |||||||||||||||||||||||||||||||||||||||||||
GeezerVison is showing muen.sk — Muen | SK for x86/64 OverviewMuen is an Open Source separation kernel (SK) for the Intel x86/64 architecture that has been formally proven to contain no runtime errors at the source code level. It is developed in Switzerland by codelabs GmbH. Muen was designed specifically to meet the challenging requirements of high-assurance systems on the Intel x86/64 platform. To ensure Muen is suitable for highly critical systems and advanced national security platforms, codelabs closely cooperates with the high-security specialist secunet Security Networks AG in Germany. 
A separation kernel is a specialized microkernel that provides an execution environment for components that exclusively communicate according to a given security policy and are otherwise strictly isolated from each other. The covert channel problem, largely ignored by other platforms, is addressed explicitly by these kernels. SKs are generally more static and smaller than dynamic microkernels, which minimizes the possibility of kernel failure, enables the application of formal verification techniques and the mitigation of covert channels. Muen uses Intel’s hardware-assisted virtualization technology VT-x as core mechanism to separate components. The kernel executes in VMX root mode, while user components, so called subjects, run in VMX non-root mode. Hardware passthrough is realized using Intel’s VT-d DMA and interrupt remapping technology. This enables the secure assignment of PCI devices to subjects.
FeaturesKernelThe following list outlines the most-prominent features of the Muen kernel:
Tau0Tau0 (τ₀) is the Muen System Composer. In its current static mode of operation, the task of Tau0 is to compose a system image while making sure that certain invariants are not violated. The Tau0 concept is a mechanism to gradually increase the flexibility of component-based systems running on top of Muen, while keeping a high level of assurance regarding the correctness of isolation enforcement. Read more about Tau0 here. ComponentsThe Muen platform includes re-usable components which implement common services:
Furthermore the [muenblock], [muenevents], [muenfs] and [muennet] Linux kernel modules provide block I/O, inter-subject event, virtual filesystem and network interface drivers based on inter-subject memory channels. ToolchainThe Muen platform includes a versatile toolchain which facilitates the specification and construction of component-based systems in different application domains. The [mugenhwcfg] tool for automated hardware description generation simplifies the addition of support for new target machines. There is also a Debian Live-based bootable image [mugenhwcfg-live] with persistence to simplify the collection of hardware configurations from new targets. ResourcesDocumentationThe following detailed project documentation is available:
Mailing listThe [email protected] mailing list is used for project announcements and discussions regarding the Muen separation kernel.
Tested HardwareThe following hardware is used for the development of Muen. There is a good chance similar hardware works out-of-the box if the microarchitecture is Ivy Bridge or newer. Intel x86
Building MuenPrerequisitesMuen is built using the Bob Build Tool [bob], install it via $ pipx install BobBuildTool Further variants of installing bob are described here: https://bob-build-tool.readthedocs.io/en/latest/installation.html#install. We recommend using the following bob user configuration in
Replace the example number 32 with your desired job count (e.g. number of CPU
cores of your build machine). The Once bob is ready, clone the Muen recipes and update all layers: $ git clone --recurse-submodules https://git.codelabs.ch/bob/muen.git $ cd muen $ bob layers update Deployment & TestingEmulationTo ease kernel development and testing, the Muen project makes use of nested virtualization provided by QEMU/KVM. Issue the following command in the project directory to start the Muen system in QEMU: $ contrib/runQemu.py -q x86-qemu-debug The system serial output is written to
To run an ARM64 system execute $ contrib/runQemu.py -q arm64-qemu-zcu102-minimal-debug It’s also possible to run all virtualized scenarios via the continuous integration (CI) system: $ ci/run.sh -a output This will build and test all QEMU-emulated systems automatically, writing all
artifacts to the given $ ci/run.sh -a output -r x86-qemu-debug See HardwareTo build a bootable ISO file, execute the following command: $ bob dev x86-t430s-debug This will build a system for the Lenovo T430s hardware which can be dumped on a
USB stick. If the desired system is not already present when executing the To build the minimal demo for the Xilinx MPSoC execute: $ bob dev arm64-xilinx-zcu104-minimal-debug Then copy References
LicenseUnless otherwise noted, this project and its sub-projects are licensed under the GNU General Public License v3.0 (GPLv3) or (at your option) any later version. Specific libraries are licensed under the BSD License to provide additional flexibility for commercial use. Furthermore, the interfaces between the kernel and subjects (virtual machines / user programs) constitute GPL boundaries. For authoritative information, please consult the file headers and any COPYING files within each sub-project. | |||||||||||||||||||||||||||||||||||||||||||
| You are visitor 01402503 — GeezerVison does not store the pages you look up. Best viewed with Netscape Navigator 4.7 or Internet Explorer 6 at 800×600. No cookies required. |