Po ośmiu latach rozwoju wypuszczono projekt Muen 1.0 rozwijający jądro Separation, którego brak błędów w kodzie źródłowym potwierdzono matematycznymi metodami formalnej weryfikacji niezawodności. Jądro jest dostępne dla architektury x86_64 i może być stosowane w systemach o znaczeniu krytycznym, które wymagają zwiększonego poziomu niezawodności i gwarancji braku awarii. Kod źródłowy projektu napisany jest w języku Ada i jego sprawdzalnym dialekcie SPARK 2014. Kod rozpowszechniany jest na licencji GPLv3.
Jądro separacji to mikrojądro zapewniające środowisko do wykonywania odizolowanych od siebie komponentów, których wzajemne oddziaływanie jest ściśle regulowane określonymi regułami. Izolacja opiera się na wykorzystaniu rozszerzeń wirtualizacji Intel VT-x i zawiera mechanizmy bezpieczeństwa blokujące organizację tajnych kanałów komunikacji. Jądro partycjonujące jest bardziej minimalistyczne i statyczne niż inne mikrojądra, co zmniejsza liczbę sytuacji, które mogą spowodować awarię.
Jądro działa w trybie root VMX, podobnie jak hypervisor, a wszystkie inne komponenty działają w trybie innym niż root VMX, podobnie jak systemy gościa. Dostęp do sprzętu odbywa się za pomocą rozszerzeń Intel VT-d DMA i remapowania przerwań, co umożliwia realizację bezpiecznego łączenia urządzeń PCI z komponentami działającymi pod kontrolą Muen.
Możliwości Muena obejmują obsługę systemów wielordzeniowych, zagnieżdżonych stron pamięci (EPT, rozszerzone tablice stron), MSI (przerwania sygnalizowane komunikatem) i tabele atrybutów stron pamięci (PAT, tabela atrybutów stron). Muen zapewnia także stały harmonogram okrężny oparty na zegarze z wywłaszczaniem Intel VMX, kompaktowe środowisko wykonawcze, które nie wpływa na wydajność, system kontroli awarii, oparty na regułach mechanizm przydzielania zasobów statycznych, system obsługi zdarzeń i kanały pamięci współdzielonej dla komunikacja wewnątrz działających komponentów.
Obsługuje działające komponenty z 64-bitowym kodem maszynowym, 32- lub 64-bitowe maszyny wirtualne, 64-bitowe aplikacje w językach Ada i SPARK 2014, maszyny wirtualne Linux i samodzielne „unikernels” oparte na MirageOS na platformie Muen.
Główne innowacje oferowane w wersji Muen 1.0:
- Opublikowano dokumenty zawierające specyfikacje jądra (urządzenie i architektura), systemu (polityki systemowe, Tau0 i zestaw narzędzi) oraz komponentów, które dokumentują wszystkie aspekty projektu.
- Dodano zestaw narzędzi Tau0 (Muen System Composer), który zawiera zestaw gotowych, zweryfikowanych komponentów do tworzenia obrazów systemów i tworzenia standardowych usług działających na Muen. Dostarczone komponenty obejmują sterownik AHCI (SATA), Menedżer urządzeń (DM), moduł ładujący, menedżer systemu, terminal wirtualny itp.
- Sterownik muenblock dla systemu Linux (implementacja urządzenia blokowego działającego w oparciu o pamięć współdzieloną Muen) został przekonwertowany tak, aby korzystał z interfejsu API blockdev 2.0.
- Wdrożone narzędzia do zarządzania cyklem życia komponentów natywnych.
- Obrazy systemu zostały przekonwertowane tak, aby korzystały z SBS (Signed Block Stream) i CSL (Command Stream Loader), aby chronić integralność.
- Zaimplementowano zweryfikowany sterownik AHCI-DRV, napisany w języku SPARK 2014 i pozwalający na podłączenie do podzespołów dysków obsługujących interfejs ATA lub poszczególnych partycji dyskowych.
- Ulepszona obsługa unikernel z projektów MirageOS i Solo5.
- Zestaw narzędzi językowych Ada został zaktualizowany do wersji GNAT Community 2021.
- System ciągłej integracji został przeniesiony z emulatora Bochs do środowisk zagnieżdżonych QEMU/KVM.
- Obrazy komponentów systemu Linux korzystają z jądra systemu Linux 5.4.66.
Źródło: opennet.ru