È stata rilasciata la kernel di separazione (separation kernel) Muen, sviluppata dalla società svizzera Codelabs.
Muen supporta solo piattaforme Intel x86_64 e garantisce che i kernel del sistema operativo e le applicazioni eseguite al suo interno non possano accedere alle risorse oltre la quota a loro assegnata. Ciò include, tra l'altro, la memoria RAM, il tempo CPU e l'accesso ai dispositivi di input/output.
Come applicazioni guest, sono supportati il kernel Linux, i programmi in Ada/SPARK e i sistemi operativi di libreria scritti utilizzando il framework Solo5 (ad esempio, MirageOS su OCaml). Per Linux sono forniti driver del kernel per migliorare l'accesso a PCI e ad altre risorse dell'host.
Lo stesso Muen è completamente implementato in SPARK, un sottoinsieme sicuro del linguaggio Ada, ed è stato verificato per l'assenza di errori di runtime. Il codice è distribuito sotto licenza GPLv3.
Fonte: linux.org.ru
