Applications for summer research in Trustworthy Systems for the topics below can be made through
Supervisor: Ivan Velickovic, Gernot Heiser
Abstract:
The seL4 Core Platform (seL4CP) is a new, lean and simple OS environment built on the seL4 microkernel aimed at embedded and cyberphysical systems. Originally fully static, dynamic features were recently proposed and prototyped. This project is to evaluate these features in terms of performance and usability, e.g. in terms of enabling on-the-fly software upgrades and late application loading.
Expected outcomes:
Supervisor: Peter Chubb
Abstract:
Recent work in TS on building performance networking support in seL4 has shown that Linux networking performance lags significantly behind what can be achieved on seL4 with the seL4 Device Driver Framework (sDDF), despite Linux requiring far fewer mode and context switches than an seL4-based system for the same job. There is indication that this represents a performance regression in the Linux networking subsystem.
This project is to understand the nature and cause(s) of this regression. The work is to build various Linux point releases from the past 15 years and run network performance test on them. Identify the points of significant regression, and analyse the kernel changes that went into those releases. Try to understand the root causes of the regression.
Expected outcomes:
Project allocated!
Supervisor: Peter Chubb, Gernot Heiser
Abstract:
Bus-mastering DMA devices in modern computer systems are attached via a memory-management unit, called IOMMU or System MMU (SMMU) depending on the manufacturer. The IOMMU that can control which physical memory regions a device may access. As such, it presents an important mechanism for encapsulating untrusted devices and their drivers.
To make best use if the IOMMU, the device should only be able to access the absolute minimum portion of RAM, specifically the region(s) containing the buffer the device is to read or write. This required re-programming the IOMMU mappings for every I/O. However, this can introduce substantial overheads [Malka et al, FAST'15], leading to security-performance tradeoffs.
This project is to evaluate IOMMU performance trade-offs on recent x86 and Arm processors, and answer the following research questions:
Expected outcomes:
Project allocated!
Supervisor: Gernot Heiser
Abstract:
Pancake is a new programming language aimed at enabling the verification of device drivers. The language itself is still under development. This project is to evaluate the current Pancake language by using it to implement drivers of various complexity and providing feedback to the language developers.
Expected outcomes:
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:
Project allocated!
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:
Supervisor: Johannes Åman Pohjola
Abstract:
Low-level systems programming such as device driver development is tedious and error-prone. Pancake is a research programming language currently under development at Chalmers University of Technology, KTH, ANU, and UNSW. It comes with a formally verified compiler and is built from the ground up for predictable compilation and ease of verification.
The semantics of Pancake is currently formalised as functional big-step semantics, which is convenient for compiler correctness proofs. Unfortunately, this style of semantics is awkward for verification of interactive programs such as device drivers, because it requires a fully deterministic model of the device.
The aim of this project is to develop a denotational semantics for Pancake, where the meaning of programs are represented by interactive trees. Interaction trees are a new general-purpose coinductive data structures that describes environment interactions in a branching-time style. This new semantics should be defined in the HOL4 interactive theorem prover, and proven sound and complete wrt. the existing semantics.
Expected outcomes:
Supervisor: Johannes Åman Pohjola
Abstract:
Low-level systems programming such as device driver development is tedious and error-prone. Pancake is a research programming language currently under development at Chalmers University of Technology, KTH, ANU, and UNSW. It comes with a formally verified compiler and is built from the ground up for predictable compilation and ease of verification.
The compiler correctness proofs use machine models that don't have great support for shared memory---they generally assume that programs have exclusive read and write access to their memory domain, and that reads and writes to memory are otherwise free of side effects. Device drivers interact with devices using memory-mapped I/O, which satisfies neither of these assumptions.
The aim of this project is to investigate ways of extending these machine models to incorporate support for memory-mapped I/O in a principled way, without hardcoding it to specific devices. Time allowing, this support should then be propagated upwards in the Pancake compiler stack and reflected in the semantics of the compiler IRs. This work will be carried out in the HOL4 interactive theorem prover.
Expected outcomes: