2024-10-28 – The seL4 Foundation, chaired by Scientia Prof Gernot Heiser, ran the 6th seL4 Summit on 15–17 October. It was the first time the Summit was held in Australia, where seL4 was created. This was fitting, as it coincided with multiple “round” anniversaries: 20 years since the seL4 project started at NICTA, 15 years since the proof of implementation correctness was completed (the first ever for an operating-system kernel) and 10 years since seL4 was open-sourced.

The Summit had record attendance with 89 registrations, half of which were current (12) or former members of the Trustworthy Systems (TS) group. The majority of attendees were from overseas, mostly from industry, with the rest from universities, government or enthusiasts. Of the 31 talks, six were from TS and another ten from TS alumni.

TS also ran a tutorial on its new LionsOS operating system, another tutorial was on using Rust with seL4. A highlight was Ivan Velickovic running his presentation on LionsOS, and the seL4 web site moving to a server running on LionsOS. The Summit talks can be watched on the seL4 Foundation Youtube channel.

2024-10-15 – As of today, the seL4 web site runs on LionsOS!

2024-08-28 – The DARPA Pipeline Reasoning of Verifiers Enabling Robust Systems (PROVERS) Program is funding the project Industrial Scale Proof Engineering for Critical Trustworthy Applications (INSPECTA). TS is a member of the project team that is led by our long-standing collaborators Collins Aerospace. Other members are TS spinout Proofcraft, US company DornerWorks, as well as Carnegie Mellon University, the University of Kansas and Kansas State University. INSPECTA aims at scaling up formal verification and fully integrating it with development and maintenance processes to enable higher levels of assurance. The TS work in INSPECTA is further developing LionsOS and using automated verification tools for verifying LionsOS components.

2024-08-05 – Trustworthy Systems members have been travelling again this year.

Gernot Heiser gave the keynote address at the DSN conference in Brisbane in June, on Lions OS: Towards a truly dependable operating system.

Robert Sison travelled to Philadelphia, USA, representing TS as we further our work with Collins Aerospace.

Gernot Heiser travelled to Santa Clara, USA to attend the OSDI ’24 USENIX conference and to work with collaborators in the San Franciso area.

Researchers have also travelled to us.

Associate Professor Michael Norrish joined us from ANU for a strategy day with the Pancake team.

Alessandro Legnani, from ETH Zurich via Melbourne, joined Robert Sison for collaboration.

In October we will host Nils Wistoff, from ETH Zurich, for collaborative work on seL4.

Collaboration is an important part of the work culture at Trustworthy Systems, from meetings with sponsors to collaborations with early-career researchers and integral to our high calibre research.

2024-06-24 – Trustworthy Systems were well represented at the Oz-FM workshop in Brisbane last month. The workshop, on Formal Methods in Australia and New Zealand, included talks by four TS members.

Carroll Morgan gave the first talk of the workshop, an invited talk, on Formal Methods teaching and communication.

Gernot Heiser, also an invited speaker, spoke about Lions OS.

Rob Sison spoke about time protection and OS service verification in relation to seL4.

Johannes Åman Pohjola spoke about Pancake programs.

Their talks provoked excellent discussions about Formal Methods in teaching and research.

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

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!

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.

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.

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

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.

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!

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

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.

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.

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!

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.

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)

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

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:

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.

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:

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.

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)

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.

• Lucy and Ivan spoke about sel4 core platform
• Christopher spoke about Ceph and NFS
• Peter spoke about Creating a poetry book

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

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.

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.

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

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.

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

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.

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.

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

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.

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.

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.

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.

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.