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

Operating Systems

OS support/virtualisation of Vulkan and OpenGL

Project allocated!

Zephyr-compatible API for LionsOS

Supervisor: Gernot Heiser

Abstract:

Zephyr is a small real-time operating system for connected, resource-constrained and embedded devices. It's popularity make 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.

Expected outcomes:

Design, implementation and evaluation of a Zephyr-compatible API on top of Lions (with liberal re-use of Zephyr code (as permitted under its permissive license).
Report describing the above.

Feasibility of seL4 implemented in Pancake

Supervisor: Gernot Heiser

Abstract:

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 project 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, as covered in COMP9242.

Expected outcomes:

Prototype implementation of critical parts of the seL4 kernel, at least the IPC, Notification and interrupt fastpath, with missing functionality provided by C code (invoked via FFI).
Evaluation of fastpath performance compared to the original C version.
Report describing experience and performance.

Deployable firewall based on seL4

Supervisor: Peter Chubb, Courtney Darville

Abstract:

The TS group has developed a proof-of-concept of a secure network firewall running on the verified seL4 microkernel and LionsOS. Currently the firewall supports the transmission of traffic between two network interfaces, and is able to apply simple filtering rules to a subset of IP traffic (TCP, UDP, ICMP). Filtering rules and forwarding routes may be viewed and updated through a rudimentary web interface. Presently it has a number of missing features that prevent its practical use, with each feature requiring a varying degree of work to implement. While we are happy to leave most of them to the open-source community, we are looking for interns for the higher priority ones. These are:

Support for IPv6, as well as more IP protocols and ethernet types
A collection of optimised, concurrency-safe data structures which can be used by firewall components for reading and updating shared network state (e.g. NAT port mappings, TCP connection)

If there is sufficient time left after the above, the rest can be spent on improvements to existing features or adding further functionality, with the ultimate aim of enabling the firewall to be deployed on the TS network.

Expected outcomes:

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

Auto-translation of C programs to Pancake

Project allocated!

New device classes for 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 presents a highly modular design with a (compared to Linux) much simplified driver model.

The sDDF presently specifies driver interfaces for a number of device classes, this project is to contribute another class. Of specific interest are:

HID devices
video capture (camera)

Expected outcomes:

specification of sDDF driver interfaces;
implementation – depending on the device class and the complexities of the interface, this could be a native driver written from scratch, a native driver ported from a different OS, or a a driver embedded in its normal OS running as a guest in a virtual machine on top of seL4 (a “driver OS”);
performance evaluation (keeping in mind that a driver OS will have limited ability to test the performance limits of the design).

VMM environment for developing Microkit applications on Linux

Project allocated!

Supervisor: Peter Chubb and Ivan Velickovic

Abstract:

The seL4 Microkit provides a simple programming model for seL4-based systems, aimed at supporting embedded systems. Developing directly on an embedded platform restricts the available tools, and it would be preferable use a full Linux environment for development.

There exists a rudimentary library for emulating Microkit interfaces on Linux, using UIO to map sDDF shared memory into the space, and to map between notification events and Linux IRQs. There also exists the ability to pass a block device through to a Linux VMM. This leaves the following tasks:

maturation of the library including (synchronous) protected procedure calls;
inclusion of simple ways to map device registers and IRQs into UIO;
actual use cases of drivers developed using this framework.

Expected outcomes:

A framework that allows using a standard editor, make, GCC, and GDB inside a Linux VMM to build and debug components that can then be deployed natively.
Report describing the system.

Formal Methods

Improvements to Viper-based verification of seL4 Microkit

Supervisors: Rob Sison, Zoltan Kocsis, 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 key functionality of the Microkit's original C implementation using an in-house SMT solver-based framework, research at TS has been exploring the use of a new SMT solver-based automated deductive verification workflow based on transpilation to Viper to verify new Pancake language implementations of the Microkit library and Microkit-based OS components in a more scalable manner.

This project is to continue bringing the verification of the seL4 Microkit library up to date using this workflow and integrate them into the Microkit's continuous integration testing framework.

Expected outcomes:

Report describing experience verifying the latest Pancake language version of the seL4 Microkit library using the Viper-based workflow;
Pull requests against the seL4 Microkit library's implementation and continuous integration testing framework;
Verification of some simple Microkit-based example systems added to the CI testing framework if time allows.

Proving more functional properties for seL4's system calls

Project allocated!

Proving even more functional properties for seL4's system calls

Supervisors: Rob Sison, Gernot Heiser

Abstract:

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 is now underway 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, continuing to focus 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:

Verification of a Microkit-relevant functional property for at least one seL4 system call;
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, Thomas Sewell

Abstract:

Pancake is a research programming language for systems programming 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:

Multiple file compilation for Pancake.
Support division.
Support field updates to structs.
Further performance characterisation of the compiler, to identify other important compiler optimisations.

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:

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

Enhancing Pancake parser with more PEG features

Supervisor: Miki Tanaka, Thomas Sewell, Michael Norrish

Abstract:

PEG (parsing expression grammar) is an expressive formalism for defining machine-oriented syntax that allows for parser generation. The current frontend, i.e., the parser for the concrete syntax, of the Pancake compiler uses the PEG as its core, but it does not leverage all of the features that PEG provides.

This project is to reimplement the Pancake parser to use more of the PEG advantages to improve the parser performance and the maintainability, possibly by improving the HOL4 PEG library.

Expected outcomes:

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

SMT-based verification of Pancake device drivers via Viper

Project allocated!

Pancake-to-Viper transpiler refactor

Project allocated!

Investigating alternative verification backends for Pancake transpiler

Supervisor: Miki Tanaka, Gernot Heiser

Abstract:

Pancake is a research programming language for systems programming 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 a transpilation tool ("transpiler") that converts annotated Pancake code into Viper, an intermediate language for an SMT-backend. Using this transpiler, we have verified some properties of device drivers written in Pancake, with annotations stating the necessary conditions.

The aim of this project is to investigate the possibility of alternative transpiler backends, such as Why3, for this verification framework. This will involve assessing the advantages and disadvantages over Viper, as well as the feasibility of hybrid verification (of SMT-based and interactive verification).

Expected outcomes:

Report outlining the approach taken, discoveries and conclusions of the investigation;
Pull request to the Trustworthy Systems Group's github repository (if applicable).

Linking Pancake annotations to a Hoare Logic

Supervisor: Miki Tanaka, Gernot Heiser

Abstract:

We have a transpilation tool ("transpiler") that converts annotated Pancake code into Viper, an intermediate language for an SMT-backend. These annotations encode the pre- and post-conditions that specify the behaviour of the Pancake code in a pseudo-Viper syntax. We then verify that the code correctly implements the specification by sending the transpiled Viper files to the SMT-backend.

The aim of this project is to explore the ways to represent these annotations directly in HOL4 interactive theorem prover, most likely as a Hoare logic. This work can leverage the currently on-going work on Viper semantics in HOL4, which is likely to provide a basis for semantics for annotated Pancake.

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!

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.