A secure microkernel
Authors
Philip Geoffrey Derrin
School of Computer Science and Engineering
UNSW,
Sydney 2052, 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,
address = {Sydney, Australia},
author = {Philip Geoffrey Derrin},
keywords = {sel4 capability haskell},
month = jun,
note = {Available from publications page at \url{http://ts.data61.csiro.au/}},
paperUrl = {https://trustworthy.systems/publications/theses_public/05/Derrin%3Abe.pdf},
school = {School of Computer Science and Engineering},
title = {A Secure Microkernel},
year = {2005}
}
Download