Applications for summer research in Trustworthy Systems for the topics below can be made through
Project allocated!
Supervisors: Peter Chubb, Gernot Heiser
Abstract:
The project is to overcome the limitation on supported devices for seL4, by supporting the reuse of Linux drivers. This is to be achieved by providing a high-performance interface between virtual machines (VMs) on seL4 and the seL4 Device Driver framework (sDDF). This can then used to host Linux drivers in a minimal Linux kernel running inside a VM to provide device access to the sDDF. This will massively expand the set of supported devices for the seL4 ecosystem.
Expected outcomes:
Supervisors: Peter Chubb, Gernot Heiser
Abstract:
The seL4 Device Driver Framework (sDDF) is a specification and libraries for writing high-performance device drivers for systems based on the seL4 microkernel. It presently has network and storage (SDcard) drivers, but the framework itself is still fairly network-centric.
The aim of this project is to design and implement a high-perfornamce storage layer. This implies understanding the different trade-offs between network and storage, and designing an appropriate model for caching, naming and secure sharing of devices. For performance, the approach will use an asynchronous interface (very much unlike Posix). The design should also be agnostic to the underlying persistent data structure (also known as the on-medium file system) and should re-use an existing one. This will add a core system service to the seL4 ecosystem.
Expected outcomes:
Supervisor: Gernot Heiser
Abstract: The seL4 microkernel is known on the one hand for its correctness and security proofs, on the other hand for its unbeaten performance. Performance optimisations have so far targeted the critical IPC operation, and to a lesser degree signalling notification objects. While interrupt and exception handling are mapped onto notifications and IPC, respectively, they have not been optimised to the same degree.
This project is to analyse interrupt (IRQ) delivery performance and compare it to optimised notification signalling. Using the performance monitoring unit (PMU) and tracing in a simulator (QEMU), the student will analyse overheads and write or improve an IRQ fast path.
Expected outcomes:
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.
Expected outcomes:
Supervisor: Gernot Heiser
Abstract:
Development of operating-system functionality frequently involves performance analysis and optimisation. The seL4 microkernel presently has limited support for this. In particular, it is missing a gprof-like framework for performance analysis through statistical sampling. The project is to learn how statistical sampling is implemented in Linux and implement equivalent functionality on seL4, with generation of output suitable for post-processing by gprof.
Expected outcomes:
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:
Project allocated!
Supervisor: Gernot Heiser
Abstract:
Microarchitectural timing channels are a serious security threat, that 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 proof base for seL4 to account for changes made to seL4's abstract specification 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:
Supervisor: Gernot Heiser, Courtney Darville
Abstract:
The seL4 Device Driver Framework (sDDF) is a specification and libraries for writing high-performance device drivers for systems based on the seL4 microkernel. It aims to combine performance with implementation simplicity by using a highly modular design, strict separation of concerns and simple, event-based sequential module implementation. Modules communicate via lock-free, bounded, single-producer, single-consumer queues and asynchronous, semaphore-like signalling.
While the resulting module simplicity aids verification of functional correctness, it shifts some complexity into inter-module communication protocols, and these are now the leading source of implementation bugs. The aim of this project is to use model checking to verify the correct implementation of those protocols.
Expected outcomes:
Supervisor: Gernot Heiser, Zoltan Kocsis
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 Core Platform (seL4CP) is a minimal seL4-based OS aimed at embedded and cyberphysical systems. TS is presently developing a highly modularised OS based on the seL4CP, code-named KISS. It is based on the approach used for the high-performance seL4 device driver framework.
KISS's design for simplicity and strong separation of concerns mean that many of the components making up the OS have very simple implementation, which means it should be possible to verify them, ideally using “push-button” techniques based on SMT solvers. This project is to investigate the use of SMT solvers to automatically verify KISS components.
Expected outcomes:
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:
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:
Supervisor: Johannes Åman Pohjola
Abstract:
Low-level systems programming such as device driver development is tedious and error-prone. Pancake is a research programming language currently under development at Chalmers University of Technology, KTH, 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 semantics of Pancake is currently formalised as functional big-step semantics, which is convenient for compiler correctness proofs. Unfortunately, this style of semantics is awkward for verification of interactive programs such as device drivers, because it requires a fully deterministic model of the device.
The aim of this project is to develop a denotational semantics for Pancake, where the meaning of programs are represented by interactive trees. Interaction trees are a new general-purpose coinductive data structures that describes environment interactions in a branching-time style. This new semantics should be defined in the HOL4 interactive theorem prover, and proven sound and complete wrt. the existing semantics.
Expected outcomes:
Supervisor: Johannes Åman Pohjola
Abstract:
Low-level systems programming such as device driver development is tedious and error-prone. Pancake is a research programming language currently under development at Chalmers University of Technology, KTH, 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 correctness proofs use machine models that don't have great support for shared memory---they generally assume that programs have exclusive read and write access to their memory domain, and that reads and writes to memory are otherwise free of side effects. Device drivers interact with devices using memory-mapped I/O, which satisfies neither of these assumptions.
The aim of this project is to investigate ways of extending these machine models to incorporate support for memory-mapped I/O in a principled way, without hardcoding it to specific devices. Time allowing, this support should then be propagated upwards in the Pancake compiler stack and reflected in the semantics of the compiler IRs. This work will be carried out in the HOL4 interactive theorem prover.
Expected outcomes: