Trustworthy Systems


Trustworthy Systems wins at the CSE Prizes Night
Left to right: Michael He, Gernot Heiser, Lucy Parker, Xavier Cooney, and Gordon Sau at the CSE Prize Night.

2024-05-13 – Trustworthy Systems team members have been awarded at the UNSW School of Computer Science and Engineering Prizes Night on Friday May 3rd. Lucy Parker and Xavier Cooney each won two awards, and Gordon Sau and Michael He each won one. Their details are below. Congratulations to Lucy, Xavier, Gordon, and Michael!

Lucy Parker won:
The Jump Trading Hero of Operating Systems Prize
Most Outstanding CSE Thesis Prize

Xavier Cooney won:
The Citadel Securities Year 2 Computer Science Excellence Prize
The Jane Street COMP3141 Prize, 2nd Place

Gordon Sau won:
The Jane Street COMP3161 Prize, 1st Place

Michael He won:
The Optiver SENG3011 Group Prize

Lucy Parker wins University Medal
Lucy Parker and her proud supervisor Gernot Heiser at Lucy's graduation, where she won the University Medal.

2024-05-13 – Lucy Parker, former TS member and Honours student, has won the University Medal for Computer Science, awarded at her graduation ceremony on Monday April 29th 2024. Lucy completed her Honours thesis on high performance I/O on seL4. She was a much valued, and now much missed, member of the TS team. Congratulations, Lucy!

TS represented at Everything Open 2024
Peter Chubb and Gernot Heiser at Everything Open 2024

2024-05-03 – Trustworthy Systems was represented at Everything Open this year, an annual conference focused on open technologies, including Linux, open source software, open hardware and open data, and the communities that surround them. Both Gernot and Peter presented talks on the work being done at TS.

Peter spoke about running your own mailserver and what that takes, using his own work as an example.

Gernot spoke about Lions OS, the complete seL4-based OS aimed to support the needs of developers of cyberphysical, IoT and other embedded systems.

Their talks generated plenty of fruitful discussion about the future of open technologies, including with researchers who are using seL4 in their work.

TS releases first version of new Lions OS and driver framework
Lions OS structure

2024-03-27 – TS proudly announces the first release (0.1.0) of its new Lions Operating System. Lions OS is built from scratch on top of the seL4 microkernel and the seL4 Microkit.

Lions OS is aimed at embedded, IoT and cyberphysical systems and is designed to be formally verifiable, adaptable to a wide class of use cases in the target domain, while at the same time setting the benchmark for performance of microkernel-based operating systems. We expect to achieve all three aims by a highly modular yet ruthlessly performance-oriented design and strict adherence to the time-honoured KISS principle.

Lions OS is based on and intimately tied to the seL4 Device Driver Framework (sDDF), which we are also releasing for the first time, although development versions have been public for about 18 months. The sDDF is designed on the same principles as Lions OS and has already demonstrated networking performance exceeding that of the mainstream Linux OS.

Gernot Heiser inducted into Leopoldina
Gernot Heiser being inducted into the Leopoldina Academy. Credit: Markus Scholz for Leopoldina

2024-03-14 – Gernot Heiser has been formally inducted into the German Academy of Sciences Leopoldina in a ceremony in Halle. After being elected in 2023, Gernot travelled to Halle for the formal conferral ceremony in February. Election to Leopoldina membership is highly selective and testament to the groundbreaking nature of the work done by Trustworthy Systems.

Photo Credit: Markus Scholz for Leopoldina

