Taste of Research Projects

Introduction

Taste of Research (ToR) is an internship program run by the UNSW Faculty of Engineering for undergraduate students. It is accessible for 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!

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

Core management in Lions OS 

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

Formalising and verifying device controllers 

Supervisor: Hammond Pearce and 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.

The project is to take an open-source Ethernet controller from the Verilog-Ethernet repository" and, in close collaboration with the Pancake team formalise its software interface. Once successful, evaluate the use of the LUBIFIER tool for verifying the hardware implementation.

Expected outcomes:

1. Formalisation of the Ethernet controller interface in HOL4;
2. Report outlining the formalisation and experience with the use of verification tools.

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 

Supervisor: Gernot Heiser and Ivan Velickovic

Abstract:

The seL4 Microkit provides support for virtual machines (VMs) for running legacy software stacks. The present implementation has high overheads for a VM trapping into its virtual-machine monitor (VMM).

The project is to analyse the nature of VMM overheads, understand the design or implementation decisions that cause them, and improve the implementation.

Expected outcomes:

1. Improved VMM design/implementation
2. Report describing the improvements and their evaluation.

Multikernel support in Microkit

Supervisor: Gernot Heiser and 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. Among others it forms the basis of the new Lions Operating System under development at TS.

The Microkit presently supports multicore systems through the SMP (big-lock) version of seL4. For processors whose cores not all share an L2 cache, this is not an appropriate design, and a multikernel approach is required, where separate kernel images are used (per core or per cluster sharing an L2 cache).

The clustering should be mostly abstracted away by the Microkit, with inter-cluster interrupts mapping on Microkit special notifications, and a largely unchanged programming model.

Expected outcomes:

1. Bring up a (clustered) multikernel on an appropriate processor board (ideally an Orin that has two clusters);
2. Design and implement multikernel suport in the Microkit;
3. Performance evaluation;
4. Report describing design, implementation and evaluation.

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:

• USB
• SPI
• GPIO
• video capture (camera)

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:

• Adding loops to the CakeML intermediate languages, to avoid the Pancake compiler having to perform tail recursion introduction to compile loops.
• Better instruction targeting.
• Inlining support for small functions.
• Further performance characterisation of the compiler, to identify other important compiler opt imisations.

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.