Trustworthy Systems

Research Internships (Taste of Research)

Introduction

Taste of Research (ToR) is an internship program run by the UNSW Faculty of Engineering for undergraduate students. It is accessible to undergraduate students from any Australian or New Zealand university. The internship can be taken (full-time) during the summer break (with some spill-over into the teaching term for UNSW students) or completely (part-time) during the term.

TS regularly hosts a large number of ToR students. Application through the program must happen through the Faculty and according to their deadlines. However, we strongly recommend that interested students talk to potential supervisors before submitting an application!

Students from overseas universities may qualify for the UNSW Practicum Program, and under that program would be able to work on one of the projects on this page. If you are an overseas student and interested in such an internship with us, please contact us directly before applying for the practicum!

Projects

Below are our current list of projects, which changes frequently. It is synchronised with the official list just before this opens for the next round.

 

Operating Systems

Deployable firewall based on seL4 NEW

Supervisor: Peter Chubb

Abstract:

The TS group has just developed a proof-of-concept of a secure network firewall running on the verified seL4 microkernel and LionsOS. It presently has a number of limitations that prevent is practical use, including no support for IPv6, network address translation, connection tracking, filter rule chaining and a number of protocols.

This project is to add the missing functionality, with the aim of deploying the firewall to protect the TS network.

Expected outcomes:

  1. fully functional firewall that can be deployed
  2. report describing design and implementation.

IDL compiler for general-purpose OS

Project allocated!

Dynamic sDDF

Project allocated!

Labelled file system

Project allocated!

Make Time Protection Realistic

Project allocated!

IP stack in CakeML

Project allocated!

Using CompCert for LionsOS

Project allocated!

Evaluate seL4 against the HongMeng microkernel NEW

Supervisor: Peter Chubb and Gernot Heiser

Abstract:

A recent paper on the HongMeng microkernel makes a number of claims about shortcomings of other microkernels, including seL4. This project is to drill down on some of the (poorly supported by evidence) claims and check whether they hold up to scrutiny. This will require developing and evaluating some prototype implementations.

Expected outcomes:

  1. prototype implementation of alleged bottlenecks
  2. report describing design, implementation and performance.

Core management in LionsOS

Project allocated!

Alternative network measurement clients for LionsOS NEW

Supervisor: Peter Chubb and Matt Rossouw

Abstract:

In the past, TS has measured network performance using ipbench. This is a locally invented tool that orchestrates multiple load generators to stress test a network stack, and report latency and throughput for different loads.

iPerf3 is a network benchmarking tool commonly used to measure throughput, jitter and packet loss on Linux and Windows operating systems.

This project is to implement iPerf and iPerf3 clients for LionsOS, and compare results from them with ipbench results. By measuring in more than one way, we expect to gain insight into the system's behaviour, and be able to compare more directly with published results.

Expected outcomes:

  1. Implementation of an iPerf3 client for LionsOS that is as performant as our current echo server, together with pull request(s) to add it as an example to the LionsOS repository.
  2. Implementation of an iPerf client (the LWIP stack we currently use already has one)
  3. Benchmark runs on a variety of platforms comparing the different measurement techniques
  4. A report detailing the outcomes.

LionsOS on x86 NEW

Supervisor: Peter Chubb

Abstract:

The Trustworthy Systems group has developed a new Operating Systems framework, called LionsOS, that currently runs on Risc-V and aarch64. It works with multiple components each in its own address space talking to each other using seL4 notifications and queues in shared memory regions. LionsOS uses virtual machines as a way to support legacy software.

This project is largely engineering rather than research; it involves porting LionOS to x86_64, and especially, porting libvmm, the virtual machine library that provides hypervisor support, to x86_64.

Stretch goals include implementing or porting firewall components to provide and control network access between VMs, and between VMs and the outside world; and control software for shutrting down and rebooting VMs.

Expected outcomes:

  1. Performant LionsOS on x86_64
  2. Usable libvmm for x86_64

Formalising and verifying device controllers

Project allocated!

ARINC time-partitioned scheduling on seL4 MCS

Project allocated!

“Containers” on LionsOS

Project allocated!

Analyse and improve virtualisation performance on seL4 Microkit

Project allocated!

Multikernel support in Microkit

Project allocated!

New device class for sDDF

Project allocated!

WCET Analysis of seL4 on RISC-V

Project allocated!

Dynamic IOMMU management in sDDF

Supervisor: Peter Chubb and Gernot Heiser

Abstract:

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.

Expected outcomes:

  1. Prototype implementation of dynamic IOMMU mappings;
  2. Performance evaluation;
  3. Report describing the above.

Principled PMU management in seL4

Supervisor: Gernot Heiser

Abstract:

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.