DARPA awards 10-year Game Changer to HACMS
Game Changer Award 2023-12-18 – US funding agency DARPA has just awarded their annual 10-year Game Changer Award for the most impactful program to the High Assurance Cyber-Military Systems (HACMS) program, as lead-CI Darren Cofer reports.
Led by Darren and Collins Aerospace, TS partnered with Galois, Boeing and the University of Minesota to deploy seL4 to protect autonomous air and ground vehicles from cyber attacks. The project formed the base from which TS is now aiming to make true OS security universal.
NIO co-funds Lions OS
NIO logo 2023-12-12 – Premium electric-car maker NIO is co-funding TS's work on developing the Lions OS. NIO is a Premium Member of the seL4 Foundation and has recently announced that their seL4-based SkyOS will be on mass-produced cars next year.
We thank NIO for their strong support of the seL4 ecosystem!
TS at SOSP'23
Mathieu Paturel and Lucy Parker at SOSP23

2023-11-17 – Four TS undergraduate students, together with Gernot Heiser, attended the Symposium on Operating Systems Principles (SOSP) in Koblenz, Germany. Honours students Lucy Parker and Alwin Joshy, and 3rd-year students Mathieu Paturel and Krishnan Winter, had all won travel scholarships that funded the bulk of the trip expenses.

Krishnan presented a paper at the co-located Workshop on Programming Languages and Operating Systems (PLOS). The paper, titled "Pancake: verified systems programming made sweeter”, was co-authored by TS members Johannes Åman Pohjola, Miki Tanaka, Gordon Sau, Ben Nott, Tiana Tsang Ung, Craig McLaughlin, and Gernot Heiser, as well as external collaborators Hira Taqdees Syeda, Remy Seassau, Magnus Myreen and Michael Norrish.

Krishnan said of the opportunity, “It was an amazing experience to represent TS and the Pancake project at PLOS, as well as providing the opportunity to learn about all the innovative research currently undergoing in the systems world.”

Lucy Parker and Mathieu Paturel presented posters at the main conference, generating lots of interesting discussion about seL4. Mathieu said, “I had a really good time at SOSP, I got to meet some great verification people with a very keen interest in systems (and some really cool systems people of course). For me, the talks between the talks were by far the most interesting, and presenting our posters was much more fun than I expected.”

TS releases Microkit, lowering bar to entry for seL4 adopters

2023-10-31 – Trustworthy Systems has just released the seL4 Microkit. The seL4 Microkit, formerly known as the Core Platform, is an operating system framework on top of seL4 which provides a small set of simple abstractions that ease the design and implementation of statically structured systems on seL4, while still leveraging the microkernel’s benefits of security and performance. The Microkit is distributed as an SDK that integrates with the developer’s build system of choice, significantly reducing the barrier to entry for new users of seL4. The seL4 Microkit has now also been adopted by the seL4 Foundation, making it an official part of the seL4 eco-system. The Microkit is the basis for much of the active research at Trustworthy Systems such as LionsOS.

seL4 summit in Minneapolis, USA
Lucy Parker at the seL4 summit

2023-10-23 – TS members Ivan Velickovic, Lucy Parker, and Gernot Heiser participated in the seL4 Summit in Minneapolis.

Lucy Parker presented the latest developments on the seL4 device driver framework, discussing the design of the networking system, and showed off its awesome performance.

Gernot Heiser gave an overview of seL4-related research and development at Trustworthy Systems, including introducing the new Lions OS that TS is developing. He also participated in a panel on various seL4-based OSes.

Ivan Velickovic presented the seL4 Microkit, freshly adopted by the seL4 Foundation. He also presented a hands-on tutorial on the Microkit.

The Summit proved yet again an excellent forum for exchanging ideas and discussions between participants in the ecosystem. Compared to last year, the number of organisations present was significantly increased. It was also obvious that the ecosystem had matured noticeably in terms of the range and maturity of frameworks and systems built on or around seL4.

Congratulations Tessa!
Tessa Lunney at the Engineering Awards Ceremony

2023-10-10 – Tessa Lunney, TS Administrator, has been recognised by a UNSW Engineering Excellence Award for her exemplary work on supporting Trustworthy Systesm in achieving its mission. Excellence is at the core of TS.
Congratulations on this highly deserved award!

Mathieu Paturel speaks at ApSys '23 in Korea
Mathieu Paturel in Seoul, Korea

