Trustworthy Systems

Honours Thesis and Other Coursework Projects

Introduction

The thesis/project topics listed here are available to strong final-year undergraduate students, and as research projects for strong coursework 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)

Specify and implement HID driver classes NEW

Project allocated!

Bluetooth client for LionsOS NEW

LionsOS is a new seL4-based OS for embedded systems under development at TS. It features a highly modular structure and a (compared to legacy OSes) much simplified device-driver model. A number of device classes have been specified and drivers implemented.

One of the devices not supported natively so far is Bluetooth, which is, of course, highly desirable. Leveraging current work on supporting USB, a native Bluetooth client driver can be built. An example use case is remote control of a LionsOS-based robot that is presently being developed.

Develop Serengeti into a more complete SoC design NEW

Project allocated!

Critical analysis and design revision of the LionsOS IP stack NEW

LionsOS is a new seL4-based OS for embedded systems under development at TS. It features a highly modular structure driven by the principle of separation of concerns. Among others, it separates device sharing from protocol processing, meaning that the IP stack is not shared, but each client of a networking interface has its own protocol stack. Presently this is lwIP.

There are a number of issues with the present design. For one, it is unclear whether lwIP is the best choice. Furthermore, while having per-client IP stacks should remove these from the trusted computing base (TCB), in reality LionsOS currently trusts the IP addresses the stack puts into network packets, creating a potential of denial-of-service attacks by a malicious client.

The thesis is to re-visit this design, explore alternatives, and evaluate performance.

LionsOS-based Wifi Router NEW

The LionsOS Firewall project provides basic (but rapidly growing) infrastructure for networking systems. This project is to use it as a starting point to develop a complete, deployable Wifi router, using a commercial, open hardware platform, such as the Banana Pi OpenWrt One Router or the Mono devkit.

Secure Boot Process of LionsOS NEW

Project allocated!

Analyse and optimise driver VMs

Joint Supervisor: Peter Chubb

LionsOS is a new seL4-based OS for embedded systems under development at TS. It uses a modular device-driver model that passes I/O data via shared-memory, zero-copy data structures. LionsOS I/O outperforms Linux.

However, the LionsOS driver model is incompatible with that of legacy systems, making it necessary to re-write drivers from scratch. While this is ok for selected, performance- or security-critical devices, and made approachable by the simplicity of the model, it is unfeasible to write all drivers from scratch.

LionsOS supports re-use of unmodified Linux drivers by encapsulating a driver into a minimally configured Linux kernel hosted in a per-device driver VM, which appears to the rest of the system like a native driver. While efficient in terms of engineering cost, this comes at a significant performance cost.

This project is to evaluate and analyse the overheads of driver VMs and investigate how far they can be reduced. While we cannot expect driver VMs to perform at par with native drivers, we are interested in minimising overheads for complex yet important device classes, such as Wifi, USB and graphics. Native Linux will serve as the performance baseline.

LionsOS-based robot demonstrating hard real-time capabilities

Project allocated!

ARINC-653 OS on seL4

Project allocated!

NASA core Flight System on LionsOS

Project allocated!

Persistence for LionsOS apps

Project allocated!

Secure file system

A secure operating system, such as TS's LionsOS or the Secure general-purpose OS, needs a secure file service, where “secure” implies two properties:

  1. The file system enforces access control based on the system's security policy.
  2. The file system can be formally verified to behave according to specification.

While building and verifying a file system is beyond the scope of a thesis project, this thesis is to lay the groundwork, by designing and implementing a file system for SDcard storage that is:

Basing the new file service on an existing low-level storage organisation, such as FAT, is desirable to provide a degree of compatibility. The TCB components should be implemented in C to be later transliterated into Pancake for verification, other components can be implemented in C or Rust.

Principled PMU management in seL4

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 mainline 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, but is stalled.

This project is to revisit PMU management with the aim of coming up with a less intrusive model that supports a combination of global and per-process monitoring. A driving use case is providing introspection in LionsOS, including monitoring CPU and memory load, and functionality similar to top.

Dynamic IOMMU management in sDDF

The seL4 Device Driver Framework (sDDF) provides the basis for high-performance I/O in LionsOS, 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.

Secure OS for Sunswift

This topic is to evaluate requirements on an operating system for the Sunswift solar racing car, and design and implement such a system on the seL4 Microkit. This project will be done in close collaboration with Sunswift developers and will support/prototype a number of real Sunswift subsystems. Design work includes a threat analysis and effective passive defences against cyber attacks.

Most topics can lead to publications.

Present topics supervised by Rob Sison (official list)

Proving functional properties for system calls that block

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. Verifying systems that run on top of seL4 (e.g. via the seL4 Microkit), however, will rely on its system calls correctly implementing certain functional properties, phrased as postconditions on its outputs it must meet if its caller satisfies preconditions on its inputs.

For system calls that block on the activity of other processes - e.g. waiting for a message to be queued, through to being woken up when that happens - this is a verification result that has yet to be achieved by the prior OS verification literature. Work at TS has recently begun on proving such properties are satisfied by the seL4 kernel's abstract specification in the Isabelle/HOL interactive theorem prover, but restricted so far to nonblocking cases - e.g. receiving a message that's already been queued.

This thesis project is to prove functional properties about seL4's system calls in Isabelle/HOL, focusing especially on sensible assumptions and guarantees that could for the first time enable proofs about blocking and unblocking system calls to be composed into a single functional property from the temporarily blocked caller's perspective. Stretch goals can include furthermore attempting to develop and apply the formal methods needed to achieve this composition.

Validating seL4's accounting of touched addresses for Time Protection

Project allocated!

Refining seL4's accounting of touched addresses for Time Protection

Project allocated!

Formalising the composition of security subpolicies for OS components

Project allocated!

Topics supervised by Miki Tanaka (official list)

Formalising and verifying device controllers

Joint Supervisor: Gernot Heiser

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.

This on-going project is to take an open-source device design (from e.g. OpenTitan project) and, in close collaboration with the Pancake team, formalise its software interface, which we also validate against the original hardware design.

This thesis project is to continue the current formalisation of several devices (including I2C and SPI) and also to apply the framework to a new device to access its usability.

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