Title:		A Secure Microkernel

Author:		Philip Geoffrey Derrin

		School of Computer Science and Engineering,
		The University of New South Wales, Sydney 2052, Australia,
		philipd@cse.unsw.edu.au

Abstract:

Specification of a new kernel API is a challenging task. If the specification
is initially developed at an abstract level, it is easy to overlook important
implementation issues; on the other hand, writing a real kernel to test a
specification involves low-level programming and debugging, which takes a lot
of time and effort and which may be difficult to formally verify. This project
is an attempt to develop a technique for prototyping a kernel in a high-level
functional language, with the goal of being able to rapidly evaluate design
decisions and specify the behaviour of the kernel more precisely than an
abstract model.