2023-9-18 – Undergraduate team member Mathieu Paturel spoke at ApSys ‘23 on behalf of Trustworthy Systems and our research. He had these words to say about the experience:

"I was really fortunate to go to Seoul, Korea, to present some of the work we did with my former lecturer and supervisor, Zoltan Kocsis, and fellow team member Isitha Subasinghe , at the Asia Pacific Systems Workshop '23. The paper is called "First steps in verifying the seL4 Core Platform". During my taste of research project, I started writing a tool that used SMT solvers to automatically prove a key part of the correctness of the seL4 microkit (previously known as the Core Platform). The benefit is that the SMT solvers do the proof for us, so we don't have to write and maintain them ourselves; the downside is that SMT solvers aren't as smart as humans, and so we can't expect them to prove statements that are too complicated. In our case, we were able to express our conditions just right so that it was attainable. Being an undergraduate presenting the work felt pretty special, I feel pretty proud of that. To me, it just shows how amazing the people at Trustworthy Systems are: full of kindness and care, and of course, technical skills."

Congratulations to Mathieu for presenting at his first international conference.

Trustworthy Systems Travels
Gernot Heiser outside the airbus site with a Barracuda drone

2023-7-21 – This mid-year period has seen Gernot Heiser and other TS members present around the world.

After the ACM Software System Award, Gernot Heiser participated in the IFIP Working Group 10.4 meeting on the Future of Dependable Computing and Fault Tolerance in Arcos de Valdevez, Portugal.

Gernot and Ivan Velickovic delivered a seL4 tutorial at the 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). Gernot also gave a keynote, titled "Intelligent Vehicle Security Needs a Verified Operating System” at the DSN-affiliated Workshop on Safety and Security of Intelligent Vehicles and participated in a panel discussing intelligent vehicle security.

Gernot gave a talk titled “Secure Systems Design on seL4” at the RITICS-Space meeting, organised by Imperial College’s Research Institute in Trustworthy Inter-Connected Cyber-Physical Systems in London, UK.

Gernot attended the 17th Usenix Symposium on Operating Systems Design and Implementation in Boston, USA and participated in the SOSP Program Committee meeting.

Gernot, together with June Andronick, visited UK’s Defence Science & Technology Lab (Dstl) in Salisbury, UK for discussions about the development and deployment of seL4-based systems.

Gernot visited Airbus Defence & Space in Manching near Ingolstadt, Germany for discussions around seL4. (This photo is of Gernot Heiser outside the Airbus site with a Barracuda drone)

TS students honoured in CSE awards

2023-6-19 – Two TS team members have been honoured in the most recent CSE Awards.

Patrick Hao has been awarded the Arista Networks COMP9242 Prize.

Gordon Tsun Wang Sau has been awarded third place in the Jane Street COMP3141 Prize.

A big congratulations to Patrick and Gordon! More information and a full list of winners is here

Gernot Heiser received ACM award on behalf of team
Gernot accepts the ACM SSA award Some of the team receiving the ACM SSA award

2023-6-19 – Gernot was in San Francisco last week to accept the ACM Software System award on behalf of the team. More information from our previous news item is below:

The Association for Computing Machinery (ACM) has awarded the prestigious ACM Software System Award to TS members Gernot Heiser and Kevin Elphinstone, and others.

The ACM Software System Award recognises the development of a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both. It carries a prize of US$35,000. Professor Heiser and his team receive the award for the development of the first industrial-strength, high-performance operating system to have been the subject of a complete, machine-checked proof of functional correctness.

A huge congratulations goes out to the whole team:

Gernot Heiser, Kevin Elphinstone, University of New South Wales
Harvey Tuch, Google
David Cock, ETH Zurich
Philip Derrin, Qualcomm
Dhammika Elkaduwe, University of Peradeniya
Kai Engelhardt, Toby Murray, University of Melbourne
Michael Norrish, Australian National University
Thomas Sewell, University of Cambridge
Simon Winwood, Galois

