Després de vuit anys de desenvolupament, es va llançar el projecte Muen 1.0, desenvolupant el nucli Separation, l'absència d'errors en el codi font del qual es va confirmar mitjançant mètodes matemàtics de verificació formal de la fiabilitat. El nucli està disponible per a l'arquitectura x86_64 i es pot utilitzar en sistemes de missió crítica que requereixen un nivell augmentat de fiabilitat i garantia de no fallar. El codi font del projecte està escrit en l'idioma Ada i el seu dialecte verificable SPARK 2014. El codi es distribueix sota la llicència GPLv3.
El nucli de separació és un micronucli que proporciona un entorn per a l'execució de components aïllats entre si, la interacció dels quals està estrictament regulada per regles donades. L'aïllament es basa en l'ús d'extensions de virtualització Intel VT-x i inclou mecanismes de seguretat per bloquejar l'organització de canals de comunicació encoberts. El nucli de particions és més minimalista i estàtic que altres micronuclis, la qual cosa redueix el nombre de situacions que poden causar errors.
El nucli s'executa en mode arrel VMX, similar a un hipervisor, i tots els altres components s'executen en mode no arrel VMX, de manera similar als sistemes convidats. L'accés a l'equip es fa mitjançant les extensions Intel VT-d DMA i la reasignació d'interrupcions, cosa que permet implementar la vinculació segura de dispositius PCI als components que s'executen sota Muen.
Les capacitats de Muen inclouen suport per a sistemes multinúclis, pàgines de memòria imbricades (EPT, taules de pàgines ampliades), MSI (interrupcions amb senyal de missatge) i taules d'atributs de pàgines de memòria (PAT, taula d'atributs de pàgina). Muen també ofereix un programador fix de tot tipus basat en el temporitzador preventiu Intel VMX, un temps d'execució compacte que no afecta el rendiment, un sistema d'auditoria d'errors, un mecanisme d'assignació de recursos estàtics basat en regles, un sistema de gestió d'esdeveniments i canals de memòria compartida per a comunicació dins dels components en execució.
Admet l'execució de components amb codi de màquina de 64 bits, màquines virtuals de 32 o 64 bits, aplicacions de 64 bits en idiomes Ada i SPARK 2014, màquines virtuals Linux i "unikernels" autònoms basats en MirageOS a sobre de Muen.
Les principals innovacions que s'ofereixen en el llançament de Muen 1.0:
- S'han publicat documents amb especificacions per al nucli (dispositiu i arquitectura), sistema (polítiques del sistema, Tau0 i kit d'eines) i components, que documenten tots els aspectes del projecte.
- S'ha afegit el conjunt d'eines Tau0 (Muen System Composer), que inclou un conjunt de components verificats ja preparats per compondre imatges del sistema i desenvolupar serveis estàndard que s'executen a sobre de Muen. Els components proporcionats inclouen el controlador AHCI (SATA), el gestor de dispositius (DM), el carregador d'arrencada, el gestor del sistema, el terminal virtual, etc.
- El controlador muenblock Linux (una implementació d'un dispositiu de bloc que s'executa a la part superior de la memòria compartida de Muen) s'ha convertit per utilitzar l'API blockdev 2.0.
- Eines implementades per gestionar el cicle de vida dels components natius.
- Les imatges del sistema s'han convertit per utilitzar SBS (Signed Block Stream) i CSL (Command Stream Loader) per protegir la integritat.
- S'ha implementat un controlador AHCI-DRV verificat, escrit en el llenguatge SPARK 2014 i que us permet connectar unitats que admeten la interfície ATA o particions de disc individuals als components.
- Suport unikernel millorat dels projectes MirageOS i Solo5.
- El conjunt d'eines del llenguatge Ada s'ha actualitzat per a la versió 2021 de la comunitat GNAT.
- El sistema d'integració contínua s'ha transferit des de l'emulador de Bochs als entorns imbricats QEMU/KVM.
- Les imatges dels components de Linux utilitzen el nucli Linux 5.4.66.
Font: opennet.ru