Select Language

New Release of Muen Separation Kernel Upgrades to SPARK 2014 for Formal Verification

Successful transition to SPARK 2014 marks major milestone for Swiss university’s high-security kernel

NEW YORK, PARIS and RAPPERSWIL, Switzerland, January 12, 2015 – The Institute for Internet Technologies and Applications at the University of Applied Sciences in Rapperswil (Switzerland) and AdaCore today announced the development release of the Open Source Muen Separation Kernel version 0.6, completing the migration to the SPARK 2014 technology. The Muen Kernel enforces a strict and robust isolation of components to shield security-critical functions from vulnerable software running on the same physical system. To achieve the necessary level of trustworthiness, the Muen team used the SPARK language and toolset to formally prove the absence of run-time errors. The AdaCore and Muen teams cooperated closely in the work on version 0.6, ensuring a successful upgrade of the software to SPARK 2014. The kernel development at the university is sponsored by secunet Security Networks AG in Germany, who are using Muen in their product development.

SPARK 2014 represents a major enhancement to the SPARK language, enlarging the available set of features as well as incorporating the standard Ada 2012 syntax and semantics for contract-based programming. Compatibility with Ada 2012 allows a novel and productive approach to software verification, supporting both formal methods (through static enforcement of contracts by the new GNATprove technology) and traditional testing-based techniques (through run-time checks). It also makes it easier to transition from Ada to SPARK, since the specialized annotation syntax found in earlier version of the SPARK language is no longer needed. SPARK 2014 support is accessible from AdaCore’s GNAT Programming Studio (GPS) and GNATbench integrated development environments (IDE), for users of AdaCore’s SPARK Pro toolset.

The Muen team exploited SPARK 2014’s combined verification approach, complementing their use of formal methods with the application of GNATtest as the unit testing framework for the software that assembles a bootable image from a system policy. GNATtest automatically generates the test harness and test stubs, thereby saving the effort previously required to produce the large amounts of boilerplate code that are needed. And looking ahead, the improved modeling of external interfaces in SPARK 2014, combined with upcoming features such as “ghost variables” (which can capture complex invariants and hidden state), lay the groundwork for future formal verification efforts on the kernel code.

Since the last public preview release in autumn 2013, the Muen platform itself has progressed. Besides the support for Linux virtual machines, PCI-Device passthrough has been implemented using the Intel VT-d DMA and interrupt remapping mechanisms. Furthermore, the addition of a modular system description language enables users to integrate complex component-based systems running on top of the Muen kernel.

“The Muen separation kernel provides a strong platform for high security systems which can securely leverage the functionality of existing untrusted components,” said Dr. Kai Martius, CTO of secunet Security Networks AG. “SPARK 2014 enables us to formally verify isolation and security properties of Muen and key components in a cost-efficient way.”

“By adapting so quickly to the new SPARK 2014 capabilities, the Muen team has corroborated our hypothesis that this new version of the language and associated technology is both simpler to grasp and at least as powerful as the old version,” said Cyrille Comar, Managing Director of AdaCore. “It shows that the new product also serves the need of security-oriented developers who tend to push the static verifications as far as possible, including manual proofs, when necessary.”

About the Muen Project
The Institute for Internet Technologies and Applications (ITA) at the University of Applied Sciences Rapperswil (HSR) in Switzerland started the Muen Separation Kernel project to create an Open Source foundation for high-assurance platforms. To achieve the high level of trustworthiness required for security critical systems the design of the Muen kernel strictly avoids unnecessary complexity in trusted code for which the absence of runtime errors is proven. Through close cooperation with secunet Security Networks AG in Germany during the whole design and implementation process, the Muen Separation Kernel is assured of meeting the requirements of existing and future component-based high-security platforms.

The Git repository for the Kernel is available here.
The Muen development release 0.6 can be downloaded here.
The Muen Separation Kernel is available under the GNU General Public License version 3.

About SPARK
SPARK is a software development technology specifically designed for engineering high-reliability systems. It combines a programming language and a verification toolset to reduce the effort in developing ultra-low defect software in critical applications, for example where safety and/or security are key requirements. SPARK offers verification that is sound and deep and exhibits a remarkably low false-alarm rate. It has a solid industrial track record with a 25+ year history of successful usage worldwide in a range of industrial applications including civil and military avionics, railway signaling, cryptography, and cross-domain solutions. SPARK 2014 is the next generation of this leading software technology, offering key benefits such as support for hybrid verification (combining formal methods with traditional testing), executable contracts, a larger Ada language subset (for example including generic units), and convergence with Ada 2012 syntax (making it easier to combine Ada and SPARK components). For further information please visit www.spark-2014.org/.

About AdaCore

Founded in 1994, AdaCore is the leading provider of commercial Open Source software solutions for Ada, a state-of-the-art programming language designed for large, long-lived applications where safety, security, and reliability are critical. AdaCore's flagship product is the open source GNAT Pro development environment, which comes with expert on-line support and is available on more platforms than any other Ada technology. AdaCore has an extensive world-wide customer base; see http://www.adacore.com/customers/ for further information.

Ada and GNAT Pro see a growing usage in high-integrity and safety-certified applications, including space-based systems, commercial aircraft avionics, military systems, air traffic management/control, railroad systems, and medical devices, and in security-sensitive domains, such as financial services. The SPARK Pro toolset, available from AdaCore, is especially useful in such contexts.

AdaCore has North American headquarters in New York and European headquarters in Paris. www.adacore.com

Press Contacts

Jamie Ayre

AdaCore

press@adacore.com

http://twitter.com/AdaCoreCompany

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