Veröffentlichung von Muen 1.0, einem offenen Mikrokern zur Erstellung hochzuverlässiger Systeme

Nach achtjähriger Entwicklung wurde das Projekt Muen 1.0 veröffentlicht, das einen Separation Kernel entwickelt. Die Fehlerfreiheit des Quellcodes wurde durch mathematische Methoden der formalen Verifizierung der Zuverlässigkeit bestätigt. Der Kernel ist für die Architektur x86_64 verfügbar und kann in sicherheitskritischen Systemen eingesetzt werden, die ein hohes Maß an Zuverlässigkeit und Garantie für Störungsfreiheit erfordern. Der Quellcode des Projekts ist in der Programmiersprache Ada und dessen verifizierbarem Dialekt SPARK 2014 geschrieben. Der Code wird unter der Lizenz GPLv3 verbreitet.

Der Separation Kernel ist ein Mikrokernel, der eine Umgebung für die Ausführung isolierter Komponenten bereitstellt, deren Interaktion streng durch festgelegte Regeln geregelt ist. Die Isolation basiert auf der Verwendung der Intel VT-x Virtualisierungs-Extensions und umfasst auch Schutzmechanismen zur Verhinderung versteckter Kommunikationskanäle. Im Vergleich zu anderen Mikrokernen ist der Separation Kernel minimalistischer und stabiler, was die Anzahl möglicher Fehlerszenarien verringert.

Der Kernel läuft im Root-Modus VMX ähnlich wie ein Hypervisor, während alle anderen Komponenten im Non-Root-Modus VMX ähnlich wie Gastsysteme ausgeführt werden. Der Zugriff auf die Hardware erfolgt über die Intel VT-d DMA-Extensions und Interrupt-Remapping, was die sichere Bindung von PCI-Geräten an unter Muen ausgeführte Komponenten ermöglicht.

Die Möglichkeiten von Muen beinhalten die Unterstützung von Mehrkernsystemen, verschachtelten Seitentabellen (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), und Seitenattributtabellen (PAT, Page Attribute Table). Muen bietet außerdem einen festen zyklischen Scheduler auf Basis des preemptiven Timers Intel VMX, ein kompaktes Runtime, das die Leistung nicht beeinträchtigt, ein Absturz-Audit-System, einen statischen Ressourcen-Zuweisungsmechanismus basierend auf Regeln, ein Ereignisverarbeitungssystem und Shared-Memory-Kanäle für die Interaktion innerhalb der laufenden Komponenten.

Der Start von Muen-Komponenten mit 64-Bit-Maschinencode, 32-Bit- oder 64-Bit-Anwendungen in den Sprachen Ada und SPARK 2014 sowie virtuellen Maschinen mit Linux und eigenständigen "unikernel"-Systemen basierend auf MirageOS wird unterstützt. virtuellen Maschinen, 64-bit Anwendungen in den Programmiersprachen Ada und SPARK 2014, virtuellen Maschinen mit Linux und eigenständigen «unikernel» basierend auf MirageOS.

Die wichtigsten Neuerungen in der Version Muen 1.0:

• Dokumente mit den Spezifikationen des Kernels (Gerät und Architektur), des Systems (Systempolitiken, Tau0 und Werkzeuge) und der Komponenten wurden veröffentlicht, in denen alle Aspekte der Funktionsweise des Projekts dokumentiert sind.
• Das Tau0-Toolkit (Muen System Composer) wurde hinzugefügt, das eine Reihe von verifizierten Komponenten zur Erstellung von Systemabbildern und zur Entwicklung von Standarddiensten, die auf Muen laufen, beinhaltet. Zu den bereitgestellten Komponenten gehören der AHCI (SATA) Treiber, der Device Manager (DM), der Bootloader, der Systemmanager, das virtuelle Terminal usw.
• Der Linux-Treiber muenblock (Implementierung eines Blockgeräts, das über gemeinsamen Speicher Muen funktioniert) wurde auf die Verwendung der API blockdev 2.0 umgestellt.
• Es wurden Werkzeuge zur Verwaltung des Lebenszyklus nativer Komponenten implementiert.
• Die Systemabbilder wurden auf die Verwendung von SBS (Signed Block Stream) und CSL (Command Stream Loader) umgestellt, um die Integrität zu schützen.
• Ein verifizierter AHCI-DRV-Treiber, geschrieben in SPARK 2014, wurde implementiert, der die Verbindung zu Speichermedien unterstützt, die das ATA-Interface oder einzelne Festplattenpartitionen nutzen.
• Die Unterstützung für Unikernel von den Projekten MirageOS und Solo5 wurde verbessert.
• Das Toolkit für die Programmiersprache Ada wurde auf die GNAT Community 2021-Version aktualisiert.
• Das System zur kontinuierlichen Integration wurde von dem Emulator Bochs auf verschachtelte Umgebungen QEMU/KVM umgestellt.
• In den Komponentenabbildern mit Linux wird der Linux-Kernel 5.4.66 verwendet.

Quelle: opennet.ru