Nach achtjähriger Entwicklungszeit wurde das Muen 1.0-Projekt veröffentlicht, das den Separation-Kernel entwickelte, dessen Fehlerfreiheit im Quellcode mithilfe mathematischer Methoden der formalen Zuverlässigkeitsüberprüfung bestätigt wurde. Der Kernel ist für die x86_64-Architektur verfügbar und kann in unternehmenskritischen Systemen eingesetzt werden, die ein erhöhtes Maß an Zuverlässigkeit und eine Garantie für Ausfälle erfordern. Die Quelltexte des Projekts sind in der Ada-Sprache und ihrem nachweisbaren SPARK 2014-Dialekt verfasst. Der Code wird unter der GPLv3-Lizenz vertrieben.
Der Separation Kernel ist ein Mikrokernel, der eine Umgebung für die Ausführung voneinander isolierter Komponenten bereitstellt, deren Interaktion durch festgelegte Regeln streng geregelt ist. Die Isolierung basiert auf der Verwendung von Intel VT-x-Virtualisierungserweiterungen und umfasst Schutzmechanismen, um die Organisation verdeckter Kommunikationskanäle zu blockieren. Der Partitionierungskernel ist minimalistischer und statischer als andere Mikrokernel, was die Anzahl der Situationen reduziert, die zu einem Absturz führen können.
Der Kernel läuft im VMX-Root-Modus, ähnlich dem Hypervisor, und alle anderen Komponenten laufen im Nicht-Root-VMX-Modus, ähnlich wie Gäste. Der Hardwarezugriff erfolgt über Intel VT-d DMA-Erweiterungen und Interrupt-Neuzuordnung, wodurch es möglich ist, PCI-Geräte sicher an Komponenten zu binden, die unter Muen laufen.
Zu den Fähigkeiten von Muen gehört die Unterstützung von Multi-Core-Systemen, verschachtelten Speicherseiten (EPT, Extended Page Tables), MSI (Message Signaled Interrupts) und Speicherseitenattributtabellen (PAT, Page Attribute Table). Muen bietet außerdem einen festen Schleifenplaner, der auf dem präventiven Intel VMX-Timer basiert, eine kompakte Laufzeit, die die Leistung nicht beeinträchtigt, ein Crash-Audit-System, einen regelbasierten statischen Ressourcenzuweisungsmechanismus, ein Ereignisverarbeitungssystem und gemeinsam genutzte Speicherkanäle für die Kommunikation innerhalb laufende Komponenten.
Es unterstützt die Ausführung nativer 64-Bit-Komponenten, virtueller 32-Bit- oder 64-Bit-Maschinen, 64-Bit-Ada- und SPARK 2014-Anwendungen, virtueller Linux-Maschinen und MirageOS-basierter eigenständiger Unikernels auf Muen.
Die wichtigsten Neuerungen, die in der Veröffentlichung von Muen 1.0 vorgeschlagen wurden:
- Kernel- (Gerät und Architektur), System- (Systemrichtlinien, Tau0 und Toolkit) und Komponentenspezifikationsdokumente wurden veröffentlicht, die alle Aspekte des Projekts dokumentieren.
- Das Toolkit Tau0 (Muen System Composer) wurde hinzugefügt, das eine Reihe vorgefertigter verifizierter Komponenten zum Kompilieren von Systemabbildern und zum Entwickeln typischer Dienste enthält, die auf Muen laufen. Zu den bereitgestellten Komponenten gehören AHCI-Treiber (SATA), Gerätemanager (DM), Bootloader, Systemmanager, virtuelles Terminal usw.
- Der muenblock-Linux-Treiber (eine Implementierung eines Blockgeräts, das auf dem gemeinsam genutzten Muen-Speicher läuft) wurde migriert, um die Blockdev 2.0-API zu verwenden.
- Implementierte Tools zur Verwaltung des Lebenszyklus nativer Komponenten.
- Systemabbilder wurden migriert, um SBS (Signed Block Stream) und CSL (Command Stream Loader) zum Integritätsschutz zu verwenden.
- Es wurde ein verifizierter AHCI-DRV-Treiber implementiert, der in der Sprache SPARK 2014 geschrieben ist und es Ihnen ermöglicht, Laufwerke, die die ATA-Schnittstelle unterstützen, oder separate Festplattenpartitionen an die Komponenten anzuschließen.
- Verbesserte Unikernel-Unterstützung von MirageOS- und Solo5-Projekten.
- Das Ada-Sprach-Toolkit wurde für die GNAT Community 2021-Version aktualisiert.
- Das kontinuierliche Integrationssystem wurde vom Bochs-Emulator auf verschachtelte QEMU/KVM-Umgebungen übertragen.
- Die Linux-Komponenten-Images verwenden den Linux 5.4.66-Kernel.
Source: opennet.ru