Dopo otto anni di sviluppo, è stata rilasciata la versione 1.0 del progetto Muen, che sviluppa il nucleo di separazione (Separation kernel), la cui assenza di errori nel codice sorgente è confermata da metodi matematici di verifica formale dell'affidabilità. Il nucleo è disponibile per l'architettura x86_64 e può essere utilizzato in sistemi critici che richiedono un alto livello di affidabilità e garanzia di assenza di guasti. I codici sorgente del progetto sono scritti in Ada e nel suo dialetto verificabile SPARK 2014. Il codice è distribuito con licenza GPLv3.
Il nucleo di separazione è un microkernel che fornisce un ambiente per l'esecuzione di componenti isolati fra loro, il cui interazione è rigidamente regolata da regole stabilite. L'isolamento si basa sull'uso di estensioni di virtualizzazione Intel VT-x e include meccanismi di protezione per bloccare la creazione di canali di comunicazione nascosti. Il nucleo di separazione è più minimalista e statico rispetto ad altri microkernel, riducendo così il numero di situazioni che potrebbero portare a guasti.
Il kernel opera in modalità root VMX, simile a un hypervisor, mentre tutti gli altri componenti girano in modalità non-root VMX, come nei sistemi guest. L'accesso all'hardware avviene mediante estensioni Intel VT-d DMA e rimappatura delle interruzioni, permettendo una vinculación sicura delle periferiche PCI ai componenti in esecuzione sotto Muen.
Tra le funzionalità di Muen si trovano il supporto per sistemi multicore, le Extended Page Tables (EPT), gli Interrupts Segnalati da Messaggi (MSI), le Page Attribute Table (PAT). Muen offre anche uno scheduler ciclico fisso basato sul timer a preemption Intel VMX, un runtime compatto che non influisce sulle prestazioni, un sistema di auditing dei crash, un meccanismo di assegnazione statica delle risorse basato su regole, un sistema di gestione degli eventi e canali di memoria condivisa per l'interazione fra i componenti in esecuzione.
È supportato l'avvio di componenti Muen con codice macchina a 64 bit, applicazioni a 32 o 64 bit, di macchine virtualie applicazioni a 64 bit nei linguaggi Ada e SPARK 2014, macchine virtuali con Linux e 'unikernel' autosufficienti basati su MirageOS.
Le principali novità introdotte nella versione Muen 1.0:
- Sono stati pubblicati documenti con le specifiche del kernel (architettura e struttura), del sistema (politiche di sistema, Tau0 e strumenti) e dei componenti, in cui sono documentati tutti gli aspetti del funzionamento del progetto.
- È stato aggiunto lo strumento Tau0 (Muen System Composer), che include un insieme di componenti già verificati per la composizione di immagini di sistema e lo sviluppo di servizi standard, eseguibili sopra Muen. Tra i componenti forniti ci sono il driver AHCI (SATA), Device Manager (DM), bootloader, gestore di sistema, terminale virtuale, ecc.
- Il driver Linux muenblock (implementazione di un dispositivo a blocchi che funziona sopra la memoria condivisa di Muen) è stato aggiornato per utilizzare l'API blockdev 2.0.
- Sono stati realizzati strumenti per gestire il ciclo di vita dei componenti nativi.
- Le immagini di sistema sono state aggiornate 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, che consente di collegare ai componenti dispositivi che supportano l'interfaccia ATA o singole partizioni di disco.
- Supporto migliorato per unikernel dai progetti MirageOS e Solo5.
- Gli strumenti per il linguaggio Ada sono stati aggiornati alla versione GNAT Community 2021.
- Il sistema di integrazione continua è stato trasferito dall'emulatore Bochs a ambienti nidificati QEMU/KVM.
- Le immagini dei componenti Linux utilizzano il kernel Linux 5.4.66.
Fonte: opennet.ru
