|[December 10, 2013]
Muen Separation Kernel Lays Open Source Foundation for High-Assurance Software Components
NEW YORK & PARIS & RAPPERSWIL, Switzerland --(Business Wire)--
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 (News - Alert) 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
The name "Muen" is a Japanese term that means "unrelated" or "without
relaton", 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
The Institute for Internet Technologies and Applications (ITA (News - Alert)) 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
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.
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
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
[ Back To Technology News's Homepage ]