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