codelabs - High Assurance Systems
Microkernels - The component-based operating systems
An x86/64 Separation Kernel for High Assurance
Muen 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 Securi
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 th
codelabs - High Assurance Systems
Microkernels - The component-based operating systems