Select Language

Muen Separation Kernel Lays Open Source Foundation for High-Assurance Software Components

Swiss university develops formally verified Open Source kernel using SPARK language and AdaCore GNAT tools

NEW YORK, PARIS and RAPPERSWIL, Switzerland, December 10, 2013 – The Institute for Internet Technologies and Applications at the University of Applied Science in Rapperswil (Switzerland) and AdaCore today announced a significant expansion of the Open Source software model into the domain of high-assurance systems with the preview release of the Muen Separation Kernel. 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. Using AdaCore’s GNAT development environment to build their software, the team was able to achieve high productivity.

The public preview release of the Muen Separation Kernel in Autumn 2013 is the first major milestone for the ongoing Muen project, whose goal is to produce a trustworthy Open Source foundation for component-based high-assurance systems. This is an area of high potential growth, and indeed Open Source software promises to play an increasing role in the development of safe and secure systems.

“It’s an exciting occasion,” said Cyrille Comar, Managing Director of AdaCore, “for AdaCore to be participating in the birth of an Open Source community around a separation kernel that can be verified formally using Open Source tools, such as those we develop with our partner Altran. Since this type of software is expensive to produce, community-based development offers an attractive cost-sharing model for the main stakeholders. And openness in the code, and in its security-related verification data, is a key element of the trust that is required for secure software.”

The name “Muen” is a Japanese term that means “unrelated” or “without relation”, reflecting the main objective for a separation kernel: ensuring the isolation between components. Since a separation kernel enforces isolation, resource control and data flow in a component-based system, any errors in the kernel would be fatal to the security of all components. To prevent such a calamity, the Muen Kernel was written in SPARK, an Ada-based language with a long and successful track record in developing high-assurance systems. The SPARK toolset enabled the Muen team to perform static formal verification of the Kernel and to prove the absence of all run-time errors. In the future, functional correctness proofs will be added to the Kernel by using SPARK in conjunction with an interactive theorem prover.

The Muen developers used SPARK with a zero-footprint runtime – a mode where no runtime environment, and only a minimum of supporting code, is required. This setup is ideal for critical low-level programming, since no unnecessary libraries are introduced into the system.

“The Open Source license of the Muen Separation Kernel, combined with the SPARK and GNAT tools, makes it possible for the community to use Muen as a trusted core component in high-assurance systems,” said Prof. Dr. Andreas Steffen, Head of the Institute for Internet Technologies and Applications. “Anyone can inspect and compile the source code and reproduce the formal proofs at any time.”

About the Muen Project: “Trustworthy by Design -- Correct by Construction”
The Institute for Internet Technologies and Applications (ITA) at the University of Applied Science Rapperswil (HSR) in Switzerland started the Muen Separation Kernel project to create an Open Source foundation for high-assurance platforms. To achieve trustworthiness exceeding any other Open Source kernel or hypervisor, the absence of runtime errors has been formally proven using the SPARK language and toolset. 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.
A snapshot of the Muen repository can be downloaded here.
The Muen Separation Kernel is available under the GNU General Public License version 3.

About SPARK
The SPARK technology comprises the foremost language, toolset and design discipline for the engineering of high-assurance software. It combines Altran's SPARK language and verification tools with AdaCore’s GNAT Programming Studio development environment. SPARK has an enviable track-record in many industry sectors, such as aerospace, rail, nuclear and security, and has been used to meet or exceed all known industry guidance and standards at the highest assurance levels. SPARK prevents, detects and eliminates defects early in the life-cycle as the source code is developed, and it is the only modern imperative programming language created with the provision of sound static verification as the primary design goal. Through simplification of the language and the addition of contracts, SPARK also offers verification that is fast, deep, constructive and exhibits a remarkably low false-alarm rate. No other programming language or verification tools can offer this combination.

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/home/company/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

Jessie Glockner
Rainier Communications (for AdaCore)
Tel: 508-475-0025 x140
adacore@rainierco.com
http://twitter.com/JessieGlockner

Mit SPARK erstellter Muen Kernel legt Open-Source- Fundament für Software im Hochsicherheitsbereich

Paris und Rapperswil, 12. Dezember 2013 – Die Hochschule für Technik im schweizerischen Rapperswil hat den formal verifizierten Muen Open- Source- Kernel mit der Ada-basierten Programmiersprache SPARK und dem AdaCore GNAT Ada Toolset erstellt.

Das Institut für Internet-Technologien und Anwendungen an der Hochschule für Technik im schweizerischen Rapperswil und AdaCore präsentieren mit dem Preview Release des Muen Separation Kernels eine bedeutsame Erweiterung des Open-Source-Modells für Systeme im Hochsicherheitsbereich. 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.

