Scientia Prof Heiser delivers “State of the Union” address at seL4 Summit

The 3rd seL4 Summit brought together the world-wide developer and adopter community of the seL4 microkernel. seL4 is the world’s first operating system with a mathematical proof of implementation correctness and security enforcement, and is being designed into critical systems around the world, including avionics, automotive, defence and civilian critical infrastructure. It was developed by the Trustworthy Systems (TS) group at UNSW and NICTA (now part of CSIRO).

 

Since April of this year, seL4 is backed by a Foundation, set up under the umbrella of the Linux Foundation, to ensure its longevity and accelerate its development and deployment. Prof Heiser is the founding chairman of the seL4 Foundation.

 

The seL4 Summit, originally planned to take place in Washington, DC, USA, was a virtual event with three days packed with talks and panels, from government, industry and academia, including six from TS. Prof Heiser delivered the traditional seL4 Report, dubbed “state of the union address”, on the state of the seL4 ecosystem, with a focus on the developments of the past 12 months. The two main events he highlighted were the creation of the seL4 Foundation (which was covered in more detail by a separate talk by Dr June Andronick, also from TS) and the completion of the formal correctness proof of seL4 on the new and open RISC-V processor architecture. He updated the community on the Foundation’s activities on endorsing trusted service providers, training modules and seL4-based products. And he described research activities that ensure seL4 will continue to define the state of the art in secure operating systems, especially the work on time protection, a revolutionary, principled approach to the systematic prevention of information leakage through timing channels.