Efter otte års udvikling blev projektet Muen 1.0 lanceret, som udvikler kernen for adskillelse (Separation kernel), hvis fravær af fejl i kildekoden er bekræftet gennem matematisk formelverifikation af pålidelighed. Kernen er tilgængelig for x86_64-arkitektur og kan anvendes i kritiske systemer, der kræver et højt niveau af pålidelighed og garanti for fravær af nedbrud. Kildekoden til projektet er skrevet i Ada-sproget og dens verifiable dialekt SPARK 2014. Koden distribueres under GPLv3-licensen.
Adskillelseskernen er et mikrokerne, der giver et miljø til udførelse af isolerede komponenter, hvis interaktioner strengt reguleres af fastsatte regler. Isoleringen baseres på anvendelsen af Intel VT-x virtualiseringsudvidelser og omfatter også beskyttelsesmekanismer til at blokere oprettelsen af skjulte kommunikationskanaler. Adskillelseskernen er mere minimalistisk og statisk sammenlignet med andre mikrokerner, hvilket reducerer antallet af situationer, der kan forårsage nedbrud.
Kernen kører i VMX-root mode på lignende måde som en hypervisor, mens alle andre komponenter kører i non-root mode VMX, på samme måde som gæstesystemer. Adgang til hardware sker ved hjælp af Intel VT-d DMA-udvidelser og remapping af afbrydelser, hvilket muliggør sikker binding af PCI-enheder til komponenter, der køres under Muen.
Blandt Muen's muligheder er støtte til flerkernede systemer, indlejrede hukommelsessider (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), hukommelsesside-attributtabeller (PAT, Page Attribute Table). Muen leverer også en fast cyklisk scheduler baseret på Intel VMX’s preemptive timer, et kompakt runtime, der ikke påvirker ydeevnen, et system til overvågning af nedbrud, en mekanisme til statisk tildeling af ressourcer baseret på regler, et system til behandling af begivenheder og kanaler til delt hukommelse til interaktion mellem de kørte komponenter.
Der understøttes kørsel af komponenter på Muen med 64-bit maskinkode, 32- eller 64-bit virtual machines, 64-bit applikationer i Ada- og SPARK 2014-sprog, virtuelle maskiner med Linux og selvstændige "unikernels" baseret på MirageOS.
De vigtigste nyskabelser introduceret i udgivelsen af Muen 1.0:
- Dokumenter med specifikationer for kernen (enhed og arkitektur), systemet (systempolitikker, Tau0 og værktøjer) og komponenterne er offentliggjort, hvori alle aspekter af projektets arbejde er dokumenteret.
- Værktøjssættet Tau0 (Muen System Composer) er tilføjet, som inkluderer et sæt af verificerede komponenter til sammensætning af systembilleder og udvikling af standardtjenester, der kører oven på Muen. Blandt de tilbydte komponenter er AHCI (SATA) driver, Device Manager (DM), bootloader, systemadministrator, virtuel terminal osv.
- Linux-driveren muenblock (implementering af en blok-enhed, der arbejder over delt hukommelse Muen) er blevet omdannet til at bruge API blockdev 2.0.
- Værktøjer til styring af livscyklussen for native komponenter er implementeret.
- Systembilleder er blevet omdannet til at bruge SBS (Signed Block Stream) og CSL (Command Stream Loader) for at beskytte integriteten.
- Den verificerede AHCI-DRV driver, skrevet i SPARK 2014, der muliggør tilslutning af lagermedier, der understøtter ATA-grænsefladen, eller separate diskpartitioner, er blevet implementeret.
- Støtten til unikernels fra projekterne MirageOS og Solo5 er blevet forbedret.
- Værktøjssættet til Ada-sprog er blevet opdateret til udgaven GNAT Community 2021.
- Det kontinuerlige integrationssystem er blevet overført fra Bochs-emulatoren til indlejrede miljøer QEMU/KVM.
- I komponentbillederne med Linux er der anvendt Linux-kernen 5.4.66.
Kilde: opennet.ru
