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.


Computer Science and Engineering

Research Area

Operating systems

The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.

  1. Improved VMM design/implementation
  2. Report describing the improvements and their evaluation.
Scientia Professor and John Lions Chair Gernot Heiser
Scientia Professor and John Lions Chair