TS News

News

TS represents at Downunder Flow 2026
TS team members Lesley Rossouw, Julia Vassiliki, and Liam Murphy presented at Downunder Flow 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 Downunder Flow 2026

TS team members Lesley Rossouw, Julia Vassiliki, and Liam Murphy presented at Downunder Flow 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
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.

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.

Show older articles