Das Public Preview Release des Muen Separation Kernels ist ein erster wichtiger Meilenstein für das Projekt, dessen Ziel es ist, ein zuverlässiges Open-Source-Fundament für komponentenbasierte Systeme im Hochsicherheitsbereich zu legen. In diesem Bereich mit viel Wachstumspotenzial spielt Open-Source-Software bei der Entwicklung hochsicherer Systeme eine immer wichtigere Rolle.

„Für AdaCore ist es sehr spannend, bei der Entstehung einer Open Source Community rund um den Muen Separation Kernel dabei zu sein. Das ist vor allem deshalb interessant, weil der Kernel unter anderem mit Open-Source-Tools, die wir mit unserem Partner Altran entwickelt haben, verifiziert wird“, sagt Cyrille Comar, Managing Director bei AdaCore. „Da die Herstellung einer solchen hochsicherheitskritischen Software teuer ist, ergibt sich durch eine Community-basierte Entwicklung die Möglichkeit, Kosten unter den Beteiligten zu splitten.

Der offene Quellcode und die sicherheitsrelevanten Prüfungen sind entscheidend für das Vertrauen in sichere Software.“

Der japanische Begriff „Muen“ bedeutet „unabhängig“ oder „ohne Beziehung untereinander“ und steht für das wichtigste Ziel des Separation Kernels: die klare 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, wurde der Muen Kernel mit der Ada-basierten Programmiersprache SPARK erstellt. Sie wird seit vielen Jahren sehr erfolgreich zur Entwicklung von Systemen im Hochsicherheitsbereich eingesetzt. Das Muen-Team nutzte das SPARK Toolset zur statischen Überprüfung des Kernels und zur Prüfung der Abwesenheit von Laufzeitfehlern. In Zukunft soll 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 ideal, da das System keine unnötigen Libraries aufweist.

„Die Open-Source-Lizenz des Muen Separation Kernels, kombiniert mit den SPARK- und GNAT-Tools, ermöglicht es der Community, Muen als zuverlässiges Herzstück für Systeme im Hochsicherheitsbereich einzusetzen“, sagt Prof. Dr. Andreas Steffen, Leiter des Instituts für Internet-Technologien und Anwendungen. „Jeder kann den Source Code prüfen, kompilieren und die formalen Nachweise jederzeit reproduzieren.“

Über das Projekt: Muen "Trustworthy by Design -- Correct by Construction"
Das Institut für Internet-Technologien und Anwendungen an der Hochschule für Technik im schweizerischen Rapperswil startete das „Muen Separation Kernel“-Projekt mit dem Ziel, eine Open-Source-Grundlage für Plattformen im Hochsicherheitsbereich zu schaffen. Um eine höchstmögliche Zuverlässigkeit zu erreichen, und damit jeden anderen Open- Source- Kernel oder Hypervisor zu übertreffen, wurde die Laufzeitfehler-Freiheit formal mit der SPARK-Sprache und dem SPARK-Toolset 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 gibt es unter http://git.codelabs.ch/?p=muen.git

Ein Snapshot des Muen Repositories steht zum Download bereit unter http://git.codelabs.ch/?
p=muen.git;a=snapshot;h=master;sf=zip
.

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

Über SPARK
Die SPARK-Technologie umfasst die gleichnamige Programmiersprache, das Toolset und die Design-Disziplin für die Entwicklung von Software im Hochsicherheitsbereich. Sie verbindet die Sprache und Verifikations-Tools von Altrans SPARK und Verifikations-Tools mit dem GNAT Programming Studio von AdaCore. SPARK verfügt über eine lange Erfolgsgeschichte in vielen Branchen wie Luft- und Raumfahrt, Schienen- und Transportwesen sowie nukleare Sicherheit und wird eingesetzt, um alle bekannten Sicherheitsvorgaben und Standards auf höchster Stufe umzusetzen. SPARK verhindert, erkennt und eliminiert Fehler bereits bei der Erstellung von Source Code – und damit sehr frühzeitig im Lebenszyklus. Zugleich ist SPARK die einzige imperative Programmiersprache, die eine statische Verifikation als primäres Designziel verfolgt. Durch eine Vereinfachung der Sprache und ergänzt um Verträge ermöglicht SPARK eine statische Überprüfung, die hinsichtlich ihrer Solidität konkurrenzlos ist – beispielsweise keine ”false negatives” –, sowie eine niedrige Fehler-Alarm-Rate und Effizienz.

Ü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. Das SPARK Pro Toolset, das ebenfalls von AdaCore erhältlich ist, eignet sich besonders für den Einsatz in diesem Umfeld.

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