Muen Kernel als Fundament für Software im Hochsicherheitsbereich
Der Open-Source-Kernel wurde mit der Programmiersprache SPARK und dem GNAT Ada Toolset erstellt. Er soll die Isolierung von Komponenten gewähren und sicherheitskritische Funktionen vor fehlerhafter Software auf dem gleichen System schützen
- Alexander Neumann
Das Institut für Internet-Technologien und Anwendungen an der Hochschule für Technik in Rapperswil hat ein Preview Release des Muen Separation Kernel vorgestellt. Der formal verifizierte Open-Source-Kernel wurde mit der Ada-basierten Programmiersprache SPARK und dem GNAT Ada Toolset von AdaCore erstellt. Der Muen-Kernel soll eine strikte und zuverlässige Isolierung von Komponenten gewähren und sicherheitskritische Funktionen vor fehlerhafter Software schützen, die auf dem gleichen physischen System läuft.
Der japanische Begriff "Muen" bedeutet "unabhängig" oder "ohne Beziehung untereinander" und steht für das Ziel des Separation Kernel: die Trennung der Komponenten. Da ein Separation Kernel die Isolierung, die Ressourcenkontrolle und den Datenfluss in einem komponentenbasierten System sicherstellt, hätte jeder Fehler im Kernel fatale Auswirkungen auf die Sicherheit aller Komponenten. Um solche schwerwiegenden Auswirkungen zu verhindern, haben sich die Entwickler dazu entschieden, den Muen Kernel mit der Programmiersprache SPARK zu erstellen.
SPARK umfasst die gleichnamige Programmiersprache und ein Toolset für die Entwicklung von Software im Hochsicherheitsbereich. Sie verbindet die Sprache und Verifikations-Tools von Altrans SPARK mit dem GNAT Programming Studio von AdaCore.
Das Muen-Team nutzte das SPARK-Toolset zur statischen Überprüfung des Kernels und zur Prüfung der Abwesenheit von Laufzeitfehlern. In Zukunft soll anscheinend auch die funktionale Korrektheit des Kernels durch den Einsatz von SPARK und einem interaktiven Theorembeweiser gezeigt werden. Die Muen-Entwickler nutzten SPARK in Kombination mit einer Zero-Footprint Runtime, einem Modus, der keine Laufzeitumgebung und nur wenig unterstützenden Code erfordert. Dieses Setup ist für kritische Low-Level-Programmierung gedacht, da das System keine unnötigen Bibliotheken aufweist.
Auf dem Git-Repository für den Kernel steht auch ein Snapshot des Muen Repositories zum Download bereit. Der Kernel ist unter der GPLv3 lizenziert. (ane)
