Trustworthy Systems

Honours Thesis Projects

Introduction

The thesis topics listed here are available to strong final-year undergraduate students. They are mostly associated with research projects and generally quite challenging; many topics have the potential to lead to a publication, and in average we get about one paper a year from the work of one (or more) undergraduate thesis students. Students who are not aiming for excellence are in the wrong place here.

We guarantee a thesis topic to any student who has obtained a HD grade in UNSW's Operating Systems or Advanced Operating Systems course, no matter what their other grades are! This does not mean that an OS HD is a prerequisite, but we do expect our students to have a strong track record in relevant courses.

Strong computer Science Honours students may qualify for the John Lions Computer Science Honours Award.

Note that the below list is constantly updated, new topics are added as we identify them as work on various research projects proceeds. Topics marked NEW are recent additions.

Topics supervised by Gernot Heiser (official list)

Formalising and verifying device controllers NEW

The TS group is working on verifying device drivers for LionsOS using the Pancake language. This work is inevitably dependent on a correct formalisation of the HW interface.

The project is to take an open-source Ethernet controller from the Verilog-Ethernet repository" and, in close collaboration with the Pancake team formalise its software interface. Once successful, evaluate the use of the LUBIFIER tool for verifying the hardware implementation.

ARINC time-partitioned scheduling on seL4 MCS

Project allocated!

“Containers” on LionsOS NEW

Containers are a hack that attempts to provide isolation similar to virtual machines at lower cost, by working around the lack of principled resource managements in mainstream OSes, such as Linux. In a lean and highly efficient OS such as LionsOS, the standard process abstraction should be lightweight enough to achieve strong isolation.

This project is to design and implement support for container-like domains on LionsOS and evaluate them against Linux containers.

Low-overhead virtual machines on Microkit NEW

The seL4 Microkit is a simple OS framework for embedded systems. It supports virtual machines by re-directing virtualisation events to a per-VM, usermode virtual-machine monitor (VMM). The present VMM is inherited from an earlier system and has high overheads.

This project is to systematically analyse the source of these overheads and develop a lightweight VMM for use in embedded systems.

Principled PMU management in seL4 NEW

The performance management unit (PMU) is a component of modern CPUs that provides insight into the operation of the processor by counting specific hardware events. The PMU is widely used for statistical profiling (for performance analysis at the microarchitecture level) but also for production use, such as driving models of energy use that are essential for managing overall energy consumption in a computer system.

The seL4 microkernel presently only supports the PMU in a debugging configuration, which is sufficient for profiling but not for production use. A recent RFC proposes the introduction of a new PMU kernel object to support these use cases. This project is to implement and evaluate the PMU object in seL4 and its use for sharing and time-multiplexing the PMU.

Automated validation of SPIN models NEW

LionsOS and the seL4 Device Driver Framework (sDDF) it is based on make extensive use of a single-producer, single-consumer shared-memory model for zero-copy data-passing between components. The model uses simple lock-free queues synchronised with binary semaphores. For performance it is important to avoid signalling a component when it cannot do useful work.

This results in complex signalling protocols that are easy to get wrong (leading to deadlocks). Model checking (using SPIN) has been valuable in aggressively optimising those protocols while ensuring lifeness. However, these SPIN models are presently manually derived from the C or Pancake implementations, which is itself an error-prone approach. This is particularly so as the models do not have a one-to-one correspondence the code, but in fact represent an abstraction in the sense that many states of the real component map to the same state of the model.

The aim of this project is to develop a tool that automatically parses the C/Pancake code (really the system calls) and data structures, as well as the SPIN model and validates that the SPIN model is indeed an abstraction, in the sense that for each state transition in the code there is a corresponding state transition in the model. Ideally it should be possible to verify that tool, but this is out of scope for the thesis.

Evaluate queueing performance in sDDF

Project allocated!

Can we make servers untrusted in seL4?

The protected-procedure call mechanism of seL4 is the microkernel equivalence of a Linux system call: it allows securely executing code with different (typically higher) privileges. As such, it is a standard assumption that the invokee (the “server”) is trusted by the client.

This thesis is to explore the degree to which that trust can be reduced. Unlike Linux, the client's address space is protected from the server (unless that has explicitly been given capabilities to some of the client's memory). However, since the client is blocked for the duration of the call, it must trust the server to return promptly. While the client can use a watchdog thread to prevent unlimited blocking (a very coarse-grain protection mechanism), a client invoking a server has essentially no mechanism for limiting the amount of its budget the (passive) server consumes. This thesis is to explore, design, implement and evaluate mechanism(s) for limiting the budget the server can consume.

Core management in Lions OS

