Despois de oito anos de desenvolvemento, lanzouse o proxecto Muen 1.0, desenvolvendo o núcleo Separation, cuxa ausencia de erros no código fonte foi confirmada mediante métodos matemáticos de verificación formal da fiabilidade. O núcleo está dispoñible para a arquitectura x86_64 e pódese usar en sistemas de misión crítica que requiren un maior nivel de fiabilidade e garantía de non producirse fallos. O código fonte do proxecto está escrito na linguaxe Ada e no seu dialecto verificable SPARK 2014. O código distribúese baixo a licenza GPLv3.
O núcleo de separación é un micronúcleo que proporciona un ambiente para a execución de compoñentes illados entre si, cuxa interacción está estrictamente regulada por regras dadas. O illamento baséase no uso de extensións de virtualización Intel VT-x e inclúe mecanismos de seguridade para bloquear a organización de canles de comunicación encubertas. O núcleo de partición é máis minimalista e estático que outros micronúcleos, o que reduce o número de situacións que poden causar fallos.
O kernel execútase en modo raíz VMX, semellante a un hipervisor, e todos os demais compoñentes execútanse en modo VMX non root, de xeito similar aos sistemas convidados. O acceso ao equipo realízase mediante extensións Intel VT-d DMA e reasignación de interrupcións, o que permite implementar a vinculación segura de dispositivos PCI aos compoñentes que se executan baixo Muen.
As capacidades de Muen inclúen soporte para sistemas multinúcleo, páxinas de memoria aniñadas (EPT, táboas de páxinas ampliadas), MSI (interrupcións sinalizadas de mensaxes) e táboas de atributos de páxinas de memoria (PAT, táboa de atributos de páxina). Muen tamén ofrece un programador fixo de round-robin baseado no temporizador preventivo Intel VMX, un tempo de execución compacto que non afecta o rendemento, un sistema de auditoría de fallos, un mecanismo de asignación de recursos estáticos baseado en regras, un sistema de xestión de eventos e canles de memoria compartidas para comunicación dentro dos compoñentes en execución.
Admite compoñentes en execución con código de máquina de 64 bits, máquinas virtuais de 32 ou 64 bits, aplicacións de 64 bits en linguaxes Ada e SPARK 2014, máquinas virtuais Linux e "unikernels" autónomos baseados en MirageOS enriba de Muen.
As principais novidades ofrecidas no lanzamento de Muen 1.0:
- Publicáronse documentos con especificacións para o núcleo (dispositivo e arquitectura), sistema (políticas do sistema, Tau0 e kit de ferramentas) e compoñentes, que documentan todos os aspectos do proxecto.
- Engadiuse o conxunto de ferramentas Tau0 (Muen System Composer), que inclúe un conxunto de compoñentes verificados preparados para compoñer imaxes do sistema e desenvolver servizos estándar que se executan enriba de Muen. Os compoñentes proporcionados inclúen o controlador AHCI (SATA), o xestor de dispositivos (DM), o cargador de arranque, o xestor do sistema, o terminal virtual, etc.
- O controlador de Linux muenblock (unha implementación dun dispositivo de bloque que se executa sobre a memoria compartida de Muen) converteuse para utilizar a API blockdev 2.0.
- Ferramentas implementadas para xestionar o ciclo de vida dos compoñentes nativos.
- As imaxes do sistema convertéronse para usar SBS (Signed Block Stream) e CSL (Command Stream Loader) para protexer a integridade.
- Implementouse un controlador AHCI-DRV verificado, escrito na linguaxe SPARK 2014 e que lle permite conectar aos compoñentes unidades que admitan a interface ATA ou as particións de disco individuais.
- Compatibilidade unikernel mellorada dos proxectos MirageOS e Solo5.
- Actualizouse o conxunto de ferramentas da linguaxe Ada para a versión 2021 da comunidade GNAT.
- O sistema de integración continua foi transferido do emulador de Bochs a ambientes anidados QEMU/KVM.
- As imaxes dos compoñentes de Linux usan o núcleo Linux 5.4.66.
Fonte: opennet.ru