După opt ani de dezvoltare, a fost lansat proiectul Muen 1.0, care dezvoltă nucleul de separare (Separation kernel), al cărui cod sursă este lipsit de erori, confirmat prin metode matematice de verificare formală a fiabilității. Nucleul este disponibil pentru arhitectura x86_64 și poate fi utilizat în sisteme critice, care necesită un nivel ridicat de fiabilitate și garanția absenței defecțiunilor. Codul sursă al proiectului este scris în Ada și dialectul său verificabil SPARK 2014. Codul este distribuit sub licența GPLv3.
Nucleul de separare reprezintă un microkernel care oferă un mediu pentru executarea componentelor izolate una de cealaltă, interacțiunea dintre acestea fiind strict reglementată de reguli stabilite. Izolarea se bazează pe utilizarea extensiilor de virtualizare Intel VT-x și prevede, printre altele, mecanisme de protecție pentru a bloca organizarea canalelor de comunicare ascunse. Nucleul de separare este mai minimalist și static comparativ cu alte microkerneluri, ceea ce permite reducerea numărului de situații care ar putea duce la defecțiuni.
Nucleul rulează în modul VMX root, similar cu un hypervisor, iar toate celelalte componente rulează în modul VMX non-root, similar sistemelor gazdă. Accesul la hardware se face prin utilizarea extensiilor Intel VT-d DMA și re-maparea întreruperilor, ceea ce permite realizarea unei legături sigure a dispozitivelor PCI la componentele care rulează sub Muen.
Printre capacitățile Muen se numără suportul pentru sisteme multi-core, pagini de memorie înnegrite (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), tabele de atribute ale paginilor de memorie (PAT, Page Attribute Table). Muen oferă de asemenea un scheduler ciclic fix bazat pe un timer preemptiv Intel VMX, un runtime compact care nu influențează performanța, un sistem de audit al defecțiunilor, un mecanism de alocare statică a resurselor pe baza regulilor, un sistem de procesare a evenimentelor și canale de memorie partajată pentru interacțiune între componentele care rulează.
Este susținută rularea componentelor Muen cu cod mașină pe 64 de biți, 32 sau 64 de biți, mașini virtualeaplicații pe 64 de biți în limbajele Ada și SPARK 2014, mașini virtuale cu Linux și unicore self-sufficient pe bază de MirageOS.
Principalele noutăți propuse în lansarea Muen 1.0:
- Au fost publicate documentele cu specificațiile nucleului (structură și arhitectură), sistemului (politici sistemice, Tau0 și instrumentarul) și componentelor, în care sunt documentate toate aspectele funcționării proiectului.
- A fost adăugat instrumentarul Tau0 (Muen System Composer), care include un set de componente verificate gata de utilizare pentru compunerea imaginilor sistemului și dezvoltarea serviciilor standard, care sunt lansate peste Muen. Printre componentele furnizate se numără driverul AHCI (SATA), Device Manager (DM), bootloader, sistemul de gestionare, terminalul virtual și altele.
- Driverul Linux muenblock (implementarea unui dispozitiv de bloc, care funcționează pe baza memoriei partajate Muen) a fost actualizat pentru a utiliza API-ul blockdev 2.0.
- Au fost implementate instrumente pentru gestionarea ciclului de viață al componentelor native.
- Imaginile sistemului au fost actualizate 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, care permite conectarea unităților care suportă interfața ATA sau a partițiilor de disc separate.
- A fost îmbunătățită suportul pentru unikernel din proiectele MirageOS și Solo5.
- Instrumentarul pentru limbajul Ada a fost actualizat la versiunea GNAT Community 2021.
- Sistemul de integrare continuă a fost transferat de la emulatorul Bochs la medii înfășurate QEMU/KVM.
- În imaginile componentelor cu Linux a fost utilizat nucleul Linux 5.4.66.
Sursa: opennet.ro
