Nyolc év fejlesztés után megjelent a Muen 1.0 projekt, amely a Separation kernelt fejlesztette, amelynek forráskódjában a hibák hiányát a formális megbízhatóság-ellenőrzés matematikai módszereivel igazolták. A kernel elérhető az x86_64 architektúrához, és olyan kritikus fontosságú rendszerekben használható, amelyek fokozott megbízhatóságot és hibamentességet igényelnek. A projekt forráskódja Ada nyelven és annak ellenőrizhető dialektusában SPARK 2014-ben készült. A kód GPLv3 licenc alatt kerül terjesztésre.
Az elválasztó kernel olyan mikrokernel, amely környezetet biztosít az egymástól elszigetelt komponensek végrehajtásához, amelyek interakcióját adott szabályok szigorúan szabályozzák. Az elkülönítés az Intel VT-x virtualizációs kiterjesztéseinek használatán alapul, és olyan biztonsági mechanizmusokat tartalmaz, amelyek blokkolják a titkos kommunikációs csatornák szervezését. A particionáló kernel minimalistabb és statikusabb, mint a többi mikrokernel, ami csökkenti a hibákat okozó helyzetek számát.
A kernel VMX root módban fut, hasonlóan a hypervisorhoz, az összes többi összetevő pedig VMX nem root módban fut, hasonlóan a vendégrendszerekhez. A berendezéshez való hozzáférés Intel VT-d DMA kiterjesztések és megszakítások újraleképezése segítségével történik, ami lehetővé teszi a PCI-eszközök biztonságos összekapcsolását a Muen alatt futó komponensekhez.
A Muen képességei közé tartozik a többmagos rendszerek, a beágyazott memórialapok (EPT, Extended Page Tables), az MSI (Message Signaled Interrupts) és a memórialap-attribútumtáblázatok (PAT, Page Attribute Table) támogatása. A Muen emellett az Intel VMX megelőző időzítőn alapuló fix körbefutó ütemezőt, a teljesítményt nem befolyásoló kompakt futásidőt, összeomlás-ellenőrző rendszert, szabályalapú statikus erőforrás-hozzárendelési mechanizmust, eseménykezelő rendszert és megosztott memóriacsatornákat is biztosít. kommunikáció a futó alkatrészeken belül.
Támogatja a 64 bites gépi kóddal futó komponenseket, 32 vagy 64 bites virtuális gépeket, 64 bites alkalmazásokat Ada és SPARK 2014 nyelveken, Linux virtuális gépeket és a Muen tetején lévő MirageOS alapú önálló „unikerneleket”.
A Muen 1.0 kiadásában kínált fő újítások:
- Dokumentumokat tettek közzé a kernel (eszköz és architektúra), a rendszer (rendszerházirendek, Tau0 és eszközkészlet) és az összetevők specifikációival, amelyek dokumentálják a projekt minden vonatkozását.
- Hozzáadásra került a Tau0 (Muen System Composer) eszközkészlet, amely kész ellenőrzött összetevőket tartalmaz a rendszerképek összeállításához és a Muen tetején futó szabványos szolgáltatások fejlesztéséhez. A mellékelt összetevők közé tartozik az AHCI (SATA) illesztőprogram, az eszközkezelő (DM), a rendszertöltő, a rendszerkezelő, a virtuális terminál stb.
- A muenblock Linux illesztőprogram (a Muen megosztott memórián futó blokkeszköz megvalósítása) át lett alakítva a blockdev 2.0 API használatára.
- Megvalósított eszközök a natív komponensek életciklusának kezelésére.
- A rendszerképeket SBS (Signed Block Stream) és CSL (Command Stream Loader) használatára alakították át az integritás védelme érdekében.
- Ellenőrzött AHCI-DRV illesztőprogram került megvalósításra, amely a SPARK 2014 nyelven íródott, és lehetővé teszi az ATA interfészt támogató meghajtók vagy az egyes lemezpartíciók komponensekhez való csatlakoztatását.
- Továbbfejlesztett unikernel támogatás a MirageOS és Solo5 projektekből.
- Az Ada nyelvi eszköztár frissítve lett a GNAT Community 2021 kiadásához.
- A folyamatos integrációs rendszer a Bochs emulátorból átkerült a QEMU/KVM beágyazott környezetekbe.
- A Linux összetevő képfájlok a Linux 5.4.66 rendszermagot használják.
Forrás: opennet.ru