Dopo otto anni di sviluppo, è stato rilasciato il progetto Muen 1.0, che sviluppa un nucleo di separazione (Separation kernel), la cui assenza di errori nei testi sorgente è stata confermata attraverso 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 testi sorgente del progetto sono scritti in Ada e nel suo dialetto verificabile SPARK 2014. Il codice è distribuito sotto licenza GPLv3.
Il nucleo di separazione è un microkernel che fornisce un ambiente per l'esecuzione di componenti isolati l'uno dall'altro, il cui interazione è rigidamente regolata da regole definite. L'isolamento si basa sull'uso delle estensioni di virtualizzazione Intel VT-x e prevede anche meccanismi di protezione per bloccare l'organizzazione di canali di comunicazione nascosti. Il nucleo di separazione è più minimalista e statico rispetto ad altri microkernel, il che consente di ridurre il numero di situazioni che possono portare a un guasto.
Il nucleo viene eseguito in modalità root VMX, analogamente a un hypervisor, mentre tutti gli altri componenti operano in modalità non root VMX, in modo simile ai sistemi guest. L'accesso all'hardware avviene utilizzando le estensioni Intel VT-d DMA e il rimappamento delle interruzioni, il che consente di realizzare un collegamento sicuro dei dispositivi PCI ai componenti in esecuzione sotto Muen.
Tra le funzionalità di Muen si segnala il supporto per sistemi multicore, pagine di memoria nidificate (EPT, Extended Page Tables), MSI (Message Signaled Interrupts) e tabelle degli attributi delle pagine di memoria (PAT, Page Attribute Table). Muen fornisce anche uno scheduler ciclico fisso basato su un timer di preemption Intel VMX, un runtime compatto che non influisce sulle prestazioni, un sistema di audit 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 tra i componenti in esecuzione.
È supportato l'avvio di componenti Muen con codice macchina a 64 bit, a 32 o 64 bit macchine virtuali, applicazioni a 64 bit in linguaggi Ada e SPARK 2014, macchine virtuali con Linux e «unikernel» autosufficienti basati su MirageOS.
Le principali novità proposte nella versione Muen 1.0:
- Sono stati pubblicati i documenti con le specifiche del kernel (dispositivo e architettura), del sistema (politiche di sistema, Tau0 e strumenti) e dei componenti, nei quali sono documentati tutti gli aspetti del lavoro del progetto.
- È stato aggiunto l'insieme di strumenti Tau0 (Muen System Composer), che include un insieme di componenti verificati pronti all'uso per assemblare immagini di sistema e sviluppare servizi standard, eseguiti sopra Muen. Tra i componenti forniti ci sono il driver AHCI (SATA), il Device Manager (DM), il bootloader, il system manager, il terminale virtuale, ecc.
- Il driver Linux muenblock (implementazione di un dispositivo block che funziona sopra la memoria condivisa Muen) è stato convertito per utilizzare l'API blockdev 2.0.
- Sono stati implementati strumenti 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 realizzato un driver AHCI-DRV verificato, scritto in SPARK 2014, che consente di collegare ai componenti unità che supportano l'interfaccia ATA o singole partizioni di disco.
- È stato migliorato il supporto per unikernel dai progetti MirageOS e Solo5.
- L'insieme di strumenti per il linguaggio Ada è stato aggiornato alla versione GNAT Community 2021.
- Il sistema di integrazione continua è stato spostato dall'emulatore Bochs a ambienti nidificati QEMU/KVM.
- Nelle immagini dei componenti con Linux è stato utilizzato il kernel Linux 5.4.66.
Fonte: opennet.ru
