A secure microkernel
Authors
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} }