You can read more about it on the UNSW website and the ACM website.

Farewell to Zoltan Kocsis
Zoltan Kocsis

2023-5-31 – We extend a very heartfelt farewell to Zoltan Kocsis, who is leaving Trustworthy Systems to pursue his real interests in pure mathematics. During his time with TS he initially worked on proving translation correctness of the seL4 kernel on the RISC-V architecture (thus taking the compiler out of the trusted computing chain). He then successfully applied his experience in the use of SMT solvers to the push-button verification of the seL4 Core Platform (seL4CP). This work opened new perspectives for verification at TS, and is now being extended to cover components of an OS that we are developing on top of seL4CP. We will miss his insights, but wish him all the best in his future endeavours.

TS Researchers receive ACM Software System Award
Researchers and developers of the sel4 microkernel

2023-5-5 – The Association for Computing Machinery (ACM) has awarded the prestigious ACM Software System Award to TS members Gernot Heiser and Kevin Elphinstone, and others.

The ACM Software System Award recognises the development of a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both. It carries a prize of US$35,000. Professor Heiser and his team receive the award for the development of the first industrial-strength, high-performance operating system to have been the subject of a complete, machine-checked proof of functional correctness.

A huge congratulations goes out to the whole team:

Gernot Heiser, Kevin Elphinstone, University of New South Wales
Harvey Tuch, Google
David Cock, ETH Zurich
Philip Derrin, Qualcomm
Dhammika Elkaduwe, University of Peradeniya
Kai Engelhardt, Toby Murray, University of Melbourne
Michael Norrish, Australian National University
Thomas Sewell, University of Cambridge
Simon Winwood, Galois

You can read more about it on the UNSW website and the ACM website.

Gernot Heiser elected to Leopoldina Academy of Science
The German National Academy of Science Leopoldina

2023-4-19 – Gernot Heiser has been elected to the German National Academy of Science Leopoldina. Leopoldina is the oldest continuous scientific academy in the world, operating for over 360 years. Elections is based on strict standards of scientific excellence and all members must be actively working in their fields. Congratulations, Gernot! Read more about it on the UNSW News Page.

Paper accepted at PLDI

2023-4-03 – A team of international collaborators that includes Trustworthy Systems member Johannes Åman Pohjola had a paper accepted by PLDI 2023, the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation. The paper is about PureCake, a lazy language on top of CakeML. This paper presents the first realistic verified compiler for a language with lazy evaluation. They will present their paper at the PLDI conference in Orlando, USA later in 2023.

