Wara tmien snin ta 'żvilupp, ġie rilaxxat il-proġett Muen 1.0, li jiżviluppa l-qalba tas-Separazzjoni, li n-nuqqas ta' żbalji fil-kodiċi tas-sors tiegħu ġie kkonfermat bl-użu ta 'metodi matematiċi ta' verifika ta 'affidabilità formali. Il-qalba hija disponibbli għall-arkitettura x86_64 u tista 'tintuża f'sistemi kritiċi għall-missjoni li jeħtieġu livell akbar ta' affidabilità u garanzija ta 'ebda fallimenti. Il-kodiċi tas-sors tal-proġett huwa miktub bil-lingwa Ada u d-djalett verifikabbli tiegħu SPARK 2014. Il-kodiċi huwa mqassam taħt il-liċenzja GPLv3.
Il-qalba tas-separazzjoni hija mikrokernel li jipprovdi ambjent għall-eżekuzzjoni ta 'komponenti iżolati minn xulxin, li l-interazzjoni tagħhom hija strettament regolata minn regoli partikolari. L-iżolament huwa bbażat fuq l-użu ta 'estensjonijiet tal-virtwalizzazzjoni Intel VT-x u jinkludi mekkaniżmi ta' sigurtà biex jimblokka l-organizzazzjoni ta 'kanali ta' komunikazzjoni moħbija. Il-qalba tal-qsim hija aktar minimalista u statika minn mikrokernels oħra, li tnaqqas in-numru ta 'sitwazzjonijiet li jistgħu jikkawżaw falliment.
Il-qalba taħdem fil-modalità għerq VMX, simili għal hypervisor, u l-komponenti l-oħra kollha jaħdmu fil-modalità mhux root VMX, simili għal sistemi mistiedna. L-aċċess għat-tagħmir isir bl-użu ta 'estensjonijiet Intel VT-d DMA u tinterrompi l-immappjar, li jagħmilha possibbli li tiġi implimentata rabta sigura ta' apparati PCI ma 'komponenti li jaħdmu taħt Muen.
Il-kapaċitajiet ta 'Muen jinkludu appoġġ għal sistemi multi-core, paġni tal-memorja nested (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), u tabelli tal-attributi tal-paġna tal-memorja (PAT, Page Attribute Table). Muen jipprovdi wkoll skedatur fiss round-robin ibbażat fuq it-tajmer preventiv Intel VMX, runtime kompatt li ma jħallix impatt fuq il-prestazzjoni, sistema ta’ verifika tal-ħabta, mekkaniżmu ta’ assenjazzjoni ta’ riżorsi statiċi bbażat fuq ir-regoli, sistema ta’ ġestjoni tal-avvenimenti, u kanali tal-memorja kondiviżi għal komunikazzjoni fi ħdan komponenti li jaħdmu.
Jappoġġja komponenti li jaħdmu b'kodiċi tal-magni ta '64-bit, magni virtwali ta' 32 jew 64-bit, applikazzjonijiet ta '64-bit fil-lingwi Ada u SPARK 2014, magni virtwali Linux u "unikernels" awtonomi bbażati fuq MirageOS fuq Muen.
L-innovazzjonijiet ewlenin offruti fir-rilaxx ta 'Muen 1.0:
- Ġew ippubblikati dokumenti bi speċifikazzjonijiet għall-kernel (apparat u arkitettura), sistema (politiki tas-sistema, Tau0 u toolkit) u komponenti, li jiddokumentaw l-aspetti kollha tal-proġett.
- Ġie miżjud is-sett ta' għodda Tau0 (Muen System Composer), li jinkludi sett ta' komponenti verifikati lesti għall-kompożizzjoni ta' immaġini tas-sistema u l-iżvilupp ta' servizzi standard li jaħdmu fuq Muen. Il-komponenti pprovduti jinkludu sewwieq AHCI (SATA), Device Manager (DM), boot loader, maniġer tas-sistema, terminal virtwali, eċċ.
- Is-sewwieq muenblock Linux (implimentazzjoni ta 'apparat tal-blokk li jaħdem fuq il-memorja kondiviża Muen) ġie kkonvertit biex juża l-API blockdev 2.0.
- Għodod implimentati għall-ġestjoni taċ-ċiklu tal-ħajja tal-komponenti indiġeni.
- Immaġini tas-sistema ġew konvertiti biex jużaw SBS (Signed Block Stream) u CSL (Command Stream Loader) biex jipproteġu l-integrità.
- Ġie implimentat sewwieq AHCI-DRV ivverifikat, miktub bil-lingwa SPARK 2014 u li jippermettilek tikkonnettja drajvs li jappoġġjaw l-interface ATA jew diviżorji individwali tad-disk mal-komponenti.
- Appoġġ unikernel imtejjeb mill-proġetti MirageOS u Solo5.
- L-għodda tal-lingwa Ada ġiet aġġornata għar-rilaxx tal-Komunità GNAT 2021.
- Is-sistema ta 'integrazzjoni kontinwa ġiet trasferita mill-emulatur Bochs għal ambjenti nested QEMU/KVM.
- Immaġini tal-komponenti Linux jużaw il-kernel Linux 5.4.66.
Sors: opennet.ru