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

IDL compiler for general-purpose OS NEW

Project allocated!

Dynamic sDDF NEW

Project allocated!

Labelled file system NEW

Supervisor: Alwin Joshy and Gernot Heiser

Abstract:

The Secure general-purpose OS should have trusted servers that support clients from different security domains. This means that the objects provided by the server must be labelled with the client's security context, so that accesses can be authorised according to the system's security policy. This project is to develop a file server of this kind.

Expected outcomes:

  1. labelled file-server prototype
  2. report describing design, implementation and performance.

Make Time Protection Realistic NEW

Supervisor: Rob Sison and Gernot Heiser

Abstract:

Our work on Time Protection aims to provably eliminate microarchitectural timing channels. A proof-of-concept implementation in seL4 is present undergoing verification. However, this implementation has two shortcomings, which this project is to address:

Expected outcomes:

  1. model for properly dealing with shared kernel state, and its implementation;
  2. stretch goal: model and implementation of shared-memory communication and synchronisation without back-channels;
  3. report describing design, implementation and performance.

IP stack in CakeML NEW

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 Lions OS, such as an IP stack. This project is to evaluate this possibility constructively.

Expected outcomes:

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

Using CompCert for LionsOS NEW

Supervisor: Ivan Velickovic

Abstract:

Some Lions OS components as well as the underlying Microkit have been verified using SMT solvers, which is far less effort than the interactive theorem proving approach used for seL4. However, that requires trusting the complex (and buggy) GCC compiler.

The TCB would be greatly reduced by using the verified C compiler. This project is to evaluate the practicability of using CompCert for LionsOS and compare the performance of the generated code with C and Pancake.

Expected outcomes:

  1. report describing results.

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

Supervisors: Peter Chubb and Gernot Heiser

Abstract:

A processor core consumes energy, whether it is doing useful work or not, unless it is in a “deep sleep” state. Transitioning into or out of such sleep states takes time (and energy), making a pure core-local energy management inefficient. Instead the OS should aim to maximise the period cores are in deep sleep. This requires monitoring overall CPU utilisation, and off-lining lowly utilised cores by migrating their activities to other cores.

The structure of LionsOS supports this approach: It has a highly modular design, with individual modules strictly sequential (executing on a single core) and modules communicating via shared memory, synchronised by semaphores. This means most modules are completely location transparent and can easily be migrated to a different core.

The aim of this project is to design and implement the mechanisms for core migration in the seL4 Microkit, which is the framework in which Lions OS is implemented. Depending on progress, the next step would be to implement a core manager, which monitors load an consolidates or spreads activities as required by load.

Expected outcomes:

  1. Report outlining the design, challenges, implementation and evaluation of core management in LionsOS;
  2. implementation on top of the Microkit;
  3. pull requests against Microkit/LionsOS as appropriate.

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.

Formalising and verifying device controllers

Project allocated!

ARINC time-partitioned scheduling on seL4 MCS

Project allocated!

“Containers” on LionsOS

Supervisor: Gernot Heiser

Abstract:

Containers are a hack that attempts to provide isolation similar to virtual machines at lower cost, by working around the lack of principled resource managements in mainstream OSes, such as Linux. In a lean and highly efficient OS such as LionsOS, the standard process abstraction should be lightweight enough to achieve strong isolation.

This project is to design and implement support for container-like domains on LionsOS and evaluate them against Linux containers.

Expected outcomes:

  1. Report describing the container model design, implementation and evaluation
  2. open-source code

Analyse and improve virtualisation performance on seL4 Microkit

Project allocated!

Multikernel support in Microkit

Project allocated!

New device class for sDDF

Supervisor: Peter Chubb and Gernot Heiser

Abstract:

The seL4 Device Driver Framework (sDDF) provides the basis for high-performance I/O in Lions OS, 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:

Expected outcomes:

  1. specification of sDDF driver interfaces;
  2. 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”);
  3. performance evaluation (keeping in mind that a driver OS will have limited ability to test the performance limits of the design).

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 Lions OS, 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.

Performance analysis of stub code overhead in client-server interaction on seL4

Supervisor: Kevin Elphinstone

Abstract:

The seL4 microkernel is known not only for its comprehensive formal verification story but also for being the benchmark for microkernel IPC performance. However, for the cost of protection in client-server interactions in a secure OS, the code required to marshal parameters to the IPC system call is also a factor. This project is to evaluate the performance cost of these stubs and the potential for the compiler optimising them away on bare seL4. In a second step, this analysis is to be extended to the interfaces required for the CAmkES framework. If there is time, look at the potential for generating efficient stubs from an interface generator.

This project requires an Advanced Operating Systems background.

Expected outcomes:

  1. Report describing the results of the performance analysis
  2. Potentially pull requests against the libsel4 repository for optimised stub code

 

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: Thomas Sewell, Miki Tanaka, Johannes Åman Pohjola

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.

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 Lions OS, using the same, highly-modular design as the seL4 Device Driver framework (sDDF).

Lions OS 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 Lions OS 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 Lions OS 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 Lions OS, 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.