TS News

News

TS students shine at annual CSE Thesis Showcase
2025-12-12 – The annual Thesis Showcase of the School of Computer Science & Engineering featured four TS students who presented their excellent honours theses: (left to right) Richard Shen, Thomas Liang (back to camera), Lesley Rossouw and Halogen Truong. Several more TS students were invited but, unfortunately, could not make it.

Trustworthy Systems Postgrads in India and Morocco
Our postgraduate students are representing TS at conferences around the world. Dao Le attended the Asian Symposium on Programming Languages and Systems (APLAS), co-located with International Symposium on Automated Technology for Verification and Analysis, in Bengaluru, India. He presented his work as a poster and short presentation, that resulted in an invitation to speak to the Boston Computation Club in 2026. Kevin Tran presented a paper at the International Colloquium on Theoretical Aspects of Computing (ICTAC) in Marrakech, Morocco. His paper, “A rely-guarantee-based simulation for cooperative semantics," was on deductive reasoning about possibly infinite-state shared-memory concurrent systems.

Trustworthy Systems Postgrads in India and Morocco

Our postgraduate students are representing TS at conferences around the world.

Dao Le attended the Asian Symposium on Programming Languages and Systems (APLAS), co-located with International Symposium on Automated Technology for Verification and Analysis, in Bengaluru, India. He presented his work as a poster and short presentation, that resulted in an invitation to speak to the Boston Computation Club in 2026.

Kevin Tran presented a paper at the International Colloquium on Theoretical Aspects of Computing (ICTAC) in Marrakech, Morocco. His paper, “A rely-guarantee-based simulation for cooperative semantics," was on deductive reasoning about possibly infinite-state shared-memory concurrent systems.

Trustworthy Systems releases LionsOS based firewall as a community project
2025-11-13 – TS is proud to announce the release of a new proof-of-concept firewall system running on LionsOS. The firewall has a highly modular design, each module being a process running in its own address space. It uses components of both LionsOS and the seL4 device driver framework (sDDF) to demonstrate how to construct a Microkit-based component architecture. Currently the firewall has only very limited functionality, and we hope that the project will engage members of our community who are interested in improving its usability, with the ultimate goal of enabling the firewall to be deployed on the TS network. The firewall supports zero-copy routing of traffic between two network interfaces, and is able to apply simple filtering rules to a subset of IP traffic (TCP, UDP, ICMP). The filtering and routing rules applied by the firewall can be updated at run time through a rudimentary web GUI interface. The firewall also contains a simple ICMP module component to generate ICMP packets on behalf of the system. Currently the system runs on both QEMU and the Compulab IOT-GATE-IMX8PLUS, and we have also created a supporting Docker container that significantly simplifies testing when running on QEMU, allowing developers to jump straight in.

Trustworthy Systems releases LionsOS based firewall as a community project

2025-11-13 – TS is proud to announce the release of a new proof-of-concept firewall system running on LionsOS. The firewall has a highly modular design, each module being a process running in its own address space. It uses components of both LionsOS and the seL4 device driver framework (sDDF) to demonstrate how to construct a Microkit-based component architecture. Currently the firewall has only very limited functionality, and we hope that the project will engage members of our community who are interested in improving its usability, with the ultimate goal of enabling the firewall to be deployed on the TS network.

The firewall supports zero-copy routing of traffic between two network interfaces, and is able to apply simple filtering rules to a subset of IP traffic (TCP, UDP, ICMP). The filtering and routing rules applied by the firewall can be updated at run time through a rudimentary web GUI interface. The firewall also contains a simple ICMP module component to generate ICMP packets on behalf of the system. Currently the system runs on both QEMU and the Compulab IOT-GATE-IMX8PLUS, and we have also created a supporting Docker container that significantly simplifies testing when running on QEMU, allowing developers to jump straight in.

Trustworthy Systems at SOSP in Korea
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.

Trustworthy Systems at SOSP in Korea

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.

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

Trustworthy Systems at the seL4 summit

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

Show older articles