Funding
Compositional Proof Methods
for system-wide safety and security properties
Aim
Scalable verification of global safety and security guarantees by composing local per-component proof efforts.
Approach
We currently focus on adapting prior rely-guarantee-based approaches to proving safety and security properties, akin to those developed by the CDDC and Information Flow projects. Specifically, the approach aims to
- apply to system implementation features used by LionsOS, and
- be able to use our Viper-based verification methods to discharge the local proof efforts for each OS component written in the Pancake language.
In parallel, we are also investigating properties encodings for LionsOS components based on concurrent separation logic.
Latest News
- 2025-01-20: Cyberagentur launches the ÖViT program, which funds this research through the PISTIs-V project.
Support
This research is financially supported by:
- Cyberagentur under the Ecosystem formally verifiable IT – Provable cybersecurity (EvIT) program funds the PISTIs-V Project of which this research is a part.
Contact
- Rob Sison, r.sison<at>unsw.edu.au
People
Current |
Past
|