Pēc astoņu gadu izstrādes tika izlaists Muen 1.0 projekts, kas izstrādāja Separation kodolu, kura avota kodā kļūdu neesamība tika apstiprināta, izmantojot formālās uzticamības pārbaudes matemātiskās metodes. Kodols ir pieejams x86_64 arhitektūrai, un to var izmantot misijai kritiskās sistēmās, kurām nepieciešams paaugstināts uzticamības līmenis un garantija, ka nav kļūdu. Projekta pirmkods ir rakstīts Ada valodā un tās pārbaudāmajā dialektā SPARK 2014. Kods tiek izplatīts saskaņā ar GPLv3 licenci.
Atdalīšanas kodols ir mikrokodolis, kas nodrošina vidi viena no otras izolētu komponentu izpildei, kuru mijiedarbību stingri reglamentē dotie noteikumi. Izolēšana ir balstīta uz Intel VT-x virtualizācijas paplašinājumu izmantošanu un ietver drošības mehānismus, lai bloķētu slēpto sakaru kanālu organizēšanu. Sadalīšanas kodols ir minimālistiskāks un statiskāks nekā citi mikrokodoli, kas samazina to situāciju skaitu, kas var izraisīt kļūmi.
Kodols darbojas VMX saknes režīmā, līdzīgi kā hipervizoram, un visi pārējie komponenti darbojas VMX bezsaknes režīmā, līdzīgi kā viesu sistēmām. Piekļuve aprīkojumam tiek nodrošināta, izmantojot Intel VT-d DMA paplašinājumus un pārtraukumu pārkartēšanu, kas ļauj īstenot drošu PCI ierīču saistīšanu ar komponentiem, kas darbojas saskaņā ar Muen.
Muen iespējas ietver atbalstu vairāku kodolu sistēmām, ligzdotām atmiņas lapām (EPT, Extended Page Tables), MSI (Ziņojuma signāla pārtraukumi) un atmiņas lapu atribūtu tabulām (PAT, Page Attribute Table). Muen nodrošina arī fiksētu apļveida plānotāju, kura pamatā ir Intel VMX preventīvais taimeris, kompaktu izpildlaiku, kas neietekmē veiktspēju, avāriju auditēšanas sistēmu, uz kārtulām balstītu statisko resursu piešķiršanas mehānismu, notikumu apstrādes sistēmu un koplietotus atmiņas kanālus komunikācija darba komponentos.
Tā atbalsta darbināmus komponentus ar 64 bitu mašīnkodu, 32 bitu vai 64 bitu virtuālās mašīnas, 64 bitu lietojumprogrammas Ada un SPARK 2014 valodās, Linux virtuālās mašīnas un autonomus “unikernels”, kuru pamatā ir MirageOS un Muen.
Galvenās Muen 1.0 izlaidumā piedāvātās inovācijas:
- Ir publicēti dokumenti ar kodola (ierīce un arhitektūra), sistēmas (sistēmas politikas, Tau0 un rīkkopa) un komponentu specifikācijām, kas dokumentē visus projekta aspektus.
- Ir pievienots Tau0 (Muen System Composer) rīku komplekts, kurā ir iekļauts gatavu pārbaudītu komponentu komplekts sistēmas attēlu veidošanai un standarta pakalpojumu izstrādei, kas darbojas ar Muen. Piedāvātie komponenti ietver AHCI (SATA) draiveri, ierīču pārvaldnieku (DM), sāknēšanas ielādētāju, sistēmas pārvaldnieku, virtuālo termināli utt.
- Muenblock Linux draiveris (blokierīces ieviešana, kas darbojas Muen koplietotās atmiņas virspusē) ir pārveidota, lai izmantotu blockdev 2.0 API.
- Ieviesti rīki vietējo komponentu dzīves cikla pārvaldībai.
- Sistēmas attēli ir pārveidoti, lai izmantotu SBS (Signed Block Stream) un CSL (Command Stream Loader), lai aizsargātu integritāti.
- Ir ieviests verificēts AHCI-DRV draiveris, kas rakstīts SPARK 2014 valodā un ļauj komponentiem savienot diskus, kas atbalsta ATA interfeisu vai atsevišķas diska nodalījumus.
- Uzlabots unikernel atbalsts no MirageOS un Solo5 projektiem.
- Ada valodas rīkkopa ir atjaunināta GNAT Community 2021 laidienam.
- Nepārtrauktās integrācijas sistēma ir pārvietota no Bochs emulatora uz QEMU/KVM ligzdotajām vidēm.
- Linux komponentu attēli izmanto Linux 5.4.66 kodolu.
Avots: opennet.ru