Funding Participants

Aim

PISTIs-V addresses the lack of an integrated IT stack with provable end-to-end security for embedded/cyber-physical systems. It aims to develop a reference system with proofs of strong safety and security properties covering hardware and software and their interaction.

Project Goals

A verified OS, based on LionsOS that:

1. provides OS services as expected by embedded and cyber-physical systems, such as aircraft, cars or industrial control systems;
2. is verified for correct operation in the sense that its critical components are proved functionally correct and the composition is proved to enforce security properties, and is also robust to implementation and (moderate) requirements changes. This specifically includes verifying device drivers for correct operation and interfacing to the hardware;
3. provides verified hardware subsystems which are critical for the correct functionality of the OS, including verified device hardware to connect to verified drivers;
4. provably confines untrusted code, i.e. prevents an untrusted program from leaking information in violation of the system's security policy. This specifically includes the prevention of leakage though timing channels;
5. supports mixed-criticality systems, where a critical component can be guaranteed to meet its deadlines despite allowing less-critical components with tighter timeliness needs to preempt the critical component.

Funding

PISTIs-V if funded by the German Cyberagentur under the Ökosystem Vertrauenswürdige IT – Beweisbare Cybersicherheit (Ecosystem formally verifiable IT – Provable cybersecurity, ÖvIT) program

Team

• Munich-based PlanV is the prime contractor for PISTIs-V, and responsible for all hardware verification work.
• The Trustworthy Systems research group at UNSW Sydney is responsible for the software architecture and most verification, especially temporal properties.
• The University of Gothenburg is working closely with UNSW on the Pancake programming language, as the main vehicle for making software verification tractable.

Key People

PlanV

• Massimiliano (Max) Giacometti, overall project manager; repsonsible for HW design
• Albert Rizaldi, responsible for hardware formal verification

UNSW

• Gernot Heiser, UNSW Lead, responsible for system architecture and real-time work
• Thomas Sewell, responsible for ITP verification of Pancake code
• Rob Sison, responsible for Time Protection and connecting proofs to seL4
• Miki Tanaka, UNSW co-lead for Pancake compiler work

Gothenburg

• Johannes Åman Pohjohla, UG co-lead for Pancake compiler work

Availability

All research outcomes from PISTIs-V will be published and all artefacts will be available as open source.

Latest News

• 2025-01-20: Cyberagentur launches the ÖViT program, of which PISTIs-V is a part.

Contact

• Gernot Heiser, gernot<at>unsw.edu.au

People

Publications

Junming Zhao, Alessandro Legnani, Tiana Tsang Ung, H. Truong, Tsun Wang Sau, Miki Tanaka, Johannes Åman Pohjola, Thomas Sewell, Rob Sison, Hira Syeda, Magnus Myreen, Michael Norrish and Gernot Heiser Verifying device drivers with Pancake arXiv preprint, January, 2025