È stato rilasciato il kernel di separazione (kernel di separazione) Muen, sviluppato dall'azienda svizzera Codelabs.
Muen supporta solo piattaforme Intel x86_64 e garantisce che i kernel di sistema operativo e le applicazioni in esecuzione non possano accedere alle risorse oltre la quota loro assegnata. Questo include, tra l'altro, la memoria RAM, il tempo di CPU e l'accesso ai dispositivi di input/output.
Come applicazioni guest sono supportati il kernel Linux, i programmi in Ada/SPARK, così come i sistemi operativi di libreria scritti utilizzando il framework Solo5 (ad esempio, MirageOS su OCaml). Per Linux sono forniti i driver del kernel per velocizzare l'accesso alle risorse PCI e ad altre risorse dell'host.
Il Muen è interamente 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
