Nyolc év fejlesztés után megjelent a Muen 1.0 projekt, amely a szeparációs kernel magját fejleszti. A forráskód hibátlanságát matematikai formális verifikációs módszerek segítségével igazolták. A kernel elérhető az x86_64 architektúrához, és olyan kritikus rendszerekben alkalmazható, amelyek magas szintű megbízhatóságot és a hibák hiányának garanciáját igénylik. A projekt forrása Ada nyelven és annak verifikálható SPARK 2014 dialektusában készült. A kód GPLv3 licenc alatt terjeszthető.
A szeparációs kernel egy mikrokernel, amely lehetőséget biztosít elszigetelt, egymástól független komponensek futtatására, amelyek közötti interakciót szigorúan meghatározott szabályok szabályozzák. Az elszigetelés az Intel VT-x virtualizációs kiterjesztések alkalmazásán alapul, és magában foglalja a rejtett kommunikációs csatornák létrehozásának blokkolására szolgáló védelmi mechanizmusokat is. A szeparációs kernel minimalistább és statikusabb, mint más mikrokernel, ami csökkenti a leálláshoz vezető helyzetek számát.
A kernel a VMX gyökér módban fut a hipervízorhoz hasonlóan, míg az összes többi komponens a VMX nem gyökér módban működik a vendég rendszerekhez hasonlóan. A hardverhez való hozzáférés az Intel VT-d DMA kiterjesztések és az interrupt remapping használatával történik, ami lehetővé teszi a PCI-eszközök biztonságos kötését a Muen által vezérelt komponensekhez.
A Muen lehetőségei között szerepel a többmagos rendszerek támogatása, a beágyazott memóriaoldalak (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), valamint a memóriaoldalak attribútumainak táblái (PAT, Page Attribute Table). A Muen emellett fix ciklikus ütemezőt biztosít az Intel VMX preemptív időzítője alapján, kompakt runtime-t, amely nem befolyásolja a teljesítményt, összeomlások audit rendszerét, szabályokon alapuló statikus erőforrás-kiosztási mechanizmust, eseménykezelő rendszert és megosztott memória csatornákat a futó komponensek közötti interakcióhoz.
Támogatott a Muen felett futó komponensek indítása 64 bites gépi kód, 32- vagy 64 bites, 64 bites Ada és SPARK 2014 nyelvű alkalmazások, Linux alapú virtuális gépek és önálló 'unikernel' rendszer MirageOS alapján. virtuális gépekhez, 64-bites alkalmazások Ada és SPARK 2014 nyelveken, Linux-alapú virtuális gépek és önálló „unikernel” MirageOS alapokon.
A Muen 1.0 kiadás által javasolt fő újdonságok:
- Megjelentek a mag specifikációit, a rendszert (rendszerpolitikai, Tau0 és eszköztár) és a komponenseket bemutató dokumentumok, amelyekben a projekt működésének minden aspektusát dokumentálták.
- Hozzáadtuk a Tau0 eszköztárat (Muen System Composer), amely kész, ellenőrzött komponensek sorozatát tartalmazza a rendszersablonok összeállításához és a Muen felületén futó tipikus szolgáltatások fejlesztéséhez. A rendelkezésre álló komponensek között szerepel az AHCI (SATA) illesztőprogram, a Device Manager (DM), a bootloader, a rendszerkezelő, a virtuális terminál stb.
- A muenblock Linux-illesztőprogram (a megosztott memória Muen feletti blokkeszköz-implementációja) át lett állítva a blockdev 2.0 API használatára.
- Eszközök valós komponensek életciklusának kezelésére valósultak meg.
- A rendszersablonok át lettek állítva az SBS (Signed Block Stream) és a CSL (Command Stream Loader) használatára az integritás védelme érdekében.
- Megvalósult egy ellenőrzött AHCI-DRV illesztőprogram, amely SPARK 2014 nyelven íródott, és lehetővé teszi az ATA interfésszel rendelkező tárolók vagy külön lemezpartíciók csatlakoztatását a komponensekhez.
- Javítottuk a unikernel támogatását a MirageOS és a Solo5 projektekből.
- Az Ada nyelvi eszköztár frissítve lett a GNAT Community 2021 kiadására.
- A folyamatos integrációs rendszer át lett állítva a Bochs emulátorról a QEMU/KVM beágyazott környezetekre.
- A Linux-alapú komponensképekben a Linux 5.4.66 kernel került alkalmazásra.
Forrás: opennet.ru
