Thesis Topic Details

Topic ID:
3824
Title:
Virtualising the seL4 ABI
Supervisor:
Gernot Heiser
Research Area:
Operating Systems, Security
Associated Staff
Assessor:
Kevin Elphinstone
Topic Details
Status:
Active
Type:
R & D
Programs:
CS CE SE
Group Suitable:
Industrial:
Pre-requisites:
COMP9242 Advanced Operating Systems
Description:
Capabilities are opaque object references with implied access rights. A capability system should allow transparent interposition, eg for security monitoring.

In a capability-based operating system, this should allow complete virtualisation of the system-call interface. This project is to put seL4, the world's most trustworthy operating system, to the test: Is seL4 truly virtualisable? I.e. can an arbitrary program written to run natively on seL4 run correctly in a virtualised envorinment where all system calls are intercepted by a security monitor? If so, what is the inherent cost of virtualisation?

The simplese proof of virtualisability is to construct a minimal wrapper around a user process that intercepts all capabiltiy transfers in and out of the process and replaces them by endpoint capabilitie. Those endpoints are invoked by the process as if they represented kernel objects, but instead send a message to the wrapper which then invokes the actual operation on behalf of the kernel. The virtualisation is complete if the wrapper can proxy all such invokations without any knowledge of the operation the client process' intended. Validate this by running the seL4 regression test suite as the client process.

The next step is to show that the interception can be done efficiently. The only truly performance-relevant operations in seL4 are fastpath IPC and notificationsand the related operations of interrupt and exception handling that are mapped to IPC and notifications. The goal is to demonstrate that these operations can proceed at full speed, by removing the intercept after the first invokation.

An advanced (and even more powerful) test will be to demonstrate a persistent version of seL4, which presents itself as a very large physical address space that gets transparently paged to disk and where all user state survives system reboot. Demonstrating this should be a publishable result.
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.