Operating Systems @ SSRG

• Aim:

  The development of operating systems for reliable and trustworthy systems.

• Main expertise and projects:
  • Kernel Development:

    Focusing on development of microkernels, in particular the seL4 microkernel used in the Trustworthy Systems project.

    The seL4 microkernel is the key enabler of most of our work. It provides a minimal and efficient lowest software level, and is the only part of our software that executes in the privileged mode of the hardware. It builds on the strengths of the L4 microkernel architecture, such as small size, high performance, and policy freedom, and extends it with a built-in capability model, which provides the secure software base upon which further secure software layers can be composed to form a trustworthy embedded system.

  • Componentised Operating Systems:

    CAmkES (Component Architecture for Microkernel-Based Embedded Systems): is a framework for building efficient medium- to large-sized software systems on top of a microkernel. It leverages the provable protection and isolation properties of the underlying kernel.

  • Device Drivers:

    Reliable device drivers are essential to building a reliable OS. We are exploring three different approaches to improving the reliability of device drivers:

    • Dingo: untangling the interface between device drivers and the OS.
    • Hardware/Software Co-Verification: integrating driver development and testing in the hardware design and verification workflow.
    • Termite: automatic synthesis of device drivers from device specifications.
  • Real Time Systems:

    Many critical systems have stringent timing requirements in addition to the need for functional correctness. We are looking at the intersection of real-time guarantees and verifiability to satisfy these requirements.

  • Virtualisation:

    Virtualisation supports the safe co-existence of large legacy systems with critical sub-systems on the same device and is developing into a major enabler for the design of embedded systems with rich functionality.

  • Power Management:

    Power management looks to improve the energy efficiency of computer systems by using advanced operating-system level techniques.

• Read more: Publications
• Contact: Gernot Heiser, gernot.heiser<at>nicta.com.au