This project requires an Advanced Operating Systems background.

Expected outcomes:

  1. Prototype implementation of a PMU object in seL4;
  2. demonstration of its use for securely sharing the PMU between processes with different monitoring needs, including processes requiring a global view as well as processes observing their own performance;
  3. report outlining findings.

VMM environment for developing Microkit applications on Linux

Project allocated!

Persistence for seL4 Microkit apps

Project allocated!

Evaluate dynamic Microkit features

Supervisors: Gernot Heiser, Ivan Velickovic

Abstract:

The seL4 Microkit is a new, lean and simple OS environment built on the seL4 microkernel aimed at embedded and cyberphysical systems. Originally fully static, dynamic features were recently proposed and prototyped. This project is to evaluate these features in terms of performance and usability, e.g. in terms of enabling on-the-fly software upgrades and late application loading.

Expected outcomes:

  1. Sample code demonstrating the use of the Microkit dynamic features for realistic uses;
  2. Written report of a critical assessment of usability and performance of the Microkit.

 

Formal Methods

Improvements to verification of seL4 Microkit

Supervisors: Rob Sison, Gernot Heiser

Abstract:

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. The seL4 Microkit is a minimal seL4-based OS framework aimed at embedded and cyberphysical systems.

Since verifying the Microkit's key functionality using an in-house SMT solver-based framework, research at TS has been exploring the use of more usable SMT solver-based automated deductive verification tools and frameworks like VeriFast or Viper to verify the implementations of Microkit-based OS components in a more scalable manner.

This project is to improve the verification of the seL4 Microkit library itself by bringing it up to date and extending its scope using such tools.

Expected outcomes:

  1. verification of the seL4 Microkit library's key functionality using a SMT solver-based automated deductive verification tool;
  2. report describing experience verifying the library using that tool;
  3. potentially pull requests against the Microkit library implementation.

Proving more functional properties for seL4's system calls

Supervisors: Rob Sison, Gernot Heiser

Abstract:

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. The seL4 Microkit is a minimal seL4-based OS framework aimed at embedded and cyberphysical systems.

The verification of the seL4 Microkit library relies on the kernel correctly implementing certain functional properties of seL4's system calls, phrased as postconditions on the system call's outputs it must meet if its caller satisfies preconditions on its inputs. 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.

This project is to increase the coverage of functional properties proved about seL4's system calls, initially focusing on cases most relevant to their use by the seL4 Microkit. Stretch goals can include proving further such properties as guided by the informal specifications given in the seL4 Reference Manual.

Expected outcomes:

  1. verification of a Microkit-relevant functional property for at least one seL4 system call;
  2. report describing experience and any new proof infrastructure developed to verify seL4 system call functional properties using Isabelle/HOL.

Implementing and verifying Pancake compiler improvements

Supervisor: Miki Tanaka, Johannes Åman Pohjola, Thomas Sewell

Abstract:

Pancake is a research programming language currently under development at UNSW, Chalmers University, ANU, and Gothenburg University. It comes with a compiler that is verified correct using the HOL4 theorem prover, and is built from the ground up for predictable compilation and ease of verification.

The compiler is an optimising compiler going through many passes and intermediate languages, but there is scope to add many more to improve the quality and performance of generated code. Example improvements we're looking for include:

These are just examples; the precise contents of this topic needs to be negotiated with the supervisors. This topic can take multiple students working different aspects of improvements.

Expected outcomes:

  1. Report outlining the approach taken, tradeoffs considered and work done.
  2. Pull request to the CakeML/Pancake github repository with an implementation and HOL4 formalisation.

Evaluation of SMT-based verification of Pancake device drivers via Viper NEW

Supervisor: Miki Tanaka, Gernot Heiser

Abstract:

Pancake is a research programming language currently under development at Chalmers University of Technology, ANU, and UNSW. It comes with a formally verified compiler and is built from the ground up for predictable compilation and ease of verification.

We have verified some properties of an ethernet driver written in Pancake by annotating the code with necessary conditions and translating it into Viper, an intermediate language, and then feeding it to SMT backends.

The aim of this project is to produce more test cases (i.e., drivers written in Pancake with annotations) for this Pancake-to-Viper verification framework and then to compare and evaluate them, with an aim to assess its efficiency and provide data points for further improvements.

Expected outcomes:

  1. Report outlining the approach taken, tradeoffs considered and work done.
  2. Pull request to the Trustworthy Systems Group's github repository with implementations.

Implementing choice trees in the HOL4 theorem prover NEW

Supervisor: Miki Tanaka, Michael Norrish

Abstract:

