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

Paris und Rapperswil, 13. Januar 2015 – Die Hochschule für Technik in Rapperswil und AdaCore haben die Entwicklerversion 0.6 des Open-Source Muen Separation Kernels 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 an der Hochschule für Technik 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 unter 
www.pr-com.de/adacore abgerufen werden.

Über das Muen-Projekt
Das Institut für Internet-Technologien und Anwendungen an der Hochschule für Technik im schweizerischen Rapperswil hat das „Muen Separation Kernel“-Projekt gestartet, um eine Open-Source-Grundlage für Plattformen im Hochsicherheitsbereich zu schaffen. Um eine höchstmögliche Zuverlässigkeit zu erreichen, wurde die Abwesenheit von Laufzeitfehlern formal mittels SPARK 2014 nachgewiesen. Durch eine enge Kooperation mit der secunet Security Networks AG aus Deutschland während der gesamten Design- und Implementierungsphase ist sichergestellt, dass der Muen Separation Kernel alle aktuellen und künftigen Anforderungen komponentenbasierter Plattformen im Hochsicherheitsbereich erfüllt.

Das Git Repository für den Kernel ist verfügbar unter http://git.codelabs.ch/?p=muen.git

Das Muen Development Release 0.6 ist erhältlich unter http://git.codelabs.ch/?p=muen.git;a=snapshot;h=v0.6.0;sf=zip

Der Muen Separation Kernel ist unter der GNU General Public License Version 3 erhältlich.

Über SPARK
SPARK ist eine Softwareentwicklungstechnologie, die speziell auf die Entwicklung von hochzuverlässigen Systemen ausgerichtet ist. SPARK ist sowohl der Name einer Programmiersprache, als auch der Name der Verifikationstools, die formale Methoden anwenden, und in der Lage sind, Fehler noch vor der Ausführung des Programms zu entdecken. Die Sprache und die Tools wurden für die Entwicklung von hochkritischen Anwendungen, bei denen Sicherheit eine wichtige Anforderung ist, entworfen. Dabei bietet SPARK eine tiefe sowie korrekte Analyse des Codes mit einer niedrigen Fehlalarmrate. SPARK wird seit über 25 Jahren in der zivilen und militärischen Luftfahrt, der Eisenbahn, Kryptographie und anderen Domänen erfolgreich eingesetzt. SPARK 2014 ist die neue Generation dieser Softwaretechnologie, mit essentiellen Features wie hybride Verifikation (Kombination formaler Methoden mit traditionellem Test), ausführbaren Verträgen, einem deutlich größeren Sprach-Subset von Ada (zum Beispiel mit generic Units), sowie der Konvergenz mit der Syntax von Ada 2012, die es einfacher macht, SPARK und Ada zu kombinieren. Weitere Informationen finden sich unter www.spark-2014.org/.

Über AdaCore
AdaCore wurde 1994 gegründet und ist der führende Anbieter von kommerziellen Softwarelösungen für Ada, einer modernen Programmiersprache für große, langlebige Anwendungen, bei denen Sicherheit und Verlässlichkeit kritisch sind. Das wichtigste Produkt des Unternehmens ist die Entwicklungsumgebung GNAT Pro, die Online-Support bietet und auf mehr Plattformen als jede andere Ada-Technologie verfügbar ist. AdaCore hat eine große, weltweite Kundenbasis; bitte finden Sie weitere Informationen auf der folgenden Seite: http://www.adacore.com/customers/

Sowohl Ada als auch GNAT Pro werden immer häufiger im High-integrity-Bereich und für sicherheitszertifizierte Anwendungen eingesetzt, so vor allem in sicherheitssensiblen Bereichen wie der Luftfahrt, militärischen Systemen, der Flugverkehrskontrolle, dem Flugverkehrsmanagement, dem Eisenbahnbereich, der medizinischen Produkte oder dem Finanzsektor.

AdaCore hat seinen nordamerikanischen Hauptsitz in New York, der europäische Hauptsitz ist in Paris. Weitere Informationen unter www.adacore.com

Pressekontakte:
AdaCore

Jamie Ayre
press@adacore.com

www.adacore.com
http://twitter.com/AdaCoreCompany

PR-COM
GmbH
Romana Redtenbacher

romana.redtenbacher@pr-com.de
www.pr-com.de

Tel. +49-89-59997-761