După opt ani de dezvoltare, a fost lansat proiectul Muen 1.0, dezvoltând nucleul Separation, a cărui absență a erorilor în codul sursă a fost confirmată cu ajutorul metodelor matematice de verificare formală a fiabilității. Nucleul este disponibil pentru arhitectura x86_64 și poate fi utilizat în sisteme critice pentru misiune care necesită un nivel sporit de fiabilitate și garanție a lipsei defecțiunilor. Codul sursă al proiectului este scris în limbajul Ada și dialectul său verificabil SPARK 2014. Codul este distribuit sub licență GPLv3.
Nucleul de separare este un microkernel care oferă un mediu pentru execuția componentelor izolate unele de altele, a căror interacțiune este strict reglementată de reguli date. Izolarea se bazează pe utilizarea extensiilor de virtualizare Intel VT-x și include mecanisme de securitate pentru a bloca organizarea canalelor de comunicații ascunse. Nucleul de partiționare este mai minimalist și mai static decât alte microkernel-uri, ceea ce reduce numărul de situații care pot cauza eșec.
Nucleul rulează în modul rădăcină VMX, similar cu un hypervisor, iar toate celelalte componente rulează în modul non-rădăcină VMX, similar sistemelor guest. Accesul la echipament se face folosind extensii Intel VT-d DMA și remaparea întreruperii, ceea ce face posibilă implementarea legăturii securizate a dispozitivelor PCI la componentele care rulează sub Muen.
Capacitățile Muen includ suport pentru sisteme multi-core, pagini de memorie imbricate (EPT, Extended Page Tables), MSI (Message Signaled Interrupts) și tabele de atribute ale paginilor de memorie (PAT, Page Attribute Table). Muen furnizează, de asemenea, un planificator fix round-robin bazat pe temporizatorul preventiv Intel VMX, un timp de rulare compact care nu afectează performanța, un sistem de auditare a erorilor, un mecanism de alocare a resurselor statice bazat pe reguli, un sistem de gestionare a evenimentelor și canale de memorie partajată pentru comunicare în cadrul componentelor care rulează.
Acceptă componente de rulare cu cod de mașină pe 64 de biți, mașini virtuale pe 32 sau 64 de biți, aplicații pe 64 de biți în limbajele Ada și SPARK 2014, mașini virtuale Linux și „unikernel-uri” autonome bazate pe MirageOS pe Muen.
Principalele inovații oferite în lansarea Muen 1.0:
- Au fost publicate documente cu specificații pentru nucleu (dispozitiv și arhitectură), sistem (politici de sistem, Tau0 și set de instrumente) și componente, care documentează toate aspectele proiectului.
- A fost adăugat setul de instrumente Tau0 (Muen System Composer), care include un set de componente verificate gata făcute pentru compunerea imaginilor de sistem și dezvoltarea serviciilor standard care rulează pe Muen. Componentele furnizate includ driverul AHCI (SATA), Device Manager (DM), încărcătorul de pornire, managerul de sistem, terminalul virtual etc.
- Driverul muenblock Linux (o implementare a unui dispozitiv bloc care rulează deasupra memoriei partajate Muen) a fost convertit pentru a utiliza API-ul blockdev 2.0.
- Instrumente implementate pentru gestionarea ciclului de viață al componentelor native.
- Imaginile de sistem au fost convertite pentru a utiliza SBS (Signed Block Stream) și CSL (Command Stream Loader) pentru a proteja integritatea.
- A fost implementat un driver AHCI-DRV verificat, scris în limbajul SPARK 2014 și care vă permite să conectați unități care acceptă interfața ATA sau partiții individuale de disc la componente.
- Suport unikernel îmbunătățit din proiectele MirageOS și Solo5.
- Setul de instrumente pentru limbajul Ada a fost actualizat pentru lansarea GNAT Community 2021.
- Sistemul de integrare continuă a fost transferat de la emulatorul Bochs în mediile imbricate QEMU/KVM.
- Imaginile componente Linux folosesc nucleul Linux 5.4.66.
Sursa: opennet.ru