TS News

News

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.

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

seL4 summit in Minneapolis, USA

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

Mathieu Paturel speaks at ApSys '23 in Korea

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.

Trustworthy Systems Travels
2023-07-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)

Trustworthy Systems Travels

Gernot Heiser outside the airbus site with a Barracuda drone

2023-07-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)

Show older articles