TS News

News

PISTIs-V Project Launched
2025-01-20 – German Cyberagentur today launched their ÖvIT (Ecosystem for trustworthy IT) program. One of the five projects funded under ÖvIT is PISTIs-V, for which TS partners with German SME PlanV and the University of Gothenburg. PISTIs-V builds on LionsOS, the highly modular, seL4-based OS which TS is developing. LionsOS adheres to the principle of radical simplicity to enable formal verification. PISTIs-V aims to make formal verification of LionsOS a reality, tied to verified hardware components, and aiming for end-to-end proofs of security enforcement, including provable confinement of untrusted code. It also aims to guarantee real-time deadlines in mixed-criticality systems. An enabler of LionsOS verification is Pancake, a new systems programming language with a verified compiler, which TS is developing with its international partners.

2025-01-20 – German Cyberagentur today launched their ÖvIT (Ecosystem for trustworthy IT) program. One of the five projects funded under ÖvIT is PISTIs-V, for which TS partners with German SME PlanV and the University of Gothenburg.

PISTIs-V builds on LionsOS, the highly modular, seL4-based OS which TS is developing. LionsOS adheres to the principle of radical simplicity to enable formal verification. PISTIs-V aims to make formal verification of LionsOS a reality, tied to verified hardware components, and aiming for end-to-end proofs of security enforcement, including provable confinement of untrusted code. It also aims to guarantee real-time deadlines in mixed-criticality systems. An enabler of LionsOS verification is Pancake, a new systems programming language with a verified compiler, which TS is developing with its international partners.

Gernot Heiser at the PISTIs-V project launch.

Another picture of Gernot Heiser at the PISTIs-V project launch.

Cyberagentur is joining the seL4 foundation.

Trustworthy Systems at the seL4 Summit
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.

Trustworthy Systems at the seL4 Summit

The photo shows the participants of the seL4 Summit.

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.

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

Trustworthy Systems member of INSPECTA Team winning a large DARPA contract
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.

Trustworthy Systems member of INSPECTA Team winning a large DARPA contract

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.

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

TS Travels

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.

Show older articles