Po ośmiu latach prac rozwojowych zadebiutował projekt Muen 1.0, rozwijający jądro separacji, którego brak błędów w kodzie źródłowym potwierdzono metodami formalnej weryfikacji bezpieczeństwa. Jądro jest dostępne dla architektury x86_64 i może być stosowane w systemach krytycznych, które wymagają wysokiego poziomu niezawodności i gwarancji braku awarii. Kody źródłowe projektu zostały napisane w języku Ada oraz jego weryfikowalnej wersji SPARK 2014. Kod jest rozpowszechniany na licencji GPLv3.
Jądro separacji to mikrojądro, które zapewnia środowisko do działania izolowanych od siebie komponentów, których interakcje są ściśle regulowane określonymi zasadami. Izolacja opiera się na zastosowaniu rozszerzeń wirtualizacji Intel VT-x, a także przewiduje mechanizmy ochronne zapobiegające powstawaniu ukrytych kanałów komunikacyjnych. Jądro separacji jest bardziej minimalistyczne i statyczne w porównaniu do innych mikrojąder, co pozwala zredukować liczbę sytuacji mogących prowadzić do awarii.
Jądro działa w trybie korzennym VMX, analogicznie do hipernadzorcy, natomiast wszystkie pozostałe komponenty działają w trybie niekorzennym VMX, tak jak systemy gościnne. Dostęp do sprzętu odbywa się przy użyciu rozszerzeń Intel VT-d DMA oraz remappingu przerwań, co umożliwia bezpieczne przypisanie urządzeń PCI do komponentów uruchamianych pod kontrolą Muen.
Wśród możliwości Muen wyróżnia się wsparcie dla systemów wielordzeniowych, zagnieżdżonych stron pamięci (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), a także tabel atrybutów stron pamięci (PAT, Page Attribute Table). Muen oferuje także ustalony cykliczny harmonizator oparty na wykluczającym timerze Intel VMX, kompaktowy runtime, który nie wpływa na wydajność, system audytu awarii, mechanizm statycznego przydzielania zasobów na podstawie reguł, system obsługi zdarzeń oraz kanały pamięci wspólnej do komunikacji wewnątrz uruchamianych komponentów.
Wspierane jest uruchamianie komponentów na Muen z 64-bitowym kodem maszynowym, 32- lub 64-bitowych maszyn wirtualnych, 64-bitowych aplikacji napisanych w językach Ada i SPARK 2014, maszyn wirtualnych z Linux oraz samowystarczalnych 'unikernel' na bazie MirageOS.
Główne nowości w wydaniu Muen 1.0:
- Opublikowano dokumenty ze specyfikacjami jądra (budowa i architektura), systemu (polityki systemowe, Tau0 i narzędzia) oraz komponentów, w których udokumentowano wszystkie aspekty działania projektu.
- Dodano narzędzie Tau0 (Muen System Composer), które zawiera zestaw gotowych, zweryfikowanych komponentów do tworzenia obrazów systemowych i opracowywania typowych usług działających na Muen. Wśród dostarczanych komponentów znajdują się sterownik AHCI (SATA), Menedżer Urządzeń (DM), bootloader, menedżer systemowy, wirtualny terminal itp.
- Sterownik Linux muenblock (realizacja urządzenia blokowego działającego na współdzielonej pamięci Muen) został przeniesiony na korzystanie z API blockdev 2.0.
- Zrealizowano narzędzia do zarządzania cyklem życia natywnych komponentów.
- Obrazy systemowe zostały przeniesione na korzystanie z SBS (Signed Block Stream) i CSL (Command Stream Loader) w celu ochrony integralności.
- Zrealizowano zweryfikowany sterownik AHCI-DRV, napisany w języku SPARK 2014, który umożliwia podłączanie do komponentów nośników obsługujących interfejs ATA lub oddzielnych partycji dyskowych.
- Zwiększono wsparcie dla unikernel z projektów MirageOS i Solo5.
- Narzędzia dla języka Ada zostały zaktualizowane do wydania GNAT Community 2021.
- System ciągłej integracji został przeniesiony z emulatora Bochs na zagnieżdżone środowiska QEMU/KVM.
- W obrazach komponentów z Linux wykorzystano jądro Linux 5.4.66.
Źródło: opennet.ru
