Após oito anos de desenvolvimento, foi lançado o projeto Muen 1.0, que desenvolve o núcleo de separação (Separation kernel), cuja ausência de erros no código fonte foi confirmada por métodos matemáticos de verificação formal de confiabilidade. O núcleo está disponível para a arquitetura x86_64 e pode ser utilizado em sistemas críticos que requerem um nível elevado de confiabilidade e garantia de ausência de falhas. Os códigos-fonte do projeto são escritos na linguagem Ada e seu dialeto verificável SPARK 2014. O código é distribuído sob a licença GPLv3.
O núcleo de separação é um microkernel que fornece um ambiente para a execução de componentes isolados entre si, cuja interação é rigidamente regulada por regras definidas. A isolamento é baseado na aplicação de extensões de virtualização Intel VT-x e prevê, entre outras coisas, mecanismos de proteção para bloquear a organização de canais de comunicação ocultos. O núcleo de separação é mais minimalista e estático em comparação com outros microkernels, o que permite reduzir o número de situações que podem levar a falhas.
O núcleo opera em modo raiz VMX, semelhante ao hipervisor, enquanto todos os outros componentes funcionam em modo não raiz VMX, semelhante aos sistemas convidados. O acesso ao hardware é feito utilizando as extensões Intel VT-d DMA e o remapeamento de interrupções, o que possibilita implementar a conexão segura de dispositivos PCI aos componentes que são executados sob o controle do Muen.
Entre as capacidades do Muen, destacam-se o suporte a sistemas multicore, páginas de memória aninhadas (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), tabelas de atributos de páginas de memória (PAT, Page Attribute Table). O Muen também oferece um agendador cíclico fixo baseado em um temporizador preemptivo Intel VMX, um runtime compacto que não impacta a performance, um sistema de auditoria de falhas, um mecanismo de alocação estática de recursos baseado em regras, um sistema de processamento de eventos e canais de memória compartilhada para comunicação entre os componentes executados.
É suportada a execução de componentes com código de máquina de 64 bits, de 32 ou 64 bits máquinas virtuais, de aplicativos de 64 bits nas linguagens Ada e SPARK 2014, máquinas virtuais com Linux e "unikernels" autossuficientes baseados no MirageOS.
As principais inovações propostas na versão Muen 1.0:
- Foram publicados documentos com as especificações do núcleo (estrutura e arquitetura), do sistema (políticas do sistema, Tau0 e ferramentas) e dos componentes, que documentam todos os aspectos do funcionamento do projeto.
- Foi adicionada a ferramenta Tau0 (Muen System Composer), que inclui um conjunto de componentes verificados prontos para a montagem de imagens de sistema e desenvolvimento de serviços padrão que são executados sobre o Muen. Entre os componentes fornecidos estão o driver AHCI (SATA), Gerenciador de Dispositivos (DM), carregador, gerenciador do sistema, terminal virtual, etc.
- O driver Linux muenblock (implementação de um dispositivo de bloco funcionando sobre memória compartilhada do Muen) foi atualizado para usar a API blockdev 2.0.
- Foram implementadas ferramentas para gerenciar o ciclo de vida de componentes nativos.
- As imagens do sistema foram alteradas para usar SBS (Signed Block Stream) e CSL (Command Stream Loader) para proteger a integridade.
- Foi implementado um driver verificado AHCI-DRV, escrito na linguagem SPARK 2014, que permite conectar dispositivos que suportam a interface ATA ou partições de disco individuais a componentes.
- Melhorado o suporte para unikernel dos projetos MirageOS e Solo5.
- A ferramenta para a linguagem Ada foi atualizada para a versão GNAT Community 2021.
- O sistema de integração contínua foi transferido do emulador Bochs para ambientes embutidos QEMU/KVM.
- Nas imagens dos componentes com Linux, foi utilizado o núcleo Linux 5.4.66.
Fonte: opennet.ru
