Applications for summer research in Trustworthy Systems for the topics below can be made through
Supervisor: Gernot Heiser
Abstract: The seL4 microkernel is known on the one hand for its correctness and security proofs, on the other hand for its unbeaten performance. Performance optimisations have so far targeted the critical IPC operation, and to a lesser degree signalling notification objects. While interrupt and exception handling are mapped onto notifications and IPC, respectively, they have not been optimised to the same degree.
This project is to analyse interrupt (IRQ) delivery performance and compare it to optimised notification signalling. Using the performance monitoring unit (PMU) and tracing in a simulator (QEMU), the student will analyse overheads and write or improve an IRQ fast path.
Expected outcomes:
Supervisor: Kevin Elphinstone
Abstract:
The seL4 microkernel is known not only for its comprehensive formal verification story but also for being the benchmark for microkernel IPC performance. However, for the cost of protection in client-server interactions in a secure OS, the code required to marshal parameters to the IPC system call is also a factor. This project is to evaluate the performance cost of these stubs and the potential for the compiler optimising them away on bare seL4. In a second step, this analysis is to be extended to the interfaces required for the CAmkES framework. If there is time, look at the potential for generating efficient stubs from an interface generator.
Expected outcomes:
Abstract: seL4 IPC operations are highly optimised for hot-cache (best case) but far less so for bad/worst-case. This project is to first determine present cold-cache performance by extending the sel4bench suite for cold caches. It is then to analyse and understand what limits present performance and is to improve it, by ensuring cache-friendly datastructure layout and other optimisations. The emphasis will be on the IPC, interrupt and exception ast paths, optionally looking at other parts of the code as well (especially slow paths).
Novelty:seL4 kernel with much improved cold-cache performance, prevention of cold-cache performance regressions.
Supervisor: Gernot Heiser, Zoltan Kocsis
Abstract:
seL4 is the world's first operating system (OS) kernel with a proof of implementation correctness, followed by proofs of security enforcement; it is at the same time the benchmark for microkernel performance. The seL4 Core Platform (sCP) is a minimal seL4-based OS aimed at embedded and cyberphysical systems. The sCP is intentionally kept lean and simple, to minimise overheads while ensuring correct use of seL4 mechanisms.
Its simplicity should enable verification of the sCP, extending seL4's assurance to the complete OS. This project is to investigate the use of SMT solvers to automatically verify the sCP implementation. The main challenges will be to formally specify the sCP API, and tweak the SMT problem, as well as the sCP implementation for verification to succeed.
Expected outcomes: