2024-10-28 – The seL4 Foundation, chaired by Scientia Prof Gernot Heiser, ran the 6th seL4 Summit on 15–17 October. It was the first time the Summit was held in Australia, where seL4 was created. This was fitting, as it coincided with multiple “round” anniversaries: 20 years since the seL4 project started at NICTA, 15 years since the proof of implementation correctness was completed (the first ever for an operating-system kernel) and 10 years since seL4 was open-sourced.

The Summit had record attendance with 89 registrations, half of which were current (12) or former members of the Trustworthy Systems (TS) group. The majority of attendees were from overseas, mostly from industry, with the rest from universities, government or enthusiasts. Of the 31 talks, six were from TS and another ten from TS alumni.

TS also ran a tutorial on its new LionsOS operating system, another tutorial was on using Rust with seL4. A highlight was Ivan Velickovic running his presentation on LionsOS, and the seL4 web site moving to a server running on LionsOS. The Summit talks can be watched on the seL4 Foundation Youtube channel.

2024-10-15 – As of today, the seL4 web site runs on LionsOS!

2024-08-28 – The DARPA Pipeline Reasoning of Verifiers Enabling Robust Systems (PROVERS) Program is funding the project Industrial Scale Proof Engineering for Critical Trustworthy Applications (INSPECTA). TS is a member of the project team that is led by our long-standing collaborators Collins Aerospace. Other members are TS spinout Proofcraft, US company DornerWorks, as well as Carnegie Mellon University, the University of Kansas and Kansas State University. INSPECTA aims at scaling up formal verification and fully integrating it with development and maintenance processes to enable higher levels of assurance. The TS work in INSPECTA is further developing LionsOS and using automated verification tools for verifying LionsOS components.

2024-08-05 – Trustworthy Systems members have been travelling again this year.

Gernot Heiser gave the keynote address at the DSN conference in Brisbane in June, on Lions OS: Towards a truly dependable operating system.

Robert Sison travelled to Philadelphia, USA, representing TS as we further our work with Collins Aerospace.

Gernot Heiser travelled to Santa Clara, USA to attend the OSDI ’24 USENIX conference and to work with collaborators in the San Franciso area.

Researchers have also travelled to us.

Associate Professor Michael Norrish joined us from ANU for a strategy day with the Pancake team.

Alessandro Legnani, from ETH Zurich via Melbourne, joined Robert Sison for collaboration.

In October we will host Nils Wistoff, from ETH Zurich, for collaborative work on seL4.

Collaboration is an important part of the work culture at Trustworthy Systems, from meetings with sponsors to collaborations with early-career researchers and integral to our high calibre research.

2024-06-24 – Trustworthy Systems were well represented at the Oz-FM workshop in Brisbane last month. The workshop, on Formal Methods in Australia and New Zealand, included talks by four TS members.

Carroll Morgan gave the first talk of the workshop, an invited talk, on Formal Methods teaching and communication.

Gernot Heiser, also an invited speaker, spoke about Lions OS.

Rob Sison spoke about time protection and OS service verification in relation to seL4.

Johannes Åman Pohjola spoke about Pancake programs.

Their talks provoked excellent discussions about Formal Methods in teaching and research.