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