The Muen Separation Kernel
Robert Dorn
Senior Consultant at secunet Security Networks AG
Adrian-Ken Rueegsegger
Researcher at the University of Applied Sciences Rapperswil (HSR)
Reto Buerki
Researcher at the University of Applied Sciences Rapperswil (HSR)
Writing large error-free software is extremely challenging or even infeasible. In order to be able to assure critical security properties it is therefore necessary to decompose the system into small security critical subjects whose correctness has to be shown and other large uncritical parts which cannot endanger security. A separation kernel can be used to assure the independent execution of multiple subjects and the enforcement of pre-defined communication channels between subjects. The correctness of the separation kernel is therefore essential for overall security.
In this talk we describe the design and implementation of the Muen separation kernel which uses the SPARK language to enable light-weight formal methods for assurance. Besides a discussion of x86 virtualization, system integration, as well as present and planned verification we demonstrate how Muen enables the construction of high security systems on x86 hardware.
About Robert Dorn
Robert Dorn is responsible for designing and building high security software at secunet AG. Since 2005 he influenced and lead research and development projects for the protection of highly classified data.Robert holds a degree as Diplom Informatiker from the University of Erlangen-Nürnberg. His domains of expertise include design of secure systems, platform security, separation kernels and component verification using formal methods (SPARK, Isabelle).About Adrian-Ken Rueegsegger
Adrian-Ken Rueegsegger is a researcher at the University of Applied Sciences Rapperswil (HSR) in Switzerland and is one of the core developers of the Muen Separation Kernel. He holds a degree as MSc in Engineering from HSR. He has been working in the field of IT-Security for more than seven years. His main areas of interest are network and system-level security, as well as designing and building secure systems.About Reto Buerki
Reto Buerki holds an MSc in Engineering from the University of Applied Sciences Rapperswil (HSR) in Switzerland. Since 2008 he has been developing secure software in Ada and also uses SPARK to further increase assurance in the code.Reto works as a researcher at HSR where he is developing secure systems.His current focus is the development of the Muen Separation Kernel as a foundation for component-based high-assurance systems.Sponsored by
