Trustworthy Systems

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