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

Project allocated!

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

Project allocated!

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

Project allocated!

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.

Present topics supervised by Thomas Sewell (official list)

Language Extensions for Pancake

Pancake (see the project page) is a new low-level language, similar in some ways to C, designed for the development of formally verified device drivers.

Pancake supports single-layout data structures (similar to struct types in C), and their syntax was substantially improved in a 2025 undergraduate thesis project. This project will extend the language further with multi-layout data structures, such as Rust's enumeration types. Interested students might also want to consider the data-representation ideas presented by the Dargent (see the paper) language.

An optional aspect of this project is to verify the correctness of the new and/or existing compiler phases which handle the syntax extensions.

This project would be appropriate for students with a substantial background in language-related apparatus (e.g. COMP3131, COMP3161 at CSE or similar experience). The optional verification component would be appropriate for a student with proof-related expertise (e.g. COMP4161 at UNSW or similar background).

Translation Improvements for HOL/CakeML

The CakeML project (see the main CakeML project page) provides a compiler for various languages with a formally verified proof of correctness. Near the heart of the project is a mechanism called the translator, which translates between high-level encodings of functions in the HOL4 logic and explicit program syntax that can be compiled by the compiler. It is this mechanism that allows the compiler to "bootstrap" by compiling itself.

This project is to consider some valuable extensions to the translation apparatus and implement (at least) one of them. All of these projects will require some design of language apparatus and substantial work in editing formal proofs. We would recommend these to students who liked COMP4161 or have similar background or experience.

Extension (A) is to provide a mode for translating from HOL4 representations to Pancake syntax. Pancake is a low-level programming language co-developed with CakeML and used extensively in UNSW systems programming projects. This would allow various low-level computations which do not need a memory allocator to be designed and verified in HOL4 and converted via Pancake to efficient machine code.

Extension (B) is to provide "seperate compilation" for the CakeML translator. The current translator produces a single output program, and requires all translations to know the complete program prior to a definition (i.e. all previous translations). This makes library modules a headache to manage. nuisance. This project will allow seperate modules to be translated individually with a final computation resolving the dependency graph to a single final program.

Extension (C) is to translate via an alternative representation for recursive functions. The current translation approach assumes that recursive functions are terminating, and that their proof of termination is either obvious or provided via an induction theorem that matches their definition. However there are various technical limitations with this approach, and it fails outright if the definition is "tweaked". This project is to experiment with a representation that combines the definition and termination condition into a single more general representation.

Experiments in Verified Complexity

UNSW has substantial expertise in analysis of branching algorithms and proving worst-case bounds on their running time. This running time bound is typically a precise measure of their exponential complexity. Recently we have become interested in verifying these proofs of running time in a formal system, e.g. Isabelle/HOL. Verifying these complex proofs will help in publishing existing results, and, we hope, actually simplify the re-analysis of the complexity bounds of an algorithm when it is slightly adjusted.

The goal of this project is to pick a branching-time algorithm of medium complexity, understand the proof of its complexity as a pen-and-paper proof, and then formally verify that proof in Isabelle/HOL.

This project is recommended to students who have background in at least one of COMP4161 (verification in Isabelle/HOL) or COMP6741 (exponential algorithms and their proofs of complexity) or similar background experience in both areas.

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.

Formalisation of Viper semantics in the HOL4 theorem prover

Project allocated!

Pancake is a new programming language for verified systems programming developed by the Trustworthy Systems group and some collaborators. Pancake has a prototype transpiler that converts annotated Pancake code into Viper, an intermediate language for efficient SMT-based verification. This thesis aims to develop a formal semantics for Viper on the HOL4 theorem prover, which we will use in future for verifying the correctness of the transpiler implementation.

Pancake versions of LionsOS components are being written, and we plan to verify them using the verification framework based on this transpiler. Verifying the transpiler implementation will allow us to remove the transpiler from the TCB.

The student is expected to be comfortable with using theorem provers. The project will start with investigating an existing semantics of a Viper subset in Isabelle/HOL and porting it to HOL4, which we will then aim to extend further to cover the necessary scope of the transpiler.

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