Welcome!

Eclipse Authors: Pat Romanski, Elizabeth White, Liz McMillan, David H Deans, JP Morgenthal

News Feed Item

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

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

More Stories By Business Wire

Copyright © 2009 Business Wire. All rights reserved. Republication or redistribution of Business Wire content is expressly prohibited without the prior written consent of Business Wire. Business Wire shall not be liable for any errors or delays in the content, or for any actions taken in reliance thereon.

IoT & Smart Cities Stories
The platform combines the strengths of Singtel's extensive, intelligent network capabilities with Microsoft's cloud expertise to create a unique solution that sets new standards for IoT applications," said Mr Diomedes Kastanis, Head of IoT at Singtel. "Our solution provides speed, transparency and flexibility, paving the way for a more pervasive use of IoT to accelerate enterprises' digitalisation efforts. AI-powered intelligent connectivity over Microsoft Azure will be the fastest connected pat...
There are many examples of disruption in consumer space – Uber disrupting the cab industry, Airbnb disrupting the hospitality industry and so on; but have you wondered who is disrupting support and operations? AISERA helps make businesses and customers successful by offering consumer-like user experience for support and operations. We have built the world’s first AI-driven IT / HR / Cloud / Customer Support and Operations solution.
Codete accelerates their clients growth through technological expertise and experience. Codite team works with organizations to meet the challenges that digitalization presents. Their clients include digital start-ups as well as established enterprises in the IT industry. To stay competitive in a highly innovative IT industry, strong R&D departments and bold spin-off initiatives is a must. Codete Data Science and Software Architects teams help corporate clients to stay up to date with the mod...
At CloudEXPO Silicon Valley, June 24-26, 2019, Digital Transformation (DX) is a major focus with expanded DevOpsSUMMIT and FinTechEXPO programs within the DXWorldEXPO agenda. Successful transformation requires a laser focus on being data-driven and on using all the tools available that enable transformation if they plan to survive over the long term. A total of 88% of Fortune 500 companies from a generation ago are now out of business. Only 12% still survive. Similar percentages are found throug...
Druva is the global leader in Cloud Data Protection and Management, delivering the industry's first data management-as-a-service solution that aggregates data from endpoints, servers and cloud applications and leverages the public cloud to offer a single pane of glass to enable data protection, governance and intelligence-dramatically increasing the availability and visibility of business critical information, while reducing the risk, cost and complexity of managing and protecting it. Druva's...
BMC has unmatched experience in IT management, supporting 92 of the Forbes Global 100, and earning recognition as an ITSM Gartner Magic Quadrant Leader for five years running. Our solutions offer speed, agility, and efficiency to tackle business challenges in the areas of service management, automation, operations, and the mainframe.
The Jevons Paradox suggests that when technological advances increase efficiency of a resource, it results in an overall increase in consumption. Writing on the increased use of coal as a result of technological improvements, 19th-century economist William Stanley Jevons found that these improvements led to the development of new ways to utilize coal. In his session at 19th Cloud Expo, Mark Thiele, Chief Strategy Officer for Apcera, compared the Jevons Paradox to modern-day enterprise IT, examin...
With 10 simultaneous tracks, keynotes, general sessions and targeted breakout classes, @CloudEXPO and DXWorldEXPO are two of the most important technology events of the year. Since its launch over eight years ago, @CloudEXPO and DXWorldEXPO have presented a rock star faculty as well as showcased hundreds of sponsors and exhibitors! In this blog post, we provide 7 tips on how, as part of our world-class faculty, you can deliver one of the most popular sessions at our events. But before reading...
DSR is a supplier of project management, consultancy services and IT solutions that increase effectiveness of a company's operations in the production sector. The company combines in-depth knowledge of international companies with expert knowledge utilising IT tools that support manufacturing and distribution processes. DSR ensures optimization and integration of internal processes which is necessary for companies to grow rapidly. The rapid growth is possible thanks, to specialized services an...
At CloudEXPO Silicon Valley, June 24-26, 2019, Digital Transformation (DX) is a major focus with expanded DevOpsSUMMIT and FinTechEXPO programs within the DXWorldEXPO agenda. Successful transformation requires a laser focus on being data-driven and on using all the tools available that enable transformation if they plan to survive over the long term. A total of 88% of Fortune 500 companies from a generation ago are now out of business. Only 12% still survive. Similar percentages are found throug...