TS News

News

New series of releases for systems projects
2025-03-25 – The systems team has made a series of releases for our major systems projects. LionsOS 0.3.0, adding more file system support and new developer tooling. seL4 Device Driver Framework 0.6.0, adding a 2D graphics device class and our first native SD card driver. Microkit 2.0.0, adding many quality-of-life improvements and minor features requested by the community.

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.

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.

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.

Show older articles