Etter åtte års utvikling ble Muen 1.0-prosjektet utgitt, og utviklet Separation-kjernen, hvis fravær av feil i kildekoden ble bekreftet ved hjelp av matematiske metoder for formell pålitelighetsverifisering. Kjernen er tilgjengelig for x86_64-arkitekturen og kan brukes i oppdragskritiske systemer som krever et økt nivå av pålitelighet og garanti for ingen feil. Kildekoden til prosjektet er skrevet på Ada-språket og dets verifiserbare dialekt SPARK 2014. Koden distribueres under GPLv3-lisensen.
Separasjonskjernen er en mikrokjerne som gir et miljø for utførelse av komponenter isolert fra hverandre, hvis interaksjon er strengt regulert av gitte regler. Isolering er basert på bruk av Intel VT-x virtualiseringsutvidelser og inkluderer sikkerhetsmekanismer for å blokkere organiseringen av skjulte kommunikasjonskanaler. Partisjoneringskjernen er mer minimalistisk og statisk enn andre mikrokjerner, noe som reduserer antall situasjoner som kan forårsake feil.
Kjernen kjører i VMX-rotmodus, på samme måte som en hypervisor, og alle andre komponenter kjører i VMX ikke-rotmodus, på samme måte som gjestesystemer. Tilgang til utstyret gjøres ved hjelp av Intel VT-d DMA-utvidelser og interrupt remapping, som gjør det mulig å implementere sikker binding av PCI-enheter til komponenter som kjører under Muen.
Muens muligheter inkluderer støtte for flerkjernesystemer, nestede minnesider (EPT, Extended Page Tables), MSI (Message Signaled Interrupts) og minnesideattributttabeller (PAT, Page Attribute Table). Muen tilbyr også en fast round-robin-planlegger basert på Intel VMX preemptive timer, en kompakt kjøretid som ikke påvirker ytelsen, et krasjrevisjonssystem, en regelbasert statisk ressurstilordningsmekanisme, et hendelseshåndteringssystem og delte minnekanaler for kommunikasjon innenfor kjørende komponenter.
Den støtter kjørende komponenter med 64-bits maskinkode, 32- eller 64-biters virtuelle maskiner, 64-bits applikasjoner i Ada og SPARK 2014-språk, virtuelle Linux-maskiner og selvstendige "unikernels" basert på MirageOS på toppen av Muen.
De viktigste nyvinningene som tilbys i utgivelsen av Muen 1.0:
- Det er publisert dokumenter med spesifikasjoner for kjernen (enhet og arkitektur), system (systempolicyer, Tau0 og verktøysett) og komponenter, som dokumenterer alle aspekter av prosjektet.
- Verktøysettet Tau0 (Muen System Composer) er lagt til, som inkluderer et sett med ferdige verifiserte komponenter for å komponere systembilder og utvikle standardtjenester som kjører på toppen av Muen. Komponentene som leveres inkluderer AHCI-driver (SATA), Device Manager (DM), oppstartslaster, systembehandling, virtuell terminal, etc.
- Muenblock Linux-driveren (en implementering av en blokkenhet som kjører på toppen av Muen delte minne) har blitt konvertert til å bruke blockdev 2.0 API.
- Implementerte verktøy for å administrere livssyklusen til native komponenter.
- Systembilder er konvertert til å bruke SBS (Signed Block Stream) og CSL (Command Stream Loader) for å beskytte integriteten.
- En verifisert AHCI-DRV-driver er implementert, skrevet på SPARK 2014-språket og lar deg koble til stasjoner som støtter ATA-grensesnittet eller individuelle diskpartisjoner til komponentene.
- Forbedret unikernel-støtte fra MirageOS- og Solo5-prosjekter.
- Ada-språkverktøysettet er oppdatert for GNAT Community 2021-utgivelsen.
- Det kontinuerlige integrasjonssystemet er overført fra Bochs-emulatoren til QEMU/KVM nestede miljøer.
- Linux-komponentbilder bruker Linux 5.4.66-kjernen.
Kilde: opennet.ru