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 Linux I/O Performance Degradation

Project allocated!

Native web server for sel4.systemsNEW

Project allocated!

Evaluate the overheads of using the IOMMU to encapsulate device driversNEW

Supervisor: Peter Chubb, Gernot Heiser

Abstract:

Bus-mastering DMA devices in modern computer systems are attached via a memory-management unit, called IOMMU or System MMU (SMMU) depending on the manufacturer. The IOMMU that can control which physical memory regions a device may access. As such, it presents an important mechanism for encapsulating untrusted devices and their drivers.

To make best use if the IOMMU, the device should only be able to access the absolute minimum portion of RAM, specifically the region(s) containing the buffer the device is to read or write. This required re-programming the IOMMU mappings for every I/O. However, this can introduce substantial overheads [Malka et al, FAST'15], leading to security-performance tradeoffs.

This project is to evaluate IOMMU performance trade-offs on recent x86 and Arm processors, and answer the following research questions:

Expected outcomes:

  1. Benchmarking setup that allows evaluating IOMMU overheads on Linux.
  2. Report describing the evaluation results on multiple platforms and proposing a way forward for secure I/O encapsulation on seL4.

Improve the seL4 benchmarking methodologyNEW

Project allocated!

Evaluate Pancake for implementing driversNEW

Project allocated!

Native support for persistent storage on seL4NEW

Project allocated!

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

Optimise seL4 cold-cache / worst-case performance

Project allocated!

 

Formal Methods

Automatic verification of the seL4 Core PlatformNEW

Project allocated!

Interaction tree semantics for PancakeNEW

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/ONEW

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.