Trustworthy Systems

Taste of Research (ToR) Project Proposals

Applications

Applications for summer research in Trustworthy Systems for the topics below can be made through

Projects

 

Systems

Optimise the seL4 IRQ fastpath

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:

  1. report describing the analysis of the IRQ code path, comparing with notification-object signalling, and optimisations based on comparison to signalling; detailed benchmarks;
  2. pull request against the seL4 kernel mainline.

Performance analysis of stub code overhead in client-server interaction on seL4NEW

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:

  1. Report describing the results of the performance analysis
  2. Potentially pull requests against the libsel4 repository for optimised stub code

Analyse and improve the seL4 MCS variantNEW

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:

  1. report outlining findings, including discussion of trade-offs and performance evaluation
  2. pull requests against the seL4 MCS variant

Profiling framework for seL4NEW

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:

  1. Gprof-like library for statistical sampling
  2. Tool that mangles the collected data into a form that can be processed by gprof

Optimise seL4 cold-cache / worst-case performance

Gernot Heiser

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.

 

Formal Methods

Automatic verification of the seL4 Core PlatformNEW

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:

  1. report describing experience verifying the sCP using an SMT solver
  2. formal specification of at least a significant part of the sCP
  3. successful verification of at least a subset of the specified functionality
  4. potentially pull requests against the public sCP source