TS News

News

Gernot Heiser gives keynote at ASPLOS+EuroSys
2025-04-01 – Gernot Heiser gave a joint keynote on 1 April at the co-located top-tier ASPLOS + EuroSys conferences in Rotterdam, Netherlands. The talk was titled "Will we ever have truly secure operating systems?” Gernot Heiser from UNSW Sydney delivered another compelling keynote titled "Will We Ever Have Truly Secure Operating Systems?”. He unpacked the technical and organisational barriers that have long hindered efforts toward provable OS security, with a particular focus on the practical difficulties of deploying the seL4 microkernel in real-world systems. As a concrete step forward, he introduced LionsOS, a new seL4-based operating system tailored for the embedded and cyber-physical systems domain, as an effort that combines security guarantees with practical design principles. This OS represents more than just an engineering milestone; it offers a promising prototype for future security research, especially in contexts where strong guarantees are critical but legacy complexity can be avoided. This led to discussing the present work of Trustworthy Systems on LionsOS, aiming to finally develop a provably secure OS at least for the embedded/cyberphysical space, and early ideas about a provably-secure general-purpose OS.

Gernot Heiser gives keynote at ASPLOS+EuroSys

2025-04-01 – Gernot Heiser gave a joint keynote on 1 April at the co-located top-tier ASPLOS + EuroSys conferences in Rotterdam, Netherlands.

The talk was titled "Will we ever have truly secure operating systems?”

Gernot Heiser from UNSW Sydney delivered another compelling keynote titled "Will We Ever Have Truly Secure Operating Systems?”. He unpacked the technical and organisational barriers that have long hindered efforts toward provable OS security, with a particular focus on the practical difficulties of deploying the seL4 microkernel in real-world systems.

As a concrete step forward, he introduced LionsOS, a new seL4-based operating system tailored for the embedded and cyber-physical systems domain, as an effort that combines security guarantees with practical design principles. This OS represents more than just an engineering milestone; it offers a promising prototype for future security research, especially in contexts where strong guarantees are critical but legacy complexity can be avoided.

This led to discussing the present work of Trustworthy Systems on LionsOS, aiming to finally develop a provably secure OS at least for the embedded/cyberphysical space, and early ideas about a provably-secure general-purpose OS.

New series of releases for systems projects
2025-03-25 – The systems team has made a series of releases for our major systems projects. LionsOS 0.3.0, adding more file system support and new developer tooling. seL4 Device Driver Framework 0.6.0, adding a 2D graphics device class and our first native SD card driver. Microkit 2.0.0, adding many quality-of-life improvements and minor features requested by the community.

PISTIs-V Project Launched
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.

PISTIs-V Project Launched

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.

Gernot Heiser at the PISTIs-V project launch.

Another picture of Gernot Heiser at the PISTIs-V project launch.

Cyberagentur is joining the seL4 foundation.

Trustworthy Systems at the seL4 Summit
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.

Trustworthy Systems at the seL4 Summit

The photo shows the participants of the seL4 Summit.

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.

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