Congratulations to Johannes and the team:
Hrutvik Kanabar (University of Kent, UK)
Samuel Vivien (École Normale Supérieure PSL, France and Chalmers University of Technology, Sweden)
Oskar Abrahamsson (Chalmers University of Technology, Sweden)
Magnus O. Myreen (Chalmers University of Technology, Sweden
Michael Norrish (Australian National University, Australia)
Johannes Åman Pohjola (University of New South Wales, Australia)
Riccardo Zanetti (Chalmers University of Technology, Sweden)
TS team at Everything Open conference in Melbourne, Australia
Peter Chubb at Everything Open 2023 Ivan Velickovic at Everything Open 2023 Lucy Parker at Everything Open 2023 Christopher Irving at Everything Open 2023

2023-3-22 – Trustworthy Systems team members Peter Chubb, Lucy Parker, Christopher Irving, and Ivan Velickovic presented their work on sel4 at the recent Everything Open conference in Melbourne.

You can find recordings of the talks for Lucy and Ivan, for Christopher, and for Peter, on the Everything Open YouTube channel.

Congratulations Dr Chen!
Dr Zilin Chen

2023-3-17 – Trustworthy Systems student Zilin Chen has just had his PhD thesis approved. We extend to him heartfelt and deserved congratulations.

His thesis is Towards A Practical High-Assurance Systems Programming Language. It was supervised by Professor Gabriele Keller, Dr. Christine Rizkallah, and TS’s Professor Gernot Heiser.

Robert Sison presents at FM conference in Lübeck, Germany
Rob Sison at the International Symposium on Formal Methods in Germany, March 2023

2023-3-15 – Robert Sison, a TS member and post-doctoral fellow from the University of Melbourne, works with TS team member Scott Buckley on Time Protection. He recently presented their work at the 25th International Symposium on Formal Methods at the University of Lübeck. Robert presented the collaborative work of the University of Melbourne, Trustworthy Systems, and Proofcraft in a paper titled “Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems”. This paper was co-authored by Gernot Heiser, Scott Buckley, Gerwin Klein, and Toby Murray.

New members of the Trustworthy Systems team
New members of Trustworthy Systems in 2023

2023-2-24 – We would like to welcome our newest members of the Trustworthy Systems team! They are (from left to right):

Isitha Subasinghe, Masters student and Research Assistant
Krishnan Winter, Taste of Research student
Mathieu Paturel, Taste of Research student
Sam Doak, Honours student
Gordan Sau, Taste of Research student
Matthew Rossouw, Taste of Research student
Waleed Shahid, Special Project student
Ben Nott, Taste of Research student
Arthur Wang, Honours student
seL4 at the Southern Summer School on Systems and Software Security at the University of Adelaide
Johannes Åman Pohjola at the Summer School Robert Sison at the Summer School Ivan
		 Velickovic at the Summer School

2023-1-27 – Trustworthy Systems Group participated in the Southern Summer School on Systems and Software Security. It was run at the University of Adelaide by Yuval Yarom (University of Adelaide) and Chitchanok Chuengsatiansup (University of Melbourne) from January 23 to 25 2023. Talks and workshops were given by Ivan Velickovic, Scott Buckley, Johannes Åman Pohjola, Robert Sison, and Gernot Heiser on seL4 and its importance to cybersecurity.

UNSW celebrates seL4 summit in Munich

2022-12-12 – UNSW Sydney has celebrated the seL4 summit in a recent news item. The summit, held in Munich on October 10 -13 2022, was the first held outside the USA and by the seL4 Foundation. The report notes that, “A number of independent observers, including from funding agencies, noted that the Summit demonstrated how active and dynamic the seL4 ecosystem is, indicating that seL4 has a bright future.”

TS Member Zilin Chen wins SIGPLAN award for his paper
Distinguished Artifact Award for Zilin Chen and co-authors

2022-12-12 – Congratulations to Zilin Chen for winning the Distinguished Artifact Award at the 2022 ACM SIGPLAN International Conference on Software Language Engineering. Chen and co-authors, including TS’s Gernot Heiser’s and TS affiliate Gerwin Klein, won the award for their artifact connected to the paper Property-Based Testing: Climbing the Stairway to Verification. The conference was on December 6-7 2022 in Auckland, New Zealand. You can find the paper on our Publications page.

Google award supports TS research

2022-12-05 – Google has awarded funds to the University of New South Wales to fund Gernot Heiser’s and Kevin Elphinstone’s work. The funds will go to their work on a Secure General-Purpose Operating System, which is a core part of the work done by the Trustworthy Systems group. This gift, Google says, is part of their “growing efforts to support excellent research in academia.”   This gift expands the influence and reach of the work done by Trustworthy Systems and UNSW.

TS Member Zilin Chen has paper accepted by POPL 2023

2022-11-17 – Congratulations to Zilin Chen and co-authors, including fellow TS member Craig McLaughlin, for having their paper accepted at POPL, the prestigious annual symposium on Principles of Programming Languages, in Boston USA in 2023. This paper forms part of Zilin Chen’s recently submitted doctoral thesis on the Cogent project.

The paper is:
Dargent: A Silver Bullet for Verified Data Layout Refinement
By Zilin Chen, Ambroise Lafont, Liam O’Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson and Christine Rizkallah

Information on the project, and the paper, is available here.

TS represented at UNSW Computing Research Expo
2022-10-25 – Trustworthy Systems had a strong presence at the UNSW Computing Research Expo on October 25th 2022. Designed to showcase the research projects of the School of Computer Science and Engineering, TS was represented by Gernot Heiser, Zoltan Kocsis and Peter Chubb. Gernot speaking at the UNSW CSE Expo in October 2022
  • Gernot Heiser gave a speech on secure and trustworthy systems
  • Gernot Heiser was part of a combined industry-academic panel speaking about impact through research and partnerships
  • Zoltan and Peter manned our ‘Hack this Drone!’ challenge to showcase seL4’s security. As expected, no one was able to hack the drone. The drone challenge is the same challenge run by DARPA at DEFCON ‘21, where, also, no one was able to hack the drone
First release of the new driver framework

2022-10-07 – TS is pleased to announce a pre-release of the seL4 Device Driver Framework (sDDF) for community feedback. We provide an initial design document, code and an official seL4 community request for comment (RFC), for details see the sDDF projects page. TS student Lucy Parker will introduce the framework and an initial performance evaluation at the seL4 Summit.

We thank our sponsors, the seL4 Foundation and the Technology Innovation Institute for their generous support for this work, and are looking forward to the community engaging with it.

TS will have a strong presence at a seL4 Summit

2022-09-20 – The first Summit organised by the seL4 Foundation will take place 10–13 October in Munich, Germany. TS will have a prominent role, with a total of 5 contributions:

  • TS Leader Gernot Heiser will deliver a keynote on the state of seL4-related research.
  • Zoltan Kocsis will present the new seL4 Core Platform (seL4CP), and on-going work on its verification and extension of its functionality
  • Lucy Parker will present the design and performance of the new seL4 Device Driver Framework (sDDF)
  • Gernot will also provide an overview of seL4’s principles, abstractions and use patterns
  • The on-site only bootcamp on the final day will have a session on the seL4CP, led by Ivan Velickovic

Scott Buckley and Craig McLaughlin will complete the on-site TS delegation, with more TS folks participating remotely.

For details check the Summit Program.

Gernot elected Fellow of the Royal Society of NSW

2022-08-18 – TS group leader Gernot Heiser has been elected a Fellow of the Royal Society of New South Wales, the oldest learned society of the Southern hemisphere.

UK's National Cybersecurity Centre supports Trustworthy Systems research

2022-06-22 – The British government backs UNSW Sydney researchers to advance their world-leading cyber security technology, which protects critical computer systems from cyber attacks.

The United Kingdom's National Cyber Security Centre (NCSC) will fund UNSW Engineering’s Trustworthy Systems research group to boost development of its seL4 microkernel technology – the world's most advanced cybersecurity technology.

Scientia Professor Gernot Heiser, leader of the Trustworthy Systems team that invented the technology, said the NCSC has been evaluating seL4 for some time now, and are working with their defence industry partners to deploy it in real-world computer systems.
Full UNSW media release.

NCSC-supported projects include: Some of the support goes to our partner Proofcraft for work on verifying seL4 on the 64-vit Arm architecture (AArch64) and for multicore processors.
Gernot delivers keynote at ACM SYSTOR
2022-06015 – TS group leader Gernot Heiser delivered a keynote at the ACM Systems and Storage Conference in Haifa, Israel. The talk, titled “Can we make trustworthy systems a reality?” examines the successes and challenges of taking the seL4 microkernel to the real world, and looks at current research done on and around seL4 at UNSW.
UNSW-SSRC collaboration to fortify systems and prevent hacking

2022-02-09 – UNSW has partnered with Secure Systems Research Center to implement ground-breaking cyber security technology.

“This collaborative effort between UNSW and SSRC will aim to extend the formally verified seL4 microkernel to support tight integration of virtualised systems,” said UNSW Trustworthy Systems leader and John Lions Chair, Scientia Professor Gernot Heiser.

Full UNSW announcement.
Full SSRC announcement.

...Older events