Skip to main content
CSIRO Logo Data 61 logo

A secure microkernel

Authors

Philip Geoffrey Derrin

NICTA, Sydney, Australia
UNSW, Australia

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.

BibTeX Entry

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

Download