Neues Release des Muen-Kernels für Open-Source-Software im Hochsicherheitsbereich

Paris und Rapperswil, 13. Januar 2015 – Die Hochschule für Technik (http://www.hsr.ch) in Rapperswil und AdaCore haben die Entwicklerversion 0.6 des Open-Source Muen Separation Kernel (http://muen.codelabs.ch) vorgestellt. Der unter Verwendung formaler Methoden entwickelte Kernel wurde erfolgreich auf die SPARK-2014-Technologie aktualisiert.

Der Muen-Kernel gewährleistet eine strikte und zuverlässige Isolierung von Komponenten und schützt sicherheitskritische Funktionen vor fehlerhafter Software, die auf dem gleichen physischen System läuft. Um eine besonders hohe Vertrauenswürdigkeit zu erreichen, verwendet das Muen-Team die Programmiersprache SPARK mit den zugehörigen Entwicklungswerkzeugen, um die Abwesenheit von Laufzeitfehlern formal nachzuweisen. Die AdaCore- und Muen-Teams haben bei der Erstellung der Version 0.6 eng zusammengearbeitet und konnten so ein erfolgreiches Upgrade der Software für SPARK 2014 sicherstellen. Die Kernel-Entwicklung am Institut für Internet-Technologien und Anwendungen (http://www.ita.hsr.ch) an der Hochschule für Technik (http://www.hsr.ch) im schweizerischen Rapperswil wird von der Essener secunet Security Networks AG in Deutschland, die Muen in ihrer Produktentwicklung einsetzt, unterstützt.

SPARK 2014 stellt eine große Verbesserung der SPARK-Sprache dar; es erweitert den einsetzbaren Sprachumfang und integriert außerdem die standardisierte Syntax und Semantik von Ada 2012 für die vertragsbasierte Programmierung. Die Kompatibilität mit Ada 2012 ermöglicht einen neuartigen und produktiven Ansatz zur Software-Verifikation und unterstützt sowohl formale Methoden – durch statische Durchsetzung von „Verträgen“ mit der neuen GNATprove-Technologie – als auch traditionelle testbasierte Verfahren durch Laufzeitüberprüfungen. Es erleichtert den Ãœbergang von Ada zu SPARK, weil die spezielle Syntax-Annotation früherer SPARK-Versionen nicht mehr benötigt wird. Die SPARK-2014-Unterstützung ist mit GNAT Programming Studio (GPS) und aus GNATbench, den integrierten Entwicklungsumgebungen von AdaCore, zugänglich und kann von Benutzern des AdaCore SPARK Pro Toolset genutzt werden.

Seit der zuletzt veröffentlichten Vorabversion im Herbst 2013 hat die Muen-Plattform deutliche Fortschritte gemacht. Neben der Unterstützung für Linux-VMs wurde das sichere Durchreichen von PCI-Geräten an Gastsysteme unter Verwendung der Intel-VT-d-DMA- und Interrupt-Remapping-Mechanismen implementiert. Des Weiteren ermöglicht die überarbeitete Sprache zur Systembeschreibung eine einfachere Integration von komplexen, komponentenbasierten Systemen mit Muen.

„Der Muen Separation Kernel bietet eine leistungsfähige Plattform für Hochsicherheitssysteme, die es ermöglicht, bestehende Funktionalität von nicht-vertrauenswürdigen Komponenten sicher zu nutzen“, erklärt Dr. Kai Martius, CTO der secunet Security Networks AG in Essen. „SPARK 2014 erlaubt es uns, die Isolations- und Sicherheitseigenschaften von Muen und kritischen Komponenten auf effiziente Weise formal zu beweisen.“

„Durch die schnelle Adaptierung der Funktionen von SPARK 2014 hat das Muen-Team unsere Annahme bestätigt, dass die neue Version der Sprache und der damit verbundenen Technologie einfacher zu verstehen und dabei mindestens so leistungsfähig ist wie die alte Version“, sagt Cyrille Comar, Geschäftsführer von AdaCore. „Es zeigt sich, dass das neue Produkt auch die Anforderungen von sicherheitsorientierten Entwicklern erfüllt, die statische Verifikation möglichst umfassend einsetzen wollen, einschließlich manueller Beweise, sofern nötig.“

Diese Presseinformation kann auch unter www.pr-com.de/adacore abgerufen werden.