Skip to main content

A secure microkernel


Philip Geoffrey Derrin

NICTA, Sydney, Australia
UNSW, Australia


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.

BibTeX Entry

    month            = jun,
    school           = {School of Computer Science and Engineering},
    keywords         = {sel4 capability haskell},
    note             = {Available from publications page at \url{}},
    author           = {Philip Geoffrey Derrin},
    title            = {A Secure Microkernel},
    address          = {Sydney, Australia},
    year             = {2005}