seL4 Summit gathers the global seL4 ecosystem

The seL4 microkernel, developed by UNSW and NICTA researchers, incl A/Prof Kevin Elphinstone and Scientia Professor Gernot Heiser, is the world's first operating system (OS) kernel with a mathematical proof of implementation correctness. Open-sourced since 2014, seL4 is deployed in defence systems and an increasing number of civilian applications and is supported by a vibrant ecosystem.

On 10-13 October, 70 members of this ecosystem from around the world gathered in Munich, Germany, for the 4th seL4 Summit. Not only was this the first Summit outside the US, and it was the first organised by the international seL4 Foundation, created in 2020 and chaired by Gernot.

The four-day program consisted of two keynotes and 16 technical talks by developers and adopters of seL4 technology. Six birds-of-a-feather and discussion sessions focussed on open issues and led to the creation of several special interest groups (SIGs) aiming to develop concrete proposals for standardisation and future work directions. The final day was a "bootcamp" with hands-on tutorials on getting started with seL4 and various seL4-based development frameworks.

CSE's Trustworthy Systems (TS) Group was well represented, with a keynote and a second talk by Gernot, technical talks by 3rd-year student Lucy Parker and Lecturer Zoltan Kocsis, and a tutorial on the new seL4 Core Platform presented by TS research assistant Ivan Velickovic. TS postdocs Craig McLaughlin and Scott Buckley also participated. A further six talks were delivered by former members of the TS team, including June Andronick, Gerwin Klein and Rafal Kolanski, who last year created the verification service provider Proofcraft, with its office co-located with TS in the CSE Building.

A number of independent observers, including from funding agencies, noted that the Summit demonstrated how active and dynamic the seL4 ecosystem is, indicating that seL4 has a bright future.