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)

Secure file system NEW

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.

Usable system model for time protection NEW

Time protection (TP) is a principled OS mechanism for preventing information leakage through microarchitectural timing channels. It was originally proposed and implemented in an seL4 prototype by TS PhD student Qian Ge in an award-winning publication and its implementation in seL4 is presently undergoing formal verification. Later work at ETH Zurich proposed a hardware mechanism, the fence.t instruction, in another award-winning paper.

While this past work created significant impact, the present TP model in seL4 is extremely limiting, as it assumes fully isolated subsystems. Most practical systems, however, require some communication between security domains, at least one-way information flow. Furthermore, the existing model fails to prevent leakage through the shared cache through accesses to shared kernel memory.

The aim of this thesis is to solve the problem of shared kernel data, and develop a model, and proof-of-concept implementation in seL4, of a system that supports overt information flow between security partitions according to a security policy, but prevents covert flows that violate the policy. A target application is a secure web browser, where untrusted java code running in a tab is confined to only communicate via trusted system components.

Prerequisite: COMP9242

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

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.

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

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

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)

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