TS News

News

TS represents at FM Oz
Trustworthy Systems was well represented at the FM Oz workshop, held at the University of Queensland on June 3^rd to 5^th 2026. TS team members spoke on Thursday 4 ^th June. Miki Tanaka gave an update on Pancake. Kurt Rihui Wu spoke about adding support for memory barriers in Pancake. Junming Zhao gave a talk titled “A Rely-Guarantee + Separation Logic for Verifying Microkit-Based Systems.” Vincent Jackson’s talk was “SecRGSep: A General Logic for Information Flow Security” Rob Sison spoke on “Clearing roadblocks to Time Protection verification for seL4” Thomas Liang also made a vox-pop analysis of the workshop, available on YouTube.

Trustworthy Systems was well represented at the FM Oz workshop, held at the University of Queensland on June 3^rd to 5^th 2026.

TS team members spoke on Thursday 4 ^th June.

Miki Tanaka gave an update on Pancake.
Kurt Rihui Wu spoke about adding support for memory barriers in Pancake.
Junming Zhao gave a talk titled “A Rely-Guarantee + Separation Logic for Verifying Microkit-Based Systems.”
Vincent Jackson’s talk was “SecRGSep: A General Logic for Information Flow Security”
Rob Sison spoke on “Clearing roadblocks to Time Protection verification for seL4”
Thomas Liang also made a vox-pop analysis of the workshop, available on YouTube.

TS students make UNSW Engineering Dean's List
2026-06-03 – At the UNSW Engineering awards night, two TS students made the Dean's list, putting them into the top 1% of students in terms of academic performance: Samuel Tyler (left) for his second year, and Lucas Harvey for his third year (although both have made the list each year of their studies). Congratulations!

TS students make UNSW Engineering Dean's List

2026-06-03 – At the UNSW Engineering awards night, two TS students made the Dean's list, putting them into the top 1% of students in terms of academic performance: Samuel Tyler (left) for his second year, and Lucas Harvey for his third year (although both have made the list each year of their studies). Congratulations!

Gernot wins IEEE Award
2026-05-21 – Gernot Heiser has been awarded the 2025 IEEE Technical Committee on Real-Time Systems (TCRTS) Outstanding Technical Achievements and Leadership Award (OTALA). Gernot received this award at RTAS on Wednesday May 13^th 2026, by TCRTS vice-chair Björn Brandenburg from MPI-SWS. Gernot’s acceptance speech was a talk titled “MCS Safety – an OS perspective.”

Gernot wins IEEE Award

Professor Gernot Heiser accepting his award at RTAS

2026-05-21 – Gernot Heiser has been awarded the 2025 IEEE Technical Committee on Real-Time Systems (TCRTS) Outstanding Technical Achievements and Leadership Award (OTALA). Gernot received this award at RTAS on Wednesday May 13^th 2026, by TCRTS vice-chair Björn Brandenburg from MPI-SWS. Gernot’s acceptance speech was a talk titled “MCS Safety – an OS perspective.”

TS represents at Down Underflow 2026
2026-03-25 – TS team members Lesley Rossouw, Julia Vassiliki, and Liam Murphy presented at Down Underflow 2026. Our team presented Sealing the hardware-software contract with LionsOS on Serengeti using time protection and device verification in this weekend of presentations and networking for the open silicon community. They talked about two weaknesses in the typical hardware-software contract and our approach to solving them. Speculative execution attacks such as Spectre rely on their use of a covert timing channel to leak information through speculation's effect on microarchitectural state. Julia described our work on time protection, an extension of the hardware-software contract to systematically prevent timing channels. Device drivers are a major source of operating system bugs, a large portion of which are caused by violations of the devices' hardware-software contracts. These contracts are often represented by unreliable datasheets, making it difficult to ensure correctness. Liam covered the device formalisation project, which strengthens this contract by replacing datasheets with formal specifications verified against the device's source code, enabling formal verification of device drivers and the prevention of driver bugs. Lesley introduced LionsOS and Serengeti, our secure operating system and experimental SoC development platform. These are the host for all the custom hardware and software features used in this work.

TS represents at Down Underflow 2026

2026-03-25 – TS team members Lesley Rossouw, Julia Vassiliki, and Liam Murphy presented at Down Underflow 2026. Our team presented Sealing the hardware-software contract with LionsOS on Serengeti using time protection and device verification in this weekend of presentations and networking for the open silicon community. They talked about two weaknesses in the typical hardware-software contract and our approach to solving them.

Speculative execution attacks such as Spectre rely on their use of a covert timing channel to leak information through speculation's effect on microarchitectural state. Julia described our work on time protection, an extension of the hardware-software contract to systematically prevent timing channels.

Device drivers are a major source of operating system bugs, a large portion of which are caused by violations of the devices' hardware-software contracts. These contracts are often represented by unreliable datasheets, making it difficult to ensure correctness. Liam covered the device formalisation project, which strengthens this contract by replacing datasheets with formal specifications verified against the device's source code, enabling formal verification of device drivers and the prevention of driver bugs.

Lesley introduced LionsOS and Serengeti, our secure operating system and experimental SoC development platform. These are the host for all the custom hardware and software features used in this work.

Foresight Institute awards grant to TS
2026-03-02 – California-based non-profit Foresight Institute has awarded a grant to Gernot Heiser and Rob Sison for our project to connect proofs about usermode components to the seL4 specs. This project is a key part in the PISTIs-V project that aims to extend seL4’s verification to the full LionsOS operating system.

Show older articles