Após oito anos de desenvolvimento, foi lançado o projeto Muen 1.0, desenvolvendo o kernel Separation, cuja ausência de erros no código-fonte foi confirmada por métodos matemáticos de verificação formal de confiabilidade. O kernel está disponível para a arquitetura x86_64 e pode ser utilizado em sistemas de missão crítica que exigem maior nível de confiabilidade e garantia de ausência de falhas. O código-fonte do projeto é escrito na linguagem Ada e seu dialeto verificável SPARK 2014. O código é distribuído sob a licença GPLv3.
O kernel de separação é um microkernel que fornece um ambiente para a execução de componentes isolados uns dos outros, cuja interação é estritamente regulada por determinadas regras. O isolamento é baseado no uso de extensões de virtualização Intel VT-x e inclui mecanismos de segurança para bloquear a organização de canais de comunicação secretos. O kernel de particionamento é mais minimalista e estático do que outros microkernels, o que reduz o número de situações que podem causar falhas.
O kernel é executado no modo raiz VMX, semelhante a um hipervisor, e todos os outros componentes são executados no modo não raiz VMX, semelhante aos sistemas convidados. O acesso ao equipamento é feito através de extensões Intel VT-d DMA e remapeamento de interrupções, o que permite implementar vinculação segura de dispositivos PCI a componentes rodando em Muen.
Os recursos do Muen incluem suporte para sistemas multi-core, páginas de memória aninhadas (EPT, Extended Page Tables), MSI (Message Signaled Interrupts) e tabelas de atributos de páginas de memória (PAT, Page Attribute Table). Muen também fornece um agendador round-robin fixo baseado no temporizador preemptivo Intel VMX, um tempo de execução compacto que não afeta o desempenho, um sistema de auditoria de falhas, um mecanismo de atribuição de recursos estáticos baseado em regras, um sistema de manipulação de eventos e canais de memória compartilhada para comunicação dentro dos componentes em execução.
Ele suporta a execução de componentes com código de máquina de 64 bits, máquinas virtuais de 32 ou 64 bits, aplicativos de 64 bits nas linguagens Ada e SPARK 2014, máquinas virtuais Linux e “unikernels” independentes baseados em MirageOS em cima de Muen.
As principais inovações oferecidas no lançamento do Muen 1.0:
- Foram publicados documentos com especificações de kernel (dispositivo e arquitetura), sistema (políticas de sistema, Tau0 e kit de ferramentas) e componentes, que documentam todos os aspectos do projeto.
- O kit de ferramentas Tau0 (Muen System Composer) foi adicionado, que inclui um conjunto de componentes verificados prontos para compor imagens do sistema e desenvolver serviços padrão que são executados no Muen. Os componentes fornecidos incluem driver AHCI (SATA), Gerenciador de dispositivos (DM), carregador de inicialização, gerenciador de sistema, terminal virtual, etc.
- O driver muenblock Linux (uma implementação de um dispositivo de bloco rodando sobre a memória compartilhada do Muen) foi convertido para usar a API blockdev 2.0.
- Implementei ferramentas para gerenciamento do ciclo de vida de componentes nativos.
- As imagens do sistema foram convertidas para usar SBS (Signed Block Stream) e CSL (Command Stream Loader) para proteger a integridade.
- Um driver AHCI-DRV verificado foi implementado, escrito na linguagem SPARK 2014 e permitindo conectar unidades que suportam a interface ATA ou partições de disco individuais aos componentes.
- Suporte melhorado ao unikernel dos projetos MirageOS e Solo5.
- O kit de ferramentas da linguagem Ada foi atualizado para o lançamento da Comunidade GNAT 2021.
- O sistema de integração contínua foi transferido do emulador Bochs para ambientes aninhados QEMU/KVM.
- As imagens de componentes do Linux usam o kernel Linux 5.4.66.
Fonte: opennet.ru