La publication du noyau de séparation (separation kernel) Muen, développé par une entreprise suisse Codelabs.
Muen prend en charge uniquement les plates-formes Intel x86_64 et garantit que les noyaux et applications qui s'exécutent dans celui-ci ne peuvent pas accéder aux ressources au-delà de leur quota alloué. Cela inclut, entre autres, la mémoire vive, le temps CPU et l'accès aux dispositifs d'entrée-sortie.
Les applications invitées prises en charge comprennent le noyau Linux, les programmes en Ada/SPARK, ainsi que les systèmes d'exploitation basés sur des bibliothèques écrites à l'aide du framework Solo5 (par exemple, MirageOS en OCaml). Pour Linux, des pilotes de noyau sont fournis pour accélérer l'accès au PCI et à d'autres ressources hôtes.
Le noyau Muen est entièrement implémenté en SPARK – un sous-ensemble sécurisé du langage Ada – et a été vérifié pour l'absence d'erreurs d'exécution. Le code est distribué sous la licence GPLv3.
Source : linux.org.ru
