The Trustworthy Systems (TS) group was strongly involved in the workshop day associated with this year’s ACM SIGOPS Symposium on Operating Systems Principles in Seoul, Korea. 

The day kicked off with Scientia Professor Gernot Heiser’s keynote address at the Workshop on Kernel Isolation, Safety and Verification (KISV). In his talk titled “Why change the kernel when you have seL4?”, Gernot’s challenged the widespread assumption that structuring OS code as isolated modules will result in excessive overhead if using traditional address-spaces. He demonstrated by ‘back-of-the-envelope’ calculations that the resulting overheads are insignificant, and backed this reasoning by measurements performed on the LionsOS operating system developed by TS.

Next on the agenda was TS honours student Liam Murphy presenting at the Programming Languages and Operating Systems (PLOS) workshop a paper titled “High-fidelity specification of real-world devices”, co-authored by Albert Rizaldi from German company PlanV, University of Wisconsin – Madison undergraduate student George Chen (who had contributed as an intern to TS), TS undergraduates Lesley Rossouw and James Treloar, and UNSW staff Hammond Pearce, Miki Tanaka and Gernot Heiser.

Finally Gernot presented an invited talk at the SIGOPS Strategy Workshop held on occasion of the 60th anniversary of SOSP, titled “Don't’ forget the OS – and the principles!” which discussed the decreasing number of OS design papers at top-tier OS conferences (although recognising that this year’s SOSP had a high number) while plenty of important OS work remains to be done.

A highlight of every year is the seL4 summit. Run by the seL4 Foundation, it showcases the cutting edge of research on and work with seL4. This year the summit was in Prague, Czechia, and was attended by three in the TS team.

Thomas Sewell gave a talk, co-written with team member Rob Sison, titled ‘Splitting the seL4 Specification verifying Kernel–Userland Integration for LionsOS.’

Junming Zhao spoke on ‘Verifying Device Drivers with Pancake.’

Gernot Heiser gave an update the research that the wider TS team is doing on seL4.

The summit was attended by a committed group of international researchers. The TS team also actively engaged in birds-of-a-feather (BoF) sessions and has good discussions with many of the participants, spreading the word and returning with some new ideas.”

2025-01-20 – German Cyberagentur today launched their ÖvIT (Ecosystem for trustworthy IT) program. One of the five projects funded under ÖvIT is PISTIs-V, for which TS partners with German SME PlanV and the University of Gothenburg.

PISTIs-V builds on LionsOS, the highly modular, seL4-based OS which TS is developing. LionsOS adheres to the principle of radical simplicity to enable formal verification. PISTIs-V aims to make formal verification of LionsOS a reality, tied to verified hardware components, and aiming for end-to-end proofs of security enforcement, including provable confinement of untrusted code. It also aims to guarantee real-time deadlines in mixed-criticality systems. An enabler of LionsOS verification is Pancake, a new systems programming language with a verified compiler, which TS is developing with its international partners.