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:
Supervisor: Kevin Elphinstone, Gernot Heiser
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. Its recent MCS variant, which is expected to become the default kernel model, is designed to provide support for mixed-criticality real-time systems, as they are increasingly common in complex cyberphysical systems, including aircraft and autonomous cars.
Initial experience with the MCS model exhibited some shortcomings that restrict the class of systems it can support. A critique of the model was provided by the honours thesis of Curtis Millar, with a number of improvements advocated, although in several cases the particular design choices were insufficiently justified and may not be the best ones. This project is to take Millar's work further by critically analysing his designs and implementations and the trade-offs involved and converge on an acceptable model.
Expected outcomes:
Supervisor: Gernot Heiser
Abstract:
Development of operating-system functionality frequently involves performance analysis and optimisation. The seL4 microkernel presently has limited support for this. In particular, it is missing a gprof-like framework for performance analysis through statistical sampling. The project is to learn how statistical sampling is implemented in Linux and implement equivalent functionality on seL4, with generation of output suitable for post-processing by gprof.
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: