Muen Separation Kernel upgrades to SPARK 2014 for formal verification

The Institute for Internet Technologies and Applications at the University of Applied Sciences in Rapperswil (Switzerland) and AdaCore have 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 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 Muen Separation Kernel is available under the GNU General Public License version 3.

Git repository for the Kernel

Muen development release 0.6

More information

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.