Presented by

  • Gernot Heiser

    Gernot Heiser
    @GernotHeiser
    https://trustworthy.systems/people/?cn=Gernot+Heiser

    Gernot is the microkernel dude, having for over 25 years led the development of various L4 microkernels, which were deployed by the billions, including on the secure enclave of all iOS devices. His team has developed the seL4 microkernel, the world's first OS kernel that is mathematically proved free of implementation bugs, and that was open-sourced in July'14. Gernot is a Scientia Professor and John Lions Chair at UNSW and founder and leader of the Trustworthy Systems group. He is a Fellow of the ACM, the IEEE and the Australian Academy of Technology and Engineering (ATSE). He has won multiple awards, including ACM SIGOPS Hall of Fame, ICT Researcher of the year 2016 of the South-East Asian Regional Computing Confederation (SEARCH) and 2015 of the Australian Computer Society (ACS), Entrepreneur of the Year 2014 by Engineers Australia, and New South Wales Scientist of the Year 2009 (Category Engineering, Mathematics and Computer Science). He serves as Chief Scientist (Software) of HENSOLDT Cyber GmbH, Chief Scientific officer of Neutrality, and was the co-founder and CTO of Open Kernel Labs which was acquired by General Dynamics in 2012.

Abstract

The seL4 microkernel is the world's first operating system (OS) kernel with a machine-checked proof of implementation correctness (originally completed in 2009 for 32-bit Arm processors). This was followed by more wold-firsts: proofs of security enforcement, proof of correctness of the executable binary, sound worst-case execution-time analysis. seL4 had been developed and verified at NICTA, a public-sector research organisation, and open-sourced in 2014. With NICTA being absorbed into CSIRO in 2015, the seL4 developers, known as the Trustworthy Systems (TS) team, became part of CSIRO, and research, development and community support continued there, mostly through funding from the US government (DARPA) and industry. However, uptake remained limited outside the defence sector. In April 2020 we created the seL4 Foundation (as a project of the Linux Foundation) as a way to encourage broader community engagement as well as removing dependency on a single organisation. The importance of the latter aspect became obvious when in May 2021 CSIRO announced that it was abandoning the Trustworthy Systems group and its research agenda of developing truly secure computer systems. This was a near-death experience for seL4: many of our highly-skilled staff and students had job offers within days. The TS team would have disintegrated within weeks, leaving seL4 orphaned, had not UNSW stepped up and offered to fund the team to the end of the year, giving us much needed breathing space. This was followed by an amazing rallying of the community. While before we had trouble scaling Foundation membership beyond the half-dozen initial members, companies we never heard of (but who were already building seL4 into their products) joined, increasing the Foundation's membership revenue ten-fold over a period of about 2 months. Many former staff increased their engagement (with backing from their employers), and community contributions increased massively. At the same time the TS continued to hit new firsts, especially on verification and security proofs for seL4 on 64-bit RISC-V. The technology and its ecosystem are very much alive and growing. Which leaves a number of questions to explore, specifically: (1) why did we not achieve more community engagement before the cataclysmic events of May'20, and (2) why did things suddenly take off after? I can only attempt to provide (at best partial) answers, and will welcome feedback from other community leaders. However it is clear that (1) had to do with the steep learning curve of seL4, but also organisational barriers. Specifically, seL4 development was not really open until we set up the Foundation, and even then it took a long time to move everything out from CSIRO, a process that was still on-going when the divorce was announced. Yet it became clear that there was far more seL4 adaptation in industry than we were aware of. (2) was clearly enabled by this existing activity: people realised that the whole of seL4 was under threat, and they had to contribute back if they wanted it to live on. Which leaves us with the question of what could we have done differently to get them engaged earlier, and how can we engage even more of the adopters? There are clearly many more out there.