Microhypervisor Verification: Possible Approaches and Relevant Properties
Hendrik Tews
Radboud Universiteit Nijmegen
<H.Tews@cs.ru.nl>
The SoS-group at the Radbout Universiteit Nijmegen participates in the Robin project. The goal of this project is to develop a minimal trusted computing base for virtualizing (multiple instances of different) distrusted legacy operating systems in a secure way. With the resulting system it shall be possible to use, for instance, Word on Microsoft Windows for composing classified documents in a secure way. Thereby it is not necessary to trust Windows in any way, the copy used could even be compromised by an attacker already.

In the presentation I give an overview over the Nizza architecture that is used in the Robin project. I further elaborate on our task: To develop a verification approach for the underlying microhypervisor for relevant security properties.

I was born on 22nd of August 1969 in Leipzig, Germany. I studied theoretical computer science in Dresden and Edinburgh and got a Diploma (Master) in Computer science in 1995. From 1996 I worked on various research positions at the University of Dresden and the University of Nijmegen under the supervision of Horst Reichel and Bart Jacobs. I obtained my PhD in 2002 on "Coalgebraic Methods for Object-Oriented Specification" with summa cum laude. I participated in the LOOP and the VFiasco projects and worked in the fields of Coalgebra and software verification. I am currently working on operating system kernel verification in the Robin project at Radboud University Nijmegen.


Last modified: Wed, 28 Feb 2007 16:14:06 +0100