The release of the separation kernel (separation kernel) Muen, developed by a Swiss company Codelabs.
Muen supports only Intel x86_64 platforms and ensures that the operating system kernels and applications running in it cannot access resources beyond the quota allocated to them. This includes RAM, CPU time, and access to I/O devices.
Guest applications supported include the Linux kernel, programs written in Ada/SPARK, as well as library operating systems developed using the Solo5 framework (e.g., MirageOS in OCaml). For Linux, kernel drivers are provided to enhance access to PCI and other host resources.
Muen itself is fully implemented in SPARK—the safe subset of the Ada language—and has been verified for the absence of runtime errors. The code is distributed under the GPLv3 license.
Source: linux.org.ru
