Thesis Topic Details
Topic ID: |
1447 | |
Title: |
A Secure Bootstrapper for the seL4 | |
Supervisor: |
Kevin Elphinstone | |
Research Area: |
Embedded Systems, Operating Systems | |
| Associated Staff | ||
|---|---|---|
Assessor: |
||
| Topic Details | ||
Status: |
Active | |
Type: |
R & D | |
Programs: |
CS CE SE | |
Group Suitable: |
No | |
Industrial: |
No | |
Pre-requisites: |
-- | |
Description: |
The seL4 microkernel is a high assurance microkernel capable of acting as a seperation kernel when it and the encompassing system is instantiated correctly. The goal of this thesis is to develop a simple component model that can specific an initial system state - i.e. the servers and applications that will run on the microkernel. THe component model is then used to generate the boot strapping code to instantiate the system with the specified seperation guarantees. The project may involve evaluating the existing CAMKES framework for the component model, and looking at formal models and guarantees for both the component model, and the generation of the boot strapper. |
|
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. |
||