Applications for summer research in Trustworthy Systems for the topics below can be made through
Supervisor: Peter Chubb and Lucy Parker
Abstract:
The high-performance I/O system for seL4, based on
the seL4 device driver framework
(sDDF) and the lwip protocol stack, is presently
highly optimised for UDP traffic (outperforming Linux) but not for
TCP. The project is to measure and analyse TCP performance, identify
bottlenecks and improve or rewrite the respective functionality
of lwip and possibly other parts of the system.
Expected outcomes:
Supervisor: Gernot Heiser and Peter Chubb
Abstract:
The high-performance I/O system for seL4, based on the seL4 device driver framework (sDDF), is designed for minimal overheads and thus uses asynchronous interfaces. This project is to design and implement an easier-to-use, Posix-style blocking interface for programmers who prefer this simplified (but less efficient) API.
Expected outcomes:
Supervisor: Gernot Heiser and Ivan Velickovic
Abstract:
The seL4 Core Platform (seL4CP) supports statically-architected systems on seL4 and is designed to serve the needs of embedded and cyberphysical systems. However, some of such systems need the ability to load applications whose resource needs and access rights are not known at system-configuration time.
To support such applications, this project is to provide a notion of protection domain (PD) templates, which are configured for maximum access and can be loaded with actual application code that is not part of the original system configuration. The template is initialised with a trusted loader, which is pointed at the actual app to be loaded. The app contains a signed header that specifies its authorised access. The trusted loader interprets that section, removes non-authorised access rights, and then loads and executes the actual target app. When the app exits, the template is re-set to its original state.
Expected outcomes:
Supervisor: Peter Chubb and Ivan Velickovic
Abstract:
The seL4 Core Platform (seL4CP) provides support for virtual machines (VMs) for running legacy software stacks. At present, these need to be packaged with the seL4CCP boot image. This project is to provide support for booting a VM from a separate disk image (possibly across a network) containing a standard Linux distribution.
Expected outcomes:
Supervisor: Gernot Heiser and Ivan Velickovic
Abstract:
The seL4 Core Platform (seL4CP) 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:
Supervisor: Gernot Heiser and Peter Chubb
Abstract:
The seL4 Core Platform (seL4CP) 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:
Supervisors: Gernot Heiser, Ivan Velickovic
Abstract:
The seL4 Core Platform (seL4CP) 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:
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: 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, 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:
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.
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 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:
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.
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.
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:
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.
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.
When writing drivers in the seL4 device driver framework, the need sometimes arises to suspend an action and complete it later. For this, native language support for a continuation-like mechanism would be handy. This project is to extend the Pancake language with such a feature.
Expected outcomes:
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.
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.
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:
Supervisors: Gernot Heiser, Robert Sison
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
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: