Taste of Research (ToR) Projects

Applications

Applications for summer research in Trustworthy Systems for the topics below can be made through

UNSW Faculty of Engineering Taste of Research Scholarships program.

For students interested in a ToR commencing in T2 or T3 2024 there will be an information session at 12.30 on Mon, 8 April in the CSE Seminar room (K17-113). Please let us know in advance if you're planning to attend.

Operating Systems

WCET Analysis of seL4 on RISC-V

Supervisor: Gernot Heiser

Abstract:

The seL4 microkernel was the first (and seemingly only) protected-mode real-time operating system kernel that underwent a complete and sound worst-case execution-time analysis (WCET analysis). This work was performed on a long obsolete Armv7 processor, using a tool chain that is also obsolete.

This project is to investigate re-doing this work for 64-bit RISC-V processors, using a state-of-the-art, open-source tool, Otawa. Specifically, it is to trial Otawa on some simple code example, and then progress to actual kernel code, starting with a subset of the seL4 kernel.

Expected outcomes:

WCET results for at least a subset of the seL4 kernel code;
Report describing experience, achievements, challenges and limitations of using Otawa on real-world kernel code.

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:

Prototype implementation of dynamic IOMMU mappings;
Performance evaluation;
Report describing the above.

Evaluate queueing performance 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 presents a highly modular design with policy isolated in individual components (as well as overall configuration parameters). It is not a-priori clear that such a simple design will provide good performance under all circumstances; other systems implement feedback loops to tune performance aspects dynamically.

This project is to stress and analyse the queueing behaviour of I/O data in sDDF networking, using extreme cases, such as a low-priority client degrading service to high-priority clients by generating excessive input traffic. It should try to answer the question of whether existing parameters (queue sizes, priorities, budgets and virtualiser-implemented queue-processing policies) are sufficient to handle extreme cases, including malicious clients that collude with external data sources.

Expected outcomes:

Thorough evaluation of sDDF under stress, using the existing policy parameters;
Report describing the evaluation, and learnings about the suitability of the existing approach, and, if appropriate, suggestions on how to improve it.

Evaluate active vs passive components in sDDF

Supervisor: 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 location-transparent, asynchronous shared-memory-based communication between components. Components are presently implemented as seL4 active servers and seL4 Notifications.

This project is evaluate an alternative approach, namely using passive servers invoked by protected procedure calls. This forces the server to execute on the caller's core, but uses a more efficient seL4 system call. The trade-off is not obvious and will likely depend on multiple aspects of the system.

Expected outcomes:

Thorough evaluation of sDDF using the passive-server model for some components, such as copiers.
Report describing the evaluation, and the proposed design.

Support for hot-plugging devices 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 presents a highly modular design with location-transparent, asynchronous shared-memory-based communication between components. The sDDF is presently fully static, which iss sufficient for supporting a large class of embedded systems.

However, hot-pugging/unplugging devices, long a standard requirement for laptop and desktop computers, is also increasingly required in some embedded/cyberphysical systems. For example, devices (eg wifi) may need to be turned off to conserve energy, SD cards may be inserted for adding or upgrading software components, or USB device may be connected for maintenance.

This project is to propose, design, implement and evaluate support for hot-plugging in the sDDF.

This project requires an Advanced Operating Systems background.

Expected outcomes:

A design, prototype implementation and evaluation of dynamically adding/removing devices in the sDDF;
Report describing the design, implementation and evaluation.

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:

Prototype implementation of a PMU object in seL4;
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;
report outlining findings.

VMM environment for developing Microkit applications on Linux

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.

Persistence for seL4 Microkit apps

Supervisor: Gernot Heiser and Peter Chubb

Abstract:

The seL4 Microkit and the operating system (OS) based on it that is under development in the Trustworthy Systems group. There should be a largely transparent way of providing persistence (via checkpoint/restart) for apps, possibly in a similar way as done on smartphones.

This project is to explore possible designs of such persistence support, specifically looking at the model used by iOS and Android, and examine the trade-offs involved with system-wide, transparent and consistent checkpoints vs per-application checkpoints. Provide a prototype implementation and evaluate.

Expected outcomes:

Report on a detailed exploration of design options and trade-offs.
Proof-of-concept implementation of the preferred model.

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:

Sample code demonstrating the use of the Microkit dynamic features for realistic uses;
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:

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

Evaluate Pancake for implementing device drivers

Supervisor: Gernot Heiser, Johannes Åman Pohjola

Abstract: seL4 is a strict microkernel, meaning that all device drivers are user-level programs, as are network protocol stacks and file systems. The seL4 device driver framework (sDDF) is designed to simplify implementation of high-performance drivers for seL4. Pancake is a new programming language under development at TS aimed at easing verification of sDDF drivers.

The Pancake language itself is still under development. This project is to evaluate the current Pancake language by using it to implement drivers of various complexity and providing feedback to the language developers.

Expected outcomes:

Sample device drivers and other sDDF components written in Pancake. Desirable targets are Ethernet and SD-card drivers and sDDF modules such as a multiplexer.
Report outlining the experience with Pancake, discussion of limitations and other shortcomings, and suggestions for improvement.

Formal Methods

Implementing and verifying Pancake compiler improvements

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

The compiler is an optimising compiler going throgh 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.
Adding support for string literals to the language.
Better instruction targeting.

These are just examples; the precise contents of this topic needs to be negotiated with the supervisors.

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.

Multiple entry points for Pancake

Supervisor: Johannes Åman Pohjola, Miki Tanaka, Gernot Heiser

Abstract:

seL4 is a microkernel, meaning that all device drivers are user-level programs, as are network protocol stacks and file systems. Low-level systems programming such as device driver development is tedious and error-prone.

The Pancake runtime expects to be the main function of a binary. But when writing drivers in the seL4 device driver framework, the need arises to use Pancake as a library, where other programs can call specific entry points and then gain back control. This project is to invent and implement an approach to supporting such entry points in a principled, low-cost and verifiable way. As a stretch goal, this work would be fully integrated into the Pancake compiler stack and verified.

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.

A ring buffer library for Pancake

Supervisor: Johannes Åman Pohjola, Miki Tanaka, Gernot Heiser

Abstract:

Interaction between device drivers and the seL4 device driver framework (sDDF) is mediated through a communication protocol where synchronisation happens via a set of shared ring buffers. Since this is necessary for any driver written in Pancake for sDDF, it would be desirable to have a verified library that abstracts away this protocol. This project is to develop and verify such a library.

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.

Connection interaction trees and state machines

Supervisor: Johannes Åman Pohjola, Miki Tanaka, Gernot Heiser

Abstract:

Weaving together a proof story that connects device drivers written in Pancake with devices and the seL4 device driver framework requires interfacing between interaction trees (the semantic domain of Pancake programs) and traditional labelled transition systems (that model devices). The aim of this project is to explore the theory and practice of how to make this connection. This may involve working on topics including but not limited to automata theory, concurrency theory, interactive theorem proving, and model checking; exploring the tradeoffs between different approaches is part of the project.

Expected outcomes:

Report outlining the approach taken, tradeoffs considered and work done.
A case study of applying the approach to the verification of a simple serial driver.

Verification of security subpolicies for seL4-based OS components

Supervisors: Robert 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 implementation, 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 solvers 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:

formal specification of a security subpolicy for one Lions OS component;
successful verification of the subpolicy for at least a subset of the anticipated cases;
report describing experience verifying security subpolicies for an OS component using SMT solvers;
potentially pull requests against the Lions OS implementation.

Update seL4's abstract specification proofs for Time Protection

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

This project is to contribute to updating the proofs about seL4's abstract specification 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:

updates to the abstract specification proofs for seL4 where time protection invalidates existing proofs;
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: Robert Sison, Gernot Heiser

Abstract:

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.

Expected outcomes:

updates to the ESpec refinement proofs for seL4 where time protection invalidates existing proofs;
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:

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.

A Hoare-Like Logic for the Branching-Time I/O behaviour of Non-Terminating Programs

Supervisor: Johannes Åman Pohjola

Abstract:

Low-level systems programming such as device driver development is tedious and error-prone, and device driver bugs are one of the leading sources of cybersecurity vulnerabilities in operating systems. Formal verification of device drivers can address this issue, but traditional device drivers have at least two features that make traditional deductive verification techniques such as Hoare Logic inapplicable: device drivers aren't meant to terminate (so what's the post-condition?), and the state of the driver are less interesting than its interaction with the device and O/S (so what use would a post-condition be anyway?).

Interaction trees is a recent denotational semantics model that addresses both of these concerns, by representing the semantics of a program as an infinite tree, whose nodes are I/O events and whose branches represent possible responses by the environment. To make reasoning about interaction trees scalable, a Hoare-like logic that can prove branching-time properties about interaction trees is needed.

The aim of this project is to develop just such a logic. It should be formulated, and ideally proven sound, in the HOL4 interactive theorem prover.

This work occurs in the context of the broader Pancake project. 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.

Expected outcomes:

Pull request against the CakeML repository with definitions and proofs.
Report outlining the work undertaken.

Automating Reasoning about Memory Safety for the Pancake Language

Supervisor: Johannes Åman Pohjola

Abstract:

Low-level systems programming such as device driver development is tedious and error-prone, and device driver bugs are one of the leading sources of cybersecurity vulnerabilities in operating systems. 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, ease of verification and the right expressive power for low-level systems programming.

Pancake is designed to avoid some of the pitfalls involved in C, the de-facto standard systems programming language, that make systems code hard to verify. For example, expressions are free of side-effects, programs are single-threaded, and memory is flat and statically allocated. The semantics of a memory access outside this statically allocated region is to fail; however, this is not enforced at runtime because the performance overhead of bounds checks is undesirable.

Ideally, full formal verification of a Pancake program will address memory safety anyway, because a memory-unsafe program cannot be shown to not fail. Even more ideally, the proof engineer should not be burdened with this task. prover.

The aim of this project is to prototype a way of automating proofs of memory safety for Pancake programs. This can be done in different ways: for example, by developing a type system that implies memory safety, or by developing tactics and algoritms for proof automation. Assessing these tradeoffs is part of the project. Any output should be formulated, and ideally proven sound, in the HOL4 interactive theorem prover.

Expected outcomes:

Pull request against the CakeML repository with definitions and proofs.
Report outlining the work undertaken.