Foi lançado o núcleo de separação (separation kernel) Muen, desenvolvido pela empresa suíça Codelabs.
O Muen suporta apenas plataformas Intel x86_64 e garante que os núcleos do sistema operacional e os aplicativos executados nele não podem acessar recursos além da cota alocada para eles. Isso inclui, entre outros, memória RAM, tempo de CPU e acesso a dispositivos de entrada/saída.
Como aplicativos convidados, são suportados o núcleo Linux, programas em Ada/SPARK, bem como sistemas operacionais de biblioteca escritos usando o framework Solo5 (por exemplo, MirageOS em OCaml). Para o Linux, drivers de kernel são fornecidos para acelerar o acesso ao PCI e a outros recursos do host.
O próprio Muen é totalmente implementado em SPARK – um subconjunto seguro da linguagem Ada – e passou por verificação para garantir a ausência de erros em tempo de execução. O código é distribuído sob a licença GPLv3.
Fonte: linux.org.ru
