TS News

News

TS at the seL4 Summit in Vancouver
2026-09-11 – There was a strong TS presence at the seL4 summit this year. Held in Vancouver on 1^st – 3^rd September 2026, it was a gathering of cutting-edge seL4 research. Gernot Heiser gave a Trustworthy Systems Research and Development update. Rob Sison gave a talk titled “Where are we with Time Protection? Verification and cross-domain communication update.” Miki Tanaka gave a talk on Pancake updates. Liam Murphy spoke about “Formalising device protocols for sDDF driver verification.” Lesley Rossouw’s talk was on “Simplifying Microkit System Composition with Acacia.” She also spoke on “Modelling and performance analysis on Ethernet on LionsOS.” Guangtao Zhu made a poster and gave a remote talk on “Carrels: Secure, high-performance microservice on seL4” and on “Efficient User-level Physical Memory Management on seL4.” Bill Nguyen spoke about “Booting Windows on an x86-64 seL4-based VMM.” You can find these talks on the seL4 YouTube channel soon.

2026-09-11 – There was a strong TS presence at the seL4 summit this year. Held in Vancouver on 1^st – 3^rd September 2026, it was a gathering of cutting-edge seL4 research.

Gernot Heiser gave a Trustworthy Systems Research and Development update.

Rob Sison gave a talk titled “Where are we with Time Protection? Verification and cross-domain communication update.”

Miki Tanaka gave a talk on Pancake updates.

Liam Murphy spoke about “Formalising device protocols for sDDF driver verification.”

Lesley Rossouw’s talk was on “Simplifying Microkit System Composition with Acacia.” She also spoke on “Modelling and performance analysis on Ethernet on LionsOS.”

Guangtao Zhu made a poster and gave a remote talk on “Carrels: Secure, high-performance microservice on seL4” and on “Efficient User-level Physical Memory Management on seL4.”

Bill Nguyen spoke about “Booting Windows on an x86-64 seL4-based VMM.”

You can find these talks on the seL4 YouTube channel soon.

Series of releases for systems projects
2026-08-26 – The systems team has made a series of releases for our major systems projects: Microkit 2.3.0 - adds x86, IOMMU, kernel domain scheduler and SMP support. Additionally Microkit now uses the capDL initialiser. seL4 Device Driver Framework 0.7.0 - there has been a great deal of development since our last release. Major additions include x86-64 and SMP support, the creation of a virtual network switch (vswitch) component allowing clients to communicate virtually over the network, and corrections to the memory barriers used by our serial queue library (including using GenMC model checking to prove the correctness of the library under the weak memory model). Additionally we have increased the number of platforms supported by our serial, timer and network examples. See the change set for more details. There have been two releases of libVMM since our last new item: libVMM 0.1.0 - (our first release) adds a library for creating AArch64 VMMs on the Microkit. libVMM 0.2.0 - (our second and most recent release) fixes a number of bugs with the initial release, and adds support for virtualising Linux on x86-64. LionsOS 0.4.0 - adds the firewall system example as well as a LionsOS libC implementation which applications requiring POSIX support can be linked with. Additionally, for each project utilising another as a dependency we have updated the dependency to point to the most recent release. For a more detailed summary of the changes contained in each release, follow the corresponding link.

Series of releases for systems projects

2026-08-26 – The systems team has made a series of releases for our major systems projects:

Microkit 2.3.0 - adds x86, IOMMU, kernel domain scheduler and SMP support. Additionally Microkit now uses the capDL initialiser.

seL4 Device Driver Framework 0.7.0 - there has been a great deal of development since our last release. Major additions include x86-64 and SMP support, the creation of a virtual network switch (vswitch) component allowing clients to communicate virtually over the network, and corrections to the memory barriers used by our serial queue library (including using GenMC model checking to prove the correctness of the library under the weak memory model). Additionally we have increased the number of platforms supported by our serial, timer and network examples. See the change set for more details.

There have been two releases of libVMM since our last new item:

libVMM 0.1.0 - (our first release) adds a library for creating AArch64 VMMs on the Microkit.

libVMM 0.2.0 - (our second and most recent release) fixes a number of bugs with the initial release, and adds support for virtualising Linux on x86-64.

LionsOS 0.4.0 - adds the firewall system example as well as a LionsOS libC implementation which applications requiring POSIX support can be linked with.

Additionally, for each project utilising another as a dependency we have updated the dependency to point to the most recent release. For a more detailed summary of the changes contained in each release, follow the corresponding link.

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.

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.

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.”

Show older articles