Se lanzó el núcleo de separación (separation kernel) Muen, desarrollado por una empresa suiza — una colección de tutoriales sobre diversos aspectos del trabajo con productos de Google. Los caminos (Pathways) del punto anterior son colecciones organizadas de laboratorios de aquí..
Muen solo es compatible con plataformas Intel x86_64 y garantiza que los núcleos del sistema operativo y las aplicaciones que se ejecutan en él no pueden acceder a recursos más allá de su cuota asignada. Esto incluye, entre otros, la memoria RAM, el tiempo de CPU y el acceso a dispositivos de entrada/salida.
Se admiten como aplicaciones invitadas el núcleo de Linux, programas en Ada/SPARK, así como sistemas operativos de biblioteca escritos utilizando el marco Solo5 (por ejemplo, MirageOS en OCaml). Para Linux, se proporcionan controladores de núcleo para acelerar el acceso a PCI y otros recursos del host.
Muen está completamente implementado en SPARK, un subconjunto seguro del lenguaje Ada, y ha sido verificado para la ausencia de errores de tiempo de ejecución. El código se distribuye bajo la licencia GPLv3.
Fuente: linux.org.ru
