Trustworthy Systems

Taste of Research (ToR) Project Proposals

Applications

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

Projects

 

Operating Systems

Evaluate the overheads of using the IOMMU to encapsulate device drivers

Project allocated!

Evaluate dynamic seL4CP featuresNEW

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:

  1. Sample code demonstrating the use of the seL4CP dynamic features for realistic uses;
  2. Written report of a critical assessment of usability and performance of the seL4CP.

Reuse of unmodified Linux device drivers on seL4NEW

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:

  1. Design of a high-performance, asynchronous interface between VMs and sDDF, based on the Linux virtIO standard;
  2. Implementation of such an interface for one or more device classes, including at least network devices, and optionally storage, frame buffer, USB;
  3. performance evaluation and analysis;
  4. written report describing design, implementation and performance evaluation and comparison with Linux performance.

Native file service on seL4NEW

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:

  1. extension of the sDDF design to storage services, with an asynchronous client interface;
  2. implementation of the design that works on an Arm-based development board;
  3. performance evaluation and analysis;
  4. written report describing design, implementation and performance evaluation and comparison with Linux performance.

Optimise the seL4 IRQ fastpath

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:

  1. report describing the analysis of the IRQ code path, comparing with notification-object signalling, and optimisations based on comparison to signalling; detailed benchmarks;
  2. pull request against the seL4 kernel mainline.

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.

Expected outcomes:

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

Profiling framework for seL4

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:

  1. Gprof-like library for statistical sampling
  2. Tool that mangles the collected data into a form that can be processed by gprof

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:

  1. 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.
  2. Report outlining the experience with Pancake, discussion of limitations and other shortcomings, and suggestions for improvement.

Optimise seL4 cold-cache / worst-case performance

Project allocated!

 

Formal Methods

Automatic verification of the seL4 Core platformNEW

Supervisor: 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. The seL4CP is intentionally kept lean and simple, to minimise overheads while ensuring correct use of seL4 mechanisms.

Its simplicity should enable verification of the seL4CP, extending seL4's assurance to the complete OS. This project is to investigate the use of SMT solvers to automatically verify the seL4CP implementation. The main challenges will be to formally specify the seL4CP API, and tweak the SMT problem, as well as the seL4CP implementation for verification to succeed.

Expected outcomes:

  1. report describing experience verifying the seL4CP using an SMT solver;
  2. formal specification of at least a significant part of the seL4CP;
  3. successful verification of at least a subset of the specified functionality;
  4. potentially pull requests against the public seL4CP source.

Updating seL4's proof codebase for Time ProtectionNEW

Supervisors: Gernot Heiser, Scott Buckley, 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:

  1. completing the time protection breakages in the abstract specification proofs for seL4;
  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.

Model-checking inter-module communication of the seL4 driver frameworkNEW

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:

  1. Verified model of the signalling protocol of the seL4 networking system built on sDDF, proving deadlock-freedom, liveness as well as (stretch goal) more stringent progress properties;
  2. Automatic extraction of the model from the C implementation of the sDDF (stretch goal) or at least an informal argument that the model represents the code;
  3. Report describing the model and the verification.

Automatic verification of seL4-based OS componentsNEW

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:

  1. formal specification of at least one KISS component
  2. successful verification of at least a subset of the specified functionality
  3. report describing experience verifying an OS component using SMT solvers
  4. potentially pull requests against the KISS implementation

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

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:

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

Automating Reasoning about Memory Safety for the Pancake LanguageNEW

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:

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

Interaction tree semantics for Pancake

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:

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

Formal machine models for memory-mapped I/O

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:

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