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)

OS support/virtualisation of Vulkan and OpenGL NEW

Support for graphics accelerators is important for many embedded/cyberphysical systems. Vulkan is an API that provides high-efficiency, cross-platform access to modern GPUs used in PCs, and as such is an excellent candidate for graphics support in LionsOS.

This thesis is to analyse Vulcan, and design, implement and evaluate support for it in LionsOS.

Zephyr-compatible API for LionsOS NEW

Zephyr is a small real-time operating system for connected, resource-constrained and embedded devices. Its popularity makes it a de-facto standard for embedded systems, with many embedded-systems engineers familiar with its API. Support for the Zephyr API in LionsOS would therefore ease porting embedded applications into native components.

This thesis is to design, implement and evaluate a Zephyr-compatible API on top of Lions, with liberal re-use of Zephyr code (as permitted under its permissive license).

Feasibility of seL4 implemented in Pancake NEW

The verified seL4 microkernel is implemented mostly in C (with a small amount of assembler code). Pancake is a new systems language developed by an international collaboration centered at Trustworthy Systems. Pancake's unique advantage is that it has a verified compiler that guarantees correct code generation, while having a much simpler (and thus more verification-friendly) semantics than C. It is mature enough to allow implementing much of LionsOS without a need for foreign function calls (FFIs) while performing close to C.

This opens up an exciting possibility: Would it be possible to re-implement seL4 in Pancake, and potentially reducing the cost of maintaining seL4's proofs (to which the complexities of the C semantics are a major contributor)?

This thesis is to evaluate the use of Pancake for implementing seL4. It does not require a formal-verification background, but deep experience in low-level programming in general and strong familiarity with kernel code in particular.

Specify and implement HID driver classes

LionsOS is a new seL4-based OS for embedded systems under development at TS. It is based on the seL4 Device Driver Framework (sDDF), which provides a much simplified device model compared to legacy OSes.

While a number of device classes have been specified and implemented on various platforms, presently there is a lack of classes for human-interface devices, such as keyboard, mouse and touchscreen. This project is to provide these. A short-term goal is enabling the touchscreen of the TS kitty, a proof-of-concept of a point-of-sale device that is in active use in the TS lab. A stretch goal is to run LionsOS on a simple laptop.

Bluetooth client for LionsOS

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

Project allocated!

Camera interfaces and device drivers for the sDDF NEW

The seL4 Device Driver Framework (sDDF) defines interfaces for many different device classes, such as network, serial, storage, etc., and for some buses (like I2C). Work is ongoing an a USB stack.

Cameras generally attach either via a MIPI CSI interface (usually CSI-2 on consumer-grade equipment), or via USB. There are several parts to the work for this thesis, not all of which would be necessary:

Of course, critically evaluating the whole system for performance and for usability is part of the project.

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

Project allocated!

Secure Boot Process of LionsOS

Project allocated!

Analyse and optimise driver VMs

Project allocated!

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

Project allocated!

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).

State Machine Model 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.

Device drivers and similar software can often be best thought of as state machines. They have a collection of major current states and possible transitions between them, and for each hardware or software event they handle they may transition state.

Such a state machine can then be encoded in a standard language, for instance by having the event-handling function perform a large "switch" or "case" division across the many states and event cases. There are other ways to do the encoding, and the problem is interesting enough that there are different schools of thought as to the best approach. An introduction to the issue is given in the slides by Madhukar Anand and Miro Samek . Work on sophisticated state machines continues, including "Rage against the State Machine" (full text may be available when viewed from a UNSW IP address) .

A better approach might be to have a design approach that made the state machine design explicit. The goal of this project is to explore a design where a state machine program can be written as a state machine, with Pancake code snippets included that are associated with some transitions. The student would develop a parser and transformer that converts this into a regular Pancake program.

Optional parts of the project might include (a) studying the semantics of the new language and the correctness of the transformer or (b) also exporting a summary of the state machine and checking with a model checker like UPPAAL or SPIN that a collection of parallel state-machine components cannot end up in a bad state.

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 formal methods expertise (e.g. COMP4161 at UNSW, use of Dafny, 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!

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