Na agt jaar van ontwikkeling is die Muen 1.0-projek vrygestel, wat die Skeidingkern ontwikkel het, waarvan die afwesigheid van foute in die bronkode bevestig is met behulp van wiskundige metodes van formele betroubaarheidsverifikasie. Die kern is beskikbaar vir die x86_64-argitektuur en kan gebruik word in missiekritieke stelsels wat 'n verhoogde vlak van betroubaarheid en waarborg van geen foute vereis nie. Die bronkode van die projek is geskryf in die Ada-taal en sy verifieerbare dialek SPARK 2014. Die kode word onder die GPLv3-lisensie versprei.
Die skeidingskern is 'n mikrokern wat 'n omgewing bied vir die uitvoering van komponente wat van mekaar geïsoleer is, waarvan die interaksie streng deur gegewe reëls gereguleer word. Isolasie is gebaseer op die gebruik van Intel VT-x-virtualiseringsuitbreidings en sluit sekuriteitsmeganismes in om die organisasie van geheime kommunikasiekanale te blokkeer. Die partisiekern is meer minimalisties en staties as ander mikrokernele, wat die aantal situasies verminder wat mislukking kan veroorsaak.
Die kern loop in VMX-wortelmodus, soortgelyk aan 'n hypervisor, en alle ander komponente loop in VMX nie-wortelmodus, soortgelyk aan gasstelsels. Toegang tot die toerusting word gemaak met behulp van Intel VT-d DMA-uitbreidings en onderbrekingsherkartering, wat dit moontlik maak om veilige binding van PCI-toestelle aan komponente wat onder Muen loop, te implementeer.
Muen se vermoëns sluit in ondersteuning vir multi-kern stelsels, geneste geheue bladsye (EPT, Uitgebreide Bladsy Tables), MSI (Message Signaled Interrupts), en geheue bladsy kenmerk tabelle (PAT, Page Attribute Table). Muen bied ook 'n vaste round-robin skeduleerder gebaseer op die Intel VMX preemptive timer, 'n kompakte looptyd wat nie werkverrigting beïnvloed nie, 'n ongelukouditeringstelsel, 'n reëlgebaseerde statiese hulpbrontoewysingsmeganisme, 'n gebeurtenishanteringstelsel en gedeelde geheuekanale vir kommunikasie binne lopende komponente.
Dit ondersteun lopende komponente met 64-bis masjienkode, 32- of 64-bis virtuele masjiene, 64-bis toepassings in Ada en SPARK 2014 tale, Linux virtuele masjiene en selfstandige "unikernels" gebaseer op MirageOS bo-op Muen.
Die belangrikste innovasies wat aangebied word in die vrystelling van Muen 1.0:
- Dokumente is gepubliseer met spesifikasies vir die kern (toestel en argitektuur), stelsel (stelselbeleide, Tau0 en toolkit) en komponente, wat alle aspekte van die projek dokumenteer.
- Die Tau0 (Muen System Composer) gereedskapstel is bygevoeg, wat 'n stel klaargemaakte geverifieerde komponente insluit vir die samestelling van stelselbeelde en die ontwikkeling van standaarddienste wat bo-op Muen loop. Komponente wat verskaf word, sluit in AHCI (SATA) bestuurder, Device Manager (DM), selflaailaaier, stelselbestuurder, virtuele terminale, ens.
- Die muenblock Linux-bestuurder ('n implementering van 'n bloktoestel wat bo-op die Muen-gedeelde geheue loop) is omgeskakel om die blockdev 2.0 API te gebruik.
- Geïmplementeerde gereedskap vir die bestuur van die lewensiklus van inheemse komponente.
- Stelselbeelde is omgeskakel om SBS (Signed Block Stream) en CSL (Command Stream Loader) te gebruik om integriteit te beskerm.
- 'n Geverifieerde AHCI-DRV-bestuurder is geïmplementeer, geskryf in die SPARK 2014-taal en laat jou toe om aandrywers wat die ATA-koppelvlak of individuele skyfpartisies ondersteun, aan die komponente te koppel.
- Verbeterde unieke ondersteuning van MirageOS- en Solo5-projekte.
- Die Ada-taalgereedskapstel is opgedateer vir die GNAT Community 2021-vrystelling.
- Die deurlopende integrasiestelsel is oorgedra vanaf die Bochs-emulator na QEMU/KVM geneste omgewings.
- Linux komponent beelde gebruik die Linux 5.4.66 kern.
Bron: opennet.ru