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

Nach acht Jahren Entwicklung wurde die Version 1.0 des Projekts Muen veröffentlicht, das einen Separation Kernel entwickelt, dessen Quelltexte mithilfe mathematischer Methoden zur formalen Verifikation von Zuverlässigkeit auf Fehlerfreiheit überprüft wurden. 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 Garantien gegen Ausfälle erfordern. Die Quelltexte des Projekts sind in der Programmiersprache Ada und ihrem verifizierbaren Dialekt SPARK 2014 geschrieben. Der Code wird unter der GPLv3-Lizenz vertrieben.

Der Separation Kernel ist ein Mikrokernel, der eine Umgebung für die Ausführung isolierter Komponenten bereitstellt, deren Interaktionen streng durch festgelegte Regeln geregelt sind. Die Isolation basiert auf der Nutzung von Virtualisierungs-Extensions wie Intel VT-x und umfasst Mechanismen zum Schutz gegen die Bildung versteckter Kommunikationskanäle. Der Separation Kernel ist im Vergleich zu anderen Mikrokernen minimaler und statischer, was die Anzahl der Situationen verringert, die zu einem Ausfall führen können.

Der Kernel wird im VMX-Ring 0 ausgeführt, ähnlich wie ein Hypervisor, während alle anderen Komponenten im VMX-Ring 1 ausgeführt werden, ähnlich wie Gastbetriebssysteme. Der Zugriff auf die Hardware erfolgt unter Verwendung von Intel VT-d DMA-Extensions und der Umleitung von Interrupts, was die sichere Bindung von PCI-Geräten an unter Muen laufende Komponenten ermöglicht.

Zu den Fähigkeiten von Muen zählen die Unterstützung von Mehrkernsystemen, Nested Page Tables (EPT), MSI (Message Signaled Interrupts) und Page Attribute Tables (PAT). Muen bietet außerdem einen festen, zyklischen Scheduler basierend auf dem preemptiven Timer von Intel VMX, ein kompaktes Runtime-System ohne Leistungseinbußen, ein Überwachungsmechanismus für Abstürze, eine statische Ressourcen-Zuweisung basierend auf Regeln, ein Ereignisverarbeitungssystem und Shared Memory-Kanäle für die Interaktion zwischen den laufenden Komponenten.

Die Ausführung von Muen-Komponenten mit 64-Bit-Maschinen-Code, 32- oder 64-Bit-Anwendungen in den Sprachen Ada und SPARK 2014, virtuellen Maschinen mit Linux und selbständigen 'Unikernel'-Systemen auf Basis von MirageOS wird unterstützt. virtuelle Maschinen, 64-Bit-Anwendungen in den Sprachen Ada und SPARK 2014, virtuellen Maschinen mit Linux und eigenständigen „Unikernels“ basierend auf MirageOS.

Die wichtigsten Neuerungen, die mit der Veröffentlichung von Muen 1.0 eingeführt wurden:

• Dokumente mit den Spezifikationen des Kernels (Architektur und Design), des Systems (Systemrichtlinien, Tau0 und Werkzeuge) und der Komponenten wurden veröffentlicht, in denen alle Aspekte der Projektarbeit dokumentiert sind.
• Das Tau0-Werkzeugset (Muen System Composer) wurde hinzugefügt, das eine Sammlung von verifizierten Komponenten zur Erstellung von Systemabbildern und zur Entwicklung typischer Dienste umfasst, die über Muen ausgeführt werden. Zu den bereitgestellten Komponenten gehören der AHCI-Treiber (SATA), der Gerätemanager (DM), der Bootloader, der Systemmanager, das virtuelle Terminal usw.
• Der Linux-Treiber muenblock (Implementierung eines Blockgeräts, das über gemeinsam genutzten Speicher von Muen arbeitet) wurde auf die Verwendung der API blockdev 2.0 umgestellt.
• Werkzeuge zur Verwaltung des Lebenszyklus von nativen Komponenten wurden 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, der in der Sprache SPARK 2014 geschrieben wurde, wurde implementiert, der es ermöglicht, Speichermedien, die das ATA-Interface unterstützen, oder einzelne Festplattenteile an die Komponenten anzuschließen.
• Die Unterstützung von Unikernels aus den Projekten MirageOS und Solo5 wurde verbessert.
• Das Werkzeugset für die Programmiersprache Ada wurde auf die Version GNAT Community 2021 aktualisiert.
• Das System zur kontinuierlichen Integration wurde von dem Emulator Bochs auf die verschachtelten Umgebungen QEMU/KVM umgestellt.
• In den Linux-Komponentenabbildern wurde der Linux-Kernel 5.4.66 verwendet.

Quelle: opennet.ru