Sandro Magi
2013-12-11 07:15:51 UTC
Probably of interest to some on this list:
http://muen.codelabs.ch/
The Muen Separation Kernel is the worldâs first Open Source
microkernel that has been formally proven to contain no runtime
errors at the source code level. It is developed in Switzerland by
the Institute for Internet Technologies and Applications (ITA) at
the University of Applied Sciences Rapperswil (HSR). 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, HSR closely cooperates with the high-security
specialist secunet Security Networks AG in Germany.
A Separation Kernel (SK) 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.
http://muen.codelabs.ch/
The Muen Separation Kernel is the worldâs first Open Source
microkernel that has been formally proven to contain no runtime
errors at the source code level. It is developed in Switzerland by
the Institute for Internet Technologies and Applications (ITA) at
the University of Applied Sciences Rapperswil (HSR). 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, HSR closely cooperates with the high-security
specialist secunet Security Networks AG in Germany.
A Separation Kernel (SK) 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.