Dopo otto anni di sviluppo, è stato rilasciato il progetto Muen 1.0, sviluppando il kernel Separation, la cui assenza di errori nel codice sorgente è stata confermata utilizzando metodi matematici di verifica formale dell'affidabilità. Il kernel è disponibile per l'architettura x86_64 e può essere utilizzato in sistemi mission-critical che richiedono un maggiore livello di affidabilità e garanzia di assenza di guasti. Il codice sorgente del progetto è scritto nel linguaggio Ada e nel suo dialetto verificabile SPARK 2014. Il codice è distribuito sotto la licenza GPLv3.
Il kernel di separazione è un microkernel che fornisce un ambiente per l'esecuzione di componenti isolati tra loro, la cui interazione è strettamente regolata da determinate regole. L'isolamento si basa sull'uso delle estensioni di virtualizzazione Intel VT-x e include meccanismi di sicurezza per bloccare l'organizzazione dei canali di comunicazione nascosti. Il kernel di partizionamento è più minimalista e statico rispetto ad altri microkernel, il che riduce il numero di situazioni che possono causare errori.
Il kernel viene eseguito in modalità root VMX, simile a un hypervisor, e tutti gli altri componenti vengono eseguiti in modalità non root VMX, simile ai sistemi guest. L'accesso all'apparecchiatura viene effettuato utilizzando le estensioni Intel VT-d DMA e la rimappatura degli interrupt, che consente di implementare l'associazione sicura dei dispositivi PCI ai componenti in esecuzione su Muen.
Le funzionalità di Muen includono il supporto per sistemi multi-core, pagine di memoria nidificate (EPT, Extended Page Tables), MSI (Message Signaled Interrupts) e tabelle di attributi delle pagine di memoria (PAT, Page Attribute Table). Muen fornisce inoltre uno scheduler round-robin fisso basato sul timer preventivo Intel VMX, un runtime compatto che non influisce sulle prestazioni, un sistema di controllo degli arresti anomali, un meccanismo di assegnazione statica delle risorse basato su regole, un sistema di gestione degli eventi e canali di memoria condivisi per comunicazione all'interno dei componenti in esecuzione.
Supporta componenti in esecuzione con codice macchina a 64 bit, macchine virtuali a 32 o 64 bit, applicazioni a 64 bit nei linguaggi Ada e SPARK 2014, macchine virtuali Linux e "unikernel" autonomi basati su MirageOS su Muen.
Le principali novità offerte nel rilascio di Muen 1.0:
- Sono stati pubblicati documenti con specifiche per il kernel (dispositivo e architettura), sistema (politiche di sistema, Tau0 e toolkit) e componenti, che documentano tutti gli aspetti del progetto.
- È stato aggiunto il toolkit Tau0 (Muen System Composer), che include una serie di componenti verificati già pronti per la composizione di immagini di sistema e lo sviluppo di servizi standard eseguiti su Muen. I componenti forniti includono driver AHCI (SATA), Device Manager (DM), boot loader, gestore di sistema, terminale virtuale, ecc.
- Il driver Linux muenblock (un'implementazione di un dispositivo a blocchi in esecuzione sulla memoria condivisa Muen) è stato convertito per utilizzare l'API blockdev 2.0.
- Strumenti implementati per la gestione del ciclo di vita dei componenti nativi.
- Le immagini di sistema sono state convertite per utilizzare SBS (Signed Block Stream) e CSL (Command Stream Loader) per proteggere l'integrità.
- È stato implementato un driver AHCI-DRV verificato, scritto nel linguaggio SPARK 2014 e che consente di connettere unità che supportano l'interfaccia ATA o singole partizioni del disco ai componenti.
- Supporto unikernel migliorato dai progetti MirageOS e Solo5.
- Il toolkit del linguaggio Ada è stato aggiornato per la versione GNAT Community 2021.
- Il sistema di integrazione continua è stato trasferito dall'emulatore Bochs agli ambienti nidificati QEMU/KVM.
- Le immagini dei componenti Linux utilizzano il kernel Linux 5.4.66.
Fonte: opennet.ru