Die Veröffentlichung des Trennkerns (separation kernel) Muen, entwickelt von der Schweizer Firma Codelabs.
Muen unterstützt nur Intel x86_64-Plattformen und gewährleistet, dass die darin ausgeführten Betriebssystemkerne und Anwendungen nicht auf Ressourcen zugreifen können, die über das ihnen zugewiesene Kontingent hinausgehen. Dies betrifft insbesondere den Arbeitsspeicher, die CPU-Zeit und den Zugang zu Ein- und Ausgabegeräten.
Unterstützte Gastanwendungen sind der Linux-Kernel, Programme in Ada/SPARK sowie Library-Betriebssysteme, die mit dem Solo5-Framework geschrieben wurden (zum Beispiel MirageOS in OCaml). Für Linux werden Kernel-Treiber bereitgestellt, um den Zugang zu PCI und anderen Host-Ressourcen zu beschleunigen.
Muen selbst ist vollständig in SPARK – einem sicheren Teilbereich der Ada-Sprache – implementiert und wurde auf das Fehlen von Laufzeitfehlern verifiziert. Der Code wird unter der GPLv3-Lizenz veröffentlicht.
Quelle: linux.org.ru
