HSR University of Applied Sciences Rapperswil Switzerland
The Muen Separation Kernel
Trustworthy by Design -- Correct by Construction
Today, even vital infrastructures like power grids, classified government networks or company research sites tend to be connected to the Internet to take advantage of remote management and cloud services. Traditional approaches to securing these infrastructures rely on a strict isolation of critical systems from untrusted networks. In the presence of critical networked environments, other strategies are required to prevent unauthorized access which may be gained through the exploitation of errors in the complex software stacks that are used. One solution are component-based high-assurance platforms where untrusted software components are strictly isolated from security-critical functions on one single physical system.
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 a trustworthiness exceeding any other Open Source kernel or hypervisor, the absence of runtime-errors is formally proven using AdaCore's and Altran's SPARK language and toolset. A close cooperation with secunet Security Networks AG in Germany throughout the whole design and implementation process ensures that the Muen Separation Kernel meets the requirements of existing and future component-based high-security platforms.
The Separation Kernel Concept
Every large and complex piece of software, like operating systems, document viewers or web browsers, contains errors which can be exploited using seemingly harmless programs, documents or web pages. It is almost certain that these kinds of programs will never be error-free, as the problems they are supposed to solve are inherently complex and force a high complexity onto the software. No matter which development process is used, error propability closely corresponds to the size of a program. The problem is compounded by the fact that the market forces vendors to release software earlier, with plenty new features and at lowest costs. The thriving commercial market of zero-day exploits for widespread software proves that this is a real threat exploitable by any adversary with sufficient time or money.
Obviously, a more effective approach for critical systems is necessary! Instead of trying to make existing complex software suitable for critical systems, it is much more realistic to identify all functions necessary to maintain security for a given set of security objectives. Security-critical functions can then be implemented in a trustworthy fashion and run as isolated components interacting with untrusted software. In such a component-based architecture, e.g. the encryption of all information sent over the network or stored on disk can be enforced, even in the presence of a vulnerable legacy operating system running in a virtual machine.
To shield against vulnerable software effectively, a strict and robust isolation of components is essential. This is where the Separation Kernel comes into play: It enables the concept of secure component-based systems by isolating virtual machines, other untrusted software and trusted components running on the same physical system. It is important to note that the Separation Kernel is a very important but not a sufficient prerequisite for building secure component-based systems. A suitable security architecture must exist and the trusted components need to be developed with the same rigor as the Separation Kernel itself.
Tools and Methodology
As the Separation Kernel enforces isolation, resource control and data flow in a component-based system, errors in the kernel are fatal to the security of all other components. Muen is written in the high-level language SPARK, which turned out to be a perfect choice for the implementation of a high-assurance operating system kernel and critical services. Even when dealing with low-level hardware details the code stays readable and comprehensible. SPARK allows for a precise and clean modeling of the hardware and the safest possible use of inline-assembly.
The SPARK toolset provides static formal verification for the Muen kernel and proves the absence of run-time errors like buffer overflows and range violations. All of the proof obligations in the kernel could be discharged automatically using the SPARK Simplifier. In the future, functional correctness proofs will be added to the kernel by using SPARK in conjunction with an interactive theorem prover.
We use 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, as no unnecessary libraries are introduced into the system.
The Muen Project
The name Muen is a Japanese term that translates to "unrelated" or "without relation" which makes for a nice allegory of the main objective of a Separation Kernel. The goal of the Muen project is the development of a trustworthy open-source foundation for component-based high-assurance systems.
In December 2013 the first major project milestone was completed successfully with the public preview release of the Muen Separation Kernel under the GNU General Public License version 3. Even though the kernel is not considered ready for production yet, all fundamental functionality of a Separation Kernel has been implemented. The SPARK implementation only took 8 person months, including the proof of absence of runtime errors.
The Muen kernel runs on the Intel x86/64 architecture and uses hardware-assisted virtualization (VT-x) as the fundamental separation mechanism. The following major features have been realized in the first milestone:
- Support for 64-bit native and 32-bit VM subjects
- Xv6 teaching OS as an example VM
- Inter-component event mechanism
- Static resource assignment according to system policy
- Fixed cyclic hard realtime scheduler
- Multicore (SMP) support
- Nested paging (EPT) and memory typing (PAT)
- Minimal Zero-Footprint Run-Time (RTS)
- A demo system involving an Xv6 VM and a native crypto component
The kernel documentation is available on the website as well as in the Muen source code repository.
The short-term objective of the project is to enable the execution of Linux virtual machines and the secure virtualization of hardware devices for the next milestone in Q1 2014. This will enable us to support more realistic scenarios like secunet's SINA Multilevel Platform, involving a variety of interacting untrusted virtual machines and trustworthy security-critical components.
Long-term goals of the project include further analysis and mitigation of inter-component covert and side channels, dynamic resource management, functional correctness and support for fully-virtualized Windows VMs. Future versions of the Muen Separation Kernel will also take advantage of the new capabilities and tools of the upcoming SPARK 2014 language.
The Muen distribution contains the following:
- Source code of the Muen Separation Kernel
- Tools to create system images
- Scripts for easy emulation and system image creation
- Configuration for an example system
The Git repository is available under http://git.codelabs.ch/?p=muen.git. A snapshot of the Muen repository can be downloaded from here.
Muen - An x86/64 Separation Kernel for High Assurance
Architecting High-Assurance Systems
Component-based system use-case: TKM
SPARK Product Page