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
Run-time reloading of LionsOS systems
Project allocated!
Better debugging tools for LionsOS
Supervisor: Ivan Velickovic, Julia Vassiliki
Abstract:
LionsOS is a new seL4-based OS for embedded systems under development at TS. LionsOS isolates programs more than conventional Operating Systems and relies a lot more on asynchronous communication. Current tools used for debugging on conventional OSes are more limited for our use case.
Current tools such as GDB are not equipped to debug our kind of architecture and so certain bugs that happen between process boundaries or rely on the scheduling of a system can be difficult to catch and fix.
This project is to explore other ways of debugging system-wide execution such as scheduling and inter-process communication. This will involve looking at more modern tools such as rr as well as tracing infrastructure available in other OSes.
Expected outcomes:
- Porting an existing or creating a new tracing framework to give us more introspection into systems built on LionsOS.
- Evaluate and investigate the feasibility of a record-and-replay debugger, such as RR.
Analyse and optimise driver VMs
Project allocated!
Deployable firewall based on seL4
Supervisor: Peter Chubb, Courtney Darville
Abstract:
The TS group has just 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.
Native USB stack
Project allocated!
LionsOS-based robot demonstrating hard real-time capabilities
Project allocated!
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
Project allocated!
Persistence for seL4 Microkit apps
Project allocated!
Formal Methods
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
Project allocated!
Implementing choice trees in the HOL4 theorem prover
Project allocated!
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.