A processor core consumes energy, whether it is doing useful work or not, unless it is in a “deep sleep” state. Transitioning into or out of such sleep states takes time (and energy), making a pure core-local energy management inefficient. Instead the OS should aim to maximise the period cores are in deep sleep. This requires monitoring overall CPU utilisation, and off-lining lowly utilised cores by migrating their activities to other cores.

The structure of Lions OS supports this approach: It has a highly modular design, with individual modules strictly sequential (executing on a single core) and modules communicating via shared memory, synchronised by semaphores. This means most modules are completely location transparent and can easily be migrated to a different core.

The aim of this thesis is to design and implement the mechanisms for core migration in the seL4 Microkit, which is the framework in which Lions OS is implemented. Depending on progress, the next step would be to implement a core manager, which monitors load an consolidates or spreads activities as required by load.

Native high-performance file-system API for seL4

Project allocated!

PD Templates for the Microkit

Project allocated!

Dynamic IOMMU management in sDDF

The seL4 Device Driver Framework (sDDF) provides the basis for high-performance I/O in Lions OS, currently under development in TS. It presently uses static I/O-space mappings in the system's IOMMU. This requires trusting the device and its driver.

This project is to implement and evaluate dynamic IOMMU mappings in sDDF. This implies a prototype implementation and a cost-benefit analysis of dynamic IOMMU mappings, as well as suggesting an appropriate kernel interface.

Driver VMs: Re-use of unmodified Linux device drivers in seL4

Project allocated!

Secure OS for Sunswift

Project allocated!

Most topics can lead to publications.

Present topics supervised by Rob Sison (official list)

Formalising the composition of security subpolicies for OS components NEW

We have been exploring the use of SMT solver-based automated deductive verification methods to verify the correctness of OS components running as guests on top of the seL4 OS kernel. However, research on verifying security properties for such components is only beginning.

This thesis is to investigate and develop formal methods to compose local security properties, which enforce appropriate "subpolicies" for each component, into global security properties that enforce integrity or confidentiality policies over the entire system.

The main task will be to explore the feasibility of (1) defining appropriate policies and properties for component-based OSes and (2) proving principles by which local security properties compose into global ones, whether with pen and paper or using an interactive theorem prover like Isabelle/HOL. In addition, the thesis should prioritise the study and further development of prior work on developing compositional security properties so as to be provable using SMT solver-based automated deductive verification tools.

Refining seL4's accounting of touched addresses for Time Protection NEW

Microarchitectural timing channels are a serious security threat: they can be used to steal critical secrets, such as the encryption keys of web servers. We have recently developed mechanisms, collectively referred to as time protection in the seL4 microkernel that aim to prevent timing channels being exploited across security boundaries. These mechanisms have been formalised and are now being formally verified using the Isabelle/HOL interactive theorem prover.

This thesis is investigate and determine the feasibility of a recently proposed strategy for proving that time protection is correctly enforced by seL4's C implementation. If feasible, this would enable the first ever proof of time protection enforcement by any OS kernel implementation.

To this end, the main tasks will be to develop initial designs for infrastructure and formal methods for seL4's Isabelle/HOL proof base for soundly overapproximating the set of "touched addresses" dereferenced by seL4's C specification (CSpec) level, in a scalable manner. The goal would be to ensure that these designs enable the construction of proofs in Isabelle that this set is both (1) a refinement of the corresponding areas of memory accounted for by seL4's abstract specification (ASpec) and (2) a subset of addresses the currently running security domain is allowed to access according to the system's policy.

Verification of OS component interactions under weak memory models

Project allocated!

Userspace verification of component-based OS as a concurrent system

Project allocated!

How to apply:

Contact the relevant supervisor.

Note for OS related topics: We promise a thesis topic to every interested student who has obtained a HD grade in COMP3231/COMP9201 Operating Systems or COMP9242 Advanced Operating Systems. If necessary we will define additional topics to match demand.

We will not turn down any students doing exceptionally well in OS courses. However, this does not mean that an HD in OS or Advanced OS is a prerequisite for doing a thesis with me. Interested students with lower OS marks are welcome to talk to me if they feel they can convince me that they will be able to perform well in an OS thesis.

Keep in mind that these topics are all research issues and generally at the level of Honours Theses. They are not suitable for marginal students or students with a weak understanding of operating systems. We expect you to know your OS before you start.

Topics for a Special Project (COMP3901/3901):

Some undergraduate thesis topics are also suitable for a special project (typically with reduced scope/expectations). But generally Taste of Research topics are a better match for this. Talk to us if you're interested!

Postgraduate project topics (COMP999x):

Undergraduate thesis topics are also suitable for coursework Master's projects. Same conditions apply: You must have a pretty good track record in OS courses for OS and FM related topics.

Information about research theses