Choice trees [Chappe, et al., 2023] is a new data structure that combines coinductive trees of computations with nondeterministic branching to naturally model internal nondeterminism and concurrency. Interaction trees, a preceding similar data structure, can be embedded into choice trees by a monad morphism. Choice trees are originally implemented in the Coq (Rocq) proof assistant. The aim of this project is to implement this choice trees (and its library) in the HOL4 theorem prover.

In a broader context, this project relates to the bigger and on-going project of the Pancake programming language. Pancake is a research programming language currently under development at UNSW, Chalmers University, ANU, and Gothenburg University. It comes with a compiler that is verified correct using the HOL4 theorem prover, and is built from the ground up for predictable compilation and ease of verification. Pancake has a semantics based on interaction trees and we are interested in investigating possible applications of choice trees to Pancake semantics and related verification, but this is out of the scope for the current Taste of Research project.

Expected outcomes:

  1. Report outlining the approach taken, tradeoffs considered and work done.
  2. Pull request to the HOL4 github repository with an implementation and HOL4 formalisation.

Verification of security subpolicies for seL4-based OS components

Supervisors: Rob Sison, Gernot Heiser

Abstract:

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. The seL4 Microkit is a minimal seL4-based OS framework aimed at embedded and cyberphysical systems. TS is presently developing LionsOS, using the same, highly-modular design as the seL4 Device Driver framework (sDDF).

LionsOS is designed for simplicity and strong separation of concerns. This means that many of the components making up the OS have very simple implementations, which should enable their formal verification, ideally using proof techniques based on SMT solvers, which were already successfully used in the verification of the Microkit.

This project is to investigate the use of SMT solver-based methods and frameworks to specify and verify the enforcement of per-component security subpolicies. Here, a subpolicy is what a trusted component must adhere to in order to enable verification of enforcement of a system-wide policy.

Expected outcomes:

  1. formal specification of a security subpolicy for one LionsOS component;
  2. successful verification of the subpolicy for at least a subset of the anticipated cases;
  3. report describing experience verifying security subpolicies for an OS component using SMT solvers;
  4. potentially pull requests against the LionsOS implementation.

Update seL4's abstract specification proofs for Time Protection

Supervisors: Rob Sison, Gernot Heiser

Abstract:

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 project is to contribute to updating the proofs about seL4's abstract specification in Isabelle/HOL to account for changes made to incorporate the time-protection mechanisms. seL4's proof base is a significant piece of proof engineering, and making core changes to the specification results in significant work updating these proofs. While frameworks to perform such proof updates have been developed, much proof work remains to be completed.

Expected outcomes:

  1. updates to the abstract specification proofs for seL4 where time protection invalidates existing proofs;
  2. written report describing the types of breakages caused by the time protection changes to seL4's abstract specification, and the approach taken to repair these breakages.

Update seL4's refinement proofs for Time Protection

Supervisors: Rob Sison, Gernot Heiser

Abstract:

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 project is to contribute to updating seL4's refinement proofs from the abstract specification (ASpec) to the (Haskell-derived) executable specification (ESpec), in particular, the addition of key assertions to ensure that the memory addresses accessed by the seL4 kernel are safely overapproximated. As all such assertions are checked by proof obligations that are part of the proof that seL4's ASpec is refined by the ESpec (an intermediate part of its full C refinement proofs), this work will involve both updating the (informal) Haskell specification to make repair to these proofs possible, and carrying out these repairs in Isabelle/HOL.

Expected outcomes:

  1. updates to the ESpec refinement proofs for seL4 where time protection invalidates existing proofs;
  2. a written report describing:
    • the changes made to the ESpec to reflect the time protection changes to the ASpec;
    • the approach taken to repair breakages to the proof of refinement between the updated ASpec and ESpec.

Automatic validation of SPIN models of sDDF inter-component communication

Supervisor: Gernot Heiser, Courtney Darville

Abstract:

The seL4 Device Driver Framework (sDDF) provides the basis for high-performance I/O in LionsOS, currently under development in TS. It is highly modular, with components communicating via shared memory and semaphore-like seL4 Notifications. sDDF performance is dependent on an efficient signalling protocol, which avoids signalling components when they cannot make progress, while maintaining deadlock- and livelock-freedom. These properties have been verified using the SPIN model-checker.

However, these proofs are only useful as long as the model is a correct abstraction of the actual sDDF. Presently the models are manually derived from inspecting the source code, or the source code is adapted to implement a verified model. The aim of this project is to provide more assurance that the model is a fair representation of the sDDF communication. The project is therefore to develop a tool that tries to establish correspondence between the model and the C implementation. The ultimate aim is to prove that the C implementation refines the SPIN model, this project is a first step towards this aim.

Expected outcomes:

  1. Tool that matches the SPIN model against the communication system calls in the sDDF implementation, and either reports success or indicates where it fails to establish correspondence;
  2. report describing the approach.