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

Analyse and optimise driver VMs

Supervisor: Peter Chubb

Abstract:

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.

Expected outcomes:

Report analysing driver VM overheads for several device classes, identifying optimisation opportunities, and achieved improvements;
pull requests against the respective sDDF/LionsOS repositories.

Deployable firewall based on seL4

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:

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

Native USB stack

Supervisor: Peter Chubb

Abstract:

USB is an important functionality for most systems, including embedded, and is often performance-critical. This project is to develop a USB driver and port a USB protocol stack to LionsOS.

Expected outcomes:

USB working natively on LionsOS;
Report describing the approach, lessons learned and presenting a performance analysis.

LionsOS-based robot demonstrating hard real-time capabilities

Supervisor: Peter Chubb

Abstract:

Develop a simple robot (using hardware TBD) that uses LionsOS and demonstrates true mixed criticality capability, by having time-critical control co-exist with untrusted functionality (networking) running at a high rate without interfering with the timeliness of the control.

Expected outcomes:

Simple robot demonstrating MCS
Report describing design, implementation and lessons learned.

Dynamic sDDF

Project allocated!

Labelled file system

Project allocated!

IP stack in CakeML

Supervisor: Ivan Velickovic

Abstract:

CakeML is a functional programming language with a verified compiler, making it an attractive language for implementing code that is to be verified. While it is not suitable for low-level OS components, it might be an attractive vehicle for building more high-level components for LionsOS, such as an IP stack. This project is to evaluate this possibility constructively.

Expected outcomes:

prototype implementation of an IPv6 stack in CakeML
report describing design, implementation and performance.

Using CompCert for LionsOS

Project allocated!

Core management in LionsOS

Project allocated!

Alternative network measurement clients for LionsOS

Supervisor: Peter Chubb and Lesley 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:

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.
Implementation of an iPerf client (the LWIP stack we currently use already has one)
Benchmark runs on a variety of platforms comparing the different measurement techniques
A report detailing the outcomes.

Evaluate the performance of Pancake

Supervisor: Gernot Heiser, Ivan Velickovic, Miki Tanaka

Abstract: seL4 is a strict microkernel, meaning that all OS services are implemented as user-level programs. Pancake is a new programming language under development at TS aimed at easing verification of sDDF drivers.

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. And Pancake should ease the verification of sDDF drivers.

This project is to evaluate and analyse the current Pancake language by using it to implement various OS components, compare the performance of the equivalent C implementations, and analyse shortcomings of the generated code to help the compiler developers focus on the most relevant optimisations.

Expected outcomes:

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

Auto-translation of C programs to Pancake

Supervisor: Gernot Heiser, Ivan Velickovic, Miki Tanaka

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.

Pancake is intended to be used for low-level programming, such as device drivers. It is similar to C, but is significantly simpler. While this makes it easier to verify Pancake programs, it means that writing or porting existing components to Pancake can be time-consuming.

This project aims to create a tool to automatically translate C code into a Pancake program that we would then either manually edit or directly do formal verification on.

Expected outcomes:

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

New device class for sDDF

Project allocated!

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:

Prototype implementation of a PMU object in seL4;
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;
report outlining findings.

Persistence for seL4 Microkit apps

Supervisor: Gernot Heiser and Peter Chubb

Abstract:

The seL4 Microkit and the operating system (OS) based on it that is under development in the Trustworthy Systems group. There should be a largely transparent way of providing persistence (via checkpoint/restart) for apps, possibly in a similar way as done on smartphones.

This project is to explore possible designs of such persistence support, specifically looking at the model used by iOS and Android, and examine the trade-offs involved with system-wide, transparent and consistent checkpoints vs per-application checkpoints. Provide a prototype implementation and evaluate.

Expected outcomes:

Report on a detailed exploration of design options and trade-offs.
Proof-of-concept implementation of the preferred model.

Formal Methods

Improvements to verification of seL4 Microkit

Project allocated!

Proving more functional properties for seL4's system calls

Project allocated!

SMT-based verification of Pancake device drivers via Viper

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. The verification process involves writing programs (in particular, device drivers) in Pancake, and then add annotations representing pre- and post-conditions of the verification.

Expected outcomes:

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

Pancake-to-Viper transpiler refactor

Supervisor: Miki Tanaka, Gernot Heiser

Abstract:

We have a prototype transpiler that translates annotated Pancake programs into Viper, which we then feed to SMT-backends for verification. We have used this framework to verify an Ethernet driver. In order to improve the guarantee that the framework provides, we plan to verify the correctness of the transpiler itself.

The project is to refactor and reimplement this transpiler to make it more amenable to verification. Specifically, we aim to reimplement it either in CakeML or directly in the theorem prover HOL4 (it is currently implemented in Rust), to improve its parsing phase, and to remove dependency on an external tool.

Expected outcomes:

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

Implementing choice trees in the HOL4 theorem prover

Project allocated!

Verification of security subpolicies for seL4-based OS components

Supervisors: Craig McLaughlin, 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:

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

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:

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;
report describing the approach.

Formalising and verifying device controllers

Supervisor: Miki Tanaka, Hammond Pearce, Gernot Heiser

Abstract:

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.

We have established a workflow to take an open-source hardware designs of device controllers (from the OpenTitan project, for example) and formalise its software interface in the theorem prover HOL4. We then validate the formalised model against the origial hardware design by showing the equivalence/refinement between them.

The project is to apply this workflow to produce more use cases, possibly by taking part in the on-going formalisation. We have been working on devices such as I2C and SPI so far.

Expected outcomes:

Formalisation of the device controller interface in HOL4 as a pull request to the Trustworhty Systems Group's github repository;
Report outlining the formalisation and experience with the use of verification tools.

Hardware verification using HOL4 device formalisation

Supervisor: Hammond Pearce, Miki Tanaka, Gernot Heiser

Abstract:

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.

We have established a workflow to take an open-source hardware designs of device controllers and formalise its software interface in the theorem prover HOL4. We then validate the formalised model against the origial hardware design by showing the equivalence/refinement between them. This means that properties proved about the formalised models should hold for the original hardware designs.

This project is to use such formalisations to prove properties about the hardware. The proof will be done using the theorem prover HOL4.

Expected outcomes:

Report outlining the approach taken, tradeoffs considered and work done;
Pull request to the Trustworthy Systems Group's github repository with proofs in HOL4.