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

Device Manager for Djawula NEW

Supervisor: Gernot Heiser, Szymon Duchniewicz

Abstract:

Djawula is an seL4-based fully dynamic, general-purpose operating system under development at TS. Unlike the reasonably mature LionsOS, which has a static architecture, Djawula supports the security policy and system architecture to evolve at runtime. This requires support for enabling, disabling and configuring device drivers at runtime.

The aim of this project is to develop a device manager, similar to the one of Haiku OS, for dynamically managing seL4 device drivers. It needs to be integrated with Djawula's security enforcement and dynamically connect and disconnect clients to drivers.

Expected outcomes:

  1. design, implementation and evaluation of a device manager for seL4 device drivers in Djawula;
  2. report describing the above.

Secure Point-of-Sale Reference System NEW

Supervisor: Gernot Heiser, Lesley Rossouw

Abstract:

The TS group has a simple point-of-sale system implemented on top of LionsOS. This project is to revisit its architecture from the security point-of-view, including minimising the trusted computing base (TCB) and investigate feasibility of verifying the TCB. Options to investigate include implementing the business/accounting logic in a verification-friendly language (Pancake or CakeML) and using scalable verification approaches under investigation in TS.

Expected outcomes:

  1. Report describing the evaluation, proposed design/implementation and take-aways;
  2. any design, implementation and verification artefacts resulting from the above.

OS support/virtualisation of Vulkan and OpenGL

Project allocated!

Zephyr-compatible API for LionsOS NEW

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:

  1. 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).
  2. Report describing the above.

ARINC-653 OS on seL4

Supervisor: Gernot Heiser, Courtney Darville

Abstract:

ARINC 653 (Avionics Application Software Standard Interface) is a software specification for space and time partitioning in safety-critical avionics real-time operating systems.

A recent honours thesis explored mapping of ARINC-653 scheduling and communication abstractions onto the seL4 Microkit. This project is to continue that work to develop a complete ARINC 653 OS environment. This mostly involves developing application libraries on top of LionsOS to provide ARINC-653-compatible APIs.

Expected outcomes:

  1. 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).
  2. Report describing the above.

Feasibility of seL4 implemented in Pancake NEW

Project allocated!

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:

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:

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

Auto-translation of C programs to Pancake

Project allocated!

New device classes for sDDF

Project allocated!

VMM environment for developing Microkit applications on Linux

Project allocated!

Project allocated!

 

Formal Methods

Improvements to Viper-based verification of seL4 Microkit NEW

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:

  1. Report describing experience verifying the latest Pancake language version of the seL4 Microkit library using the Viper-based workflow;
  2. Pull requests against the seL4 Microkit library's implementation and continuous integration testing framework;
  3. 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 NEW

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

  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 NEW

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:

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.

Enhancing Pancake parser with more PEG features NEW

Supervisor: Miki Tanaka, Thomas Sewell, Michael Norrish

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.

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:

  1. Report outlining the approach taken, tradeoffs considered and work done;
  2. 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 NEW

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:

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

Linking Pancake annotations to a Hoare Logic NEW

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

  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

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:

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