Dopu à ottu anni di sviluppu, u prughjettu Muen 1.0 hè statu liberatu, u sviluppu di u kernel Separation, l'absenza d'errori in u codice surghjente di quale hè statu cunfirmatu cù metudi matematichi di verificazione affidabilità formale. U kernel hè dispunibule per l'architettura x86_64 è pò esse usatu in sistemi di missione critica chì necessitanu un livellu aumentatu di affidabilità è guaranzia di nisun fallimentu. U codice fonte di u prugettu hè scrittu in a lingua Ada è u so dialettu verificabile SPARK 2014. U codice hè distribuitu sottu a licenza GPLv3.
U kernel di separazione hè un microkernel chì furnisce un ambiente per l'esekzione di cumpunenti isolati l'una di l'altru, l'interazzione di quale hè strettamente regulata da e regule date. L'isolamentu hè basatu annantu à l'usu di l'estensione di virtualizazione Intel VT-x è include miccanismi di sicurezza per bluccà l'urganizazione di i canali di cumunicazione segreti. U kernel di partizione hè più minimalista è staticu chì l'altri microkernels, chì reduce u nùmeru di situazioni chì ponu causà fallimentu.
U kernel funziona in u modu radicali VMX, simili à un ipervisore, è tutti l'altri cumpunenti funzionanu in modu VMX non-root, simili à i sistemi invitati. L'accessu à l'equipaggiu hè fattu utilizendu estensioni Intel VT-d DMA è interrompe a rimappatura, chì permette di implementà ubligatoriu sicuru di i dispositi PCI à i cumpunenti chì funzionanu sottu Muen.
E capacità di Muen includenu supportu per sistemi multi-core, pagine di memoria nidificate (EPT, Extended Page Tables), MSI (Message Signaled Interrupts) è tabelle di attributi di pagina di memoria (PAT, Page Attribute Table). Muen furnisce ancu un pianificatore round-robin fissu basatu annantu à u timer preventivu Intel VMX, un runtime compactu chì ùn hà micca impattu nantu à u rendiment, un sistema di verificazione di crash, un mecanismu di assignazione di risorse statiche basatu in regule, un sistema di gestione di l'eventi, è canali di memoria spartuti per cumunicazione in i cumpunenti in esecuzione.
Supporta i cumpunenti in esecuzione cù codice macchina 64-bit, macchine virtuali 32 o 64-bit, applicazioni 64-bit in lingue Ada è SPARK 2014, macchine virtuali Linux è "unikernels" autonomi basati in MirageOS sopra Muen.
L'innuvazioni principali offerte in a liberazione di Muen 1.0:
- I ducumenti sò stati publicati cù specificazioni per u kernel (dispositivu è architettura), sistema (pulitiche di sistema, Tau0 è toolkit) è cumpunenti, chì documentanu tutti l'aspettu di u prugettu.
- U toolkit Tau0 (Muen System Composer) hè statu aghjuntu, chì include un inseme di cumpunenti verificati pronti per a cumpusizioni di l'imaghjini di u sistema è u sviluppu di servizii standard chì funzionanu nantu à Muen. I cumpunenti furnuti include u driver AHCI (SATA), Device Manager (DM), boot loader, system manager, terminal virtuale, etc.
- U muenblock muenblock Linux driver (una implementazione di un dispositivu di bloccu chì corre nantu à a memoria sparta Muen) hè stata cunvertita per utilizà l'API blockdev 2.0.
- Strumenti implementati per a gestione di u ciclu di vita di i cumpunenti nativi.
- L'imaghjini di u sistema sò stati cunvertiti per utilizà SBS (Signed Block Stream) è CSL (Command Stream Loader) per prutege l'integrità.
- Un cunduttore AHCI-DRV verificatu hè statu implementatu, scrittu in a lingua SPARK 2014 è chì vi permette di cunnette unità chì supportanu l'interfaccia ATA o partizioni di discu individuali à i cumpunenti.
- Supportu unikernel migliuratu da i prughjetti MirageOS è Solo5.
- U toolkit di lingua Ada hè statu aghjurnatu per a versione GNAT Community 2021.
- U sistema di integrazione cuntinuu hè statu trasferitu da l'emulatore Bochs à l'ambienti annidati QEMU / KVM.
- L'imaghjini di cumpunenti Linux utilizanu u kernel Linux 5.4.66.
Source: opennet.ru