Thesis

Thesis Topic Details

Topic ID:
 1232
Title:
 Supporting a Haskell-based OS model on native hardware
Supervisor:
 Kevin Elphinstone
Research Area:
 Operating Systems, Programming Languages
Associated Staff
Assessor:
 Manuel Chakravarty
Topic Details
Status:
 Active
Type:
 R & D
Programs:
 CS CE BIOM BINF SE
Group Suitable:
 No
Industrial:
 No
Pre-requisites:
 Good understanding of OS and programming language implementation
Description:
 Modern functional languages, such as Haskell, are becoming
increasingly popular in application domains that require rapid
development coupled with high safety and security demands. One
particularly interesting such application domain is systems software
for embedded systems, such as mobile phones. In this context, we have
developed an executable specification of the seL4 microkernel, which
improves existing second generation microkernels. In conjunction with
an instruction level simulator, the executable kernel specification is
a functional, if inefficient, implementation of the new microkernel.

We are working on a verified implementation of the specification in a
low-level language for production use. However, this is a very
resource-intensive endeavour. Hence, we are investigating an
alternative implementation strategy where we run the Haskell code on
bare metal - i.e., the Haskell implementation of the microkernel
boots on standard hardware without any other operating system in
between. This is a challenging project as it requires the adaptation
of the Haskell runtime system to run without operating system support.
Such a bare metal Haskell implementation would also be useful for
other projects, such as trusted web service in high confidentiality
environments and is the focus of this summer project.
Comments:
 --
Past Student Reports
 
 No Reports Available. Contact the supervisor for more information.

Check out all available reports in the CSE Thesis Report Library.

NOTE: only current CSE students can login to view and select reports to download.