Trustworthy Systems

Zircon on seL4

Authors

Jack Suann

    School of Computer Science and Engineering
    UNSW,
    Sydney 2052, Australia

Abstract

seL4 is a high-performance microkernel with a proof of functional correctness, providing isolation guarantees to properly designed applications. This makes it suitable for systems where strong security guarantees are required. Despite these benefits, seL4 lacks the support of other major operating systems, and manually porting the drivers and applications from such systems is often too expensive of a solution. A more feasible approach is to re-use components of these systems and port them on seL4, providing an environment for applications that matches the specifications of the original system.

This thesis presents Zircon on seL4, a port of Google’s new Zircon microkernel to seL4. This is achieved using an API emulation approach, with a seL4 application managing Zircon kernel objects, and handling syscalls from Zircon applications that are delivered using seL4’s IPC mechanisms.

This thesis details the kernel objects and syscalls that have been implemented in this port, and how they interact with the primitives provided by seL4. This implementation is evaluated in terms of performance and porting effort. Finally, an analysis of the the future work that remains to be done to fully support dynamic user-level Zircon-based systems on seL4 is given.

BibTeX Entry

  @mastersthesis{Suann:be,
    address          = {Sydney, Australia},
    author           = {Jack Suann},
    month            = may,
    paperUrl         = {https://trustworthy.systems/publications/theses_public/18/Suann%3Abe.pdf},
    school           = {School of Computer Science and Engineering},
    title            = {Zircon on {seL4}},
    year             = {2018}
  }

Download