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)

Evaluate languages for verified LionsOS components NEW

LionsOS is a highly-modular, seL4-based OS under development at TS, with the aim of end-to-end verification of enforcement of security and safety. This requires, among others, that components of its trusted computing base (TCB) are verified for functional correctness, with proofs linked to the seL4 abstract specification and applying to the executable code (taking the compiler out of the TCB).

While in the verification of seL4 the C compiler was removed from the TCB by a translation-validation proof, this approach is fragile and imposes limits the complexity of the code. A better approach is to use a programming language with a well-defined semantics and a verified compiler, i.e. one that is proved to produce binaries that preserve the semantics of the source code. Three such languages and corresponding compilers exist:

  1. The CompCert compiler for the Clight subset of C
  2. The CakeML functional language and
  3. The Pancake low-level systems language under development at TS.

Each of these has its strengths and weaknesses. For example, CakeML is a managed language and as such unsuitable for OS code that requires deterministic resource usage and temporal behaviour but might be suitable for, eg, an IP stack, while Clight and Pancake are very low-level.

This thesis is to perform a detailed, quantitive comparison of the three langage systems, including evaluating for which parts of LionsOS each might be suited for, programmer and verifier productivity, and performance of the generated code. This will involve implementing/porting LionsOS components in/to one or more of these languages and evaluating the implementations along the criteria mentioned above. A particularly interesting target is the Microkit library, which is at the core of LionsOS.

We expect this thesis to produce verification-ready LionsOS production components. The topic has significant publication potential.

Secure file system

Project allocated!

Usable system model for time protection

Project allocated!

Fact-check HongMeng NEW

A recent paper on the HongMeng microkernel makes a number of claims about shortcomings of other microkernels, including seL4. This thesis is to analyse these claims, many of which are poorly supported by evidence, and check whether they hold up to scrutiny. This will require developing and evaluating some prototype implementations.

The aim of the project is to demonstrate that much, if not all, of what the HongMeng work claims to require adding functionality in the microkernel (in violation of the microkernel minimality principle), can in fact efficiently be provided by seL4 without requiring any kernel changes (other than possible implementation improvements that do not change the seL4 model).

Prerequisite: COMP9242

Formalising and verifying device controllers NEW

Project allocated!

Formalisation and implementation of security policies NEW

Any verification of security enforcement by an OS, whether it be a statically-architected one, such as LionsOS, or a general-purpose OS, needs a formalisation of its security policy. This project is to develop, under supervision of a formal methods expert, a formalisation of some standard security policies and proof security properties about them. The policies should be representable in the LionsOS framework and also apply to the general-purpose OS.

ARINC time-partitioned scheduling on seL4 MCS

Project allocated!

“Containers” on LionsOS

Project allocated!

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

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 LionsOS

Project allocated!

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

Project allocated!

Most topics can lead to publications.

Present topics supervised by Rob Sison (official list)

Proving functional properties for system calls that block NEW

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!

Verification of OS component interactions under weak memory models

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