Po aštuonerių metų kūrimo buvo išleistas projektas Muen 1.0, kuriame buvo sukurtas atskyrimo branduolys, kurio šaltinio kode klaidų nebuvimas buvo patvirtintas naudojant matematinius formalaus patikimumo patikrinimo metodus. Branduolys yra prieinamas x86_64 architektūrai ir gali būti naudojamas itin svarbiose sistemose, kurioms reikalingas didesnis patikimumas ir garantija, kad nebus jokių gedimų. Projekto šaltinio kodas parašytas Ada kalba ir jos patikrinama tarme SPARK 2014. Kodas platinamas pagal GPLv3 licenciją.
Atskyrimo branduolys yra mikrobranduolys, suteikiantis aplinką vienas nuo kito izoliuotų komponentų vykdymui, kurių sąveiką griežtai reglamentuoja pateiktos taisyklės. Izoliavimas pagrįstas „Intel VT-x“ virtualizacijos plėtinių naudojimu ir apima saugos mechanizmus, blokuojančius slaptų ryšio kanalų organizavimą. Skirstymo branduolys yra minimalistiškesnis ir statiškesnis nei kiti mikrobranduoliai, o tai sumažina situacijų, kurios gali sukelti gedimą, skaičių.
Branduolys veikia VMX šakniniu režimu, panašiai kaip hipervizorius, o visi kiti komponentai veikia VMX ne šakniniu režimu, panašiai kaip svečių sistemos. Prieiga prie įrangos pasiekiama naudojant „Intel VT-d DMA“ plėtinius ir pertraukų pertvarkymą, leidžiantį saugiai susieti PCI įrenginius su „Muen“ veikiančiais komponentais.
„Muen“ galimybės apima kelių branduolių sistemų palaikymą, įdėtos atminties puslapius (EPT, išplėstines puslapių lenteles), MSI (signalizuotas pertraukas) ir atminties puslapio atributų lenteles (PAT, puslapio atributų lentelę). „Muen“ taip pat teikia fiksuotą apvalų planavimo priemonę, pagrįstą „Intel VMX“ prevenciniu laikmačiu, kompaktišką vykdymo laiką, kuris neturi įtakos našumui, gedimų audito sistemą, taisyklėmis pagrįstą statinių išteklių priskyrimo mechanizmą, įvykių tvarkymo sistemą ir bendrinamus atminties kanalus. komunikacija veikiančiuose komponentuose.
Jis palaiko veikiančius komponentus su 64 bitų mašinos kodu, 32 arba 64 bitų virtualias mašinas, 64 bitų programas Ada ir SPARK 2014 kalbomis, Linux virtualias mašinas ir savarankiškus "unikernels", pagrįstus Mirage OS ant Muen.
Pagrindinės naujovės, siūlomos išleidžiant Muen 1.0:
- Buvo paskelbti dokumentai su branduolio (įrenginio ir architektūros), sistemos (sistemos politikos, Tau0 ir įrankių rinkinio) ir komponentų specifikacijomis, kuriuose dokumentuojami visi projekto aspektai.
- Pridėtas „Tau0“ („Muen System Composer“) įrankių rinkinys, į kurį įeina paruoštų patikrintų komponentų rinkinys, skirtas sistemos vaizdams kurti ir standartinėms paslaugoms, veikiančioms „Muen“ viršuje, kurti. Pateikiami komponentai: AHCI (SATA) tvarkyklė, įrenginių tvarkytuvė (DM), įkrovos įkroviklis, sistemos tvarkyklė, virtualus terminalas ir kt.
- „muenblock Linux“ tvarkyklė (blokavimo įrenginio, veikiančio „Muen“ bendrinamos atminties viršuje, įgyvendinimas) buvo konvertuotas naudoti „blockdev 2.0“ API.
- Įdiegti įrankiai, skirti valdyti savųjų komponentų gyvavimo ciklą.
- Sistemos vaizdai buvo konvertuoti į SBS (Signed Block Stream) ir CSL (Command Stream Loader), kad būtų apsaugotas vientisumas.
- Įdiegta patvirtinta AHCI-DRV tvarkyklė, parašyta SPARK 2014 kalba ir leidžianti prie komponentų prijungti diskus, palaikančius ATA sąsają arba atskirus disko skaidinius.
- Patobulintas „MirageOS“ ir „Solo5“ projektų „unikernel“ palaikymas.
- „Ada“ kalbos įrankių rinkinys buvo atnaujintas „GNAT Community 2021“ leidimui.
- Nepertraukiamo integravimo sistema buvo perkelta iš Bochs emuliatoriaus į QEMU/KVM įdėtas aplinkas.
- „Linux“ komponentų vaizdai naudoja „Linux 5.4.66“ branduolį.
Šaltinis: opennet.ru