Two students of the University of Applied Sciences Rapperswil in Switzerland, Reto Buerki and Adrian-Ken Rueegsegger, have written a small separation kernel in SPARK (less than 3000 lines of SPARK, with an additional 300 lines of Assembly) exploiting the hardware virtualization technology available in modern INTEL chips. Quite a milestone!

To present the impact of this work, I need to talk about the multilevel workstation R&D project at Secunet. Secunet (short for secunet Security Networks AG) is a small German company developing secure IT solutions for the German government and military. They have a well-known multilevel workstation product called SINA based on a hardened linux kernel. The SINA products are used for example by all German embassies around the world to send classified information. The SINA workstation allows German government employees to access different networks (say, the Internet on one side, and a confidential intranet on the other side) on the same machine, switching from one to the other with a few key strokes.

Since 2010, Secunet is investigating the use of SPARK to build the next version of SINA, to ensure complete absence of run-time errors in the trusted computing base of the system (thus fully preventing security attacks based on buffer overflows and the like), and to prove high-level security properties of the system (using a bridge from SPARK to the Isabelle proof assistant that they developed).

They have truly done an amazing job, not implementing only the core workstation in SPARK, including IPsec, but also the drivers for the keyboard and graphics card! All in a system that is 180 times smaller than a minimal equivalent linux solution (see slide 20 in the presentation I mention above), hence can be inspected by experts with a much higher degree of confidence. Stefan Berghofer presented at the SPARK User Group in 2012 how they verified formally a big number library and an ASN.1 parser (a well-known source of vulnerabilities in many high integrity systems) using SPARK and Isabelle.

Still, the larger part of the system is implemented in C, without formal guarantees regarding the absence of run-time errors, as the multilevel workstation is based on the LynxSecure separation kernel commercialized by LynuxWorks. It is this separation kernel that the much smaller Muen separation kernel in SPARK is meant to replace.

Now, why an open-source separation kernel? Their view is that a separation kernel should be a commodity that multiple parties can contribute to, so that each one can work on their core business. Which, for Secunet, is providing German government and military with ultra secure information systems, and that requires much more than a separation kernel. I encourage you to look at their webpage, which points in particular to the Git repository for the source of Muen, and the associated public mailing-list.