Funding

Aim

Scalable verification of global safety and security guarantees for component-based OSes by composing local per-component proof efforts.

Context

With the seL4 microkernel verified, the next frontier for securing our systems is guaranteeing the behaviour of the OS services implemented to run instead in user mode (on top of the kernel) as advocated by the microkernel philosophy, with services componentised to allow a separation of concerns and enforce the principle of least privilege.

When it comes to the verification of such systems of concurrently running components, ensuring compositionality of properties about individual components into properties about their possible concurrent executions with others is crucial to ensure proofs are scalable and robust to local changes. With compositionality, a code update means reverifying only the affected component, as opposed to reverifying the entire system.

Problem

Achieving compositionality of proof techniques for concurrent systems is challenging due to the need to model and manage nondeterminism at the per-component proof level that is visible via concurrent writes to memory shared between components, or due to system calls made by one component affecting state visible to another.

Compositionality is especially difficult for security properties, though our past work on Information Flow verification has shown it possible for LionsOS-like cross-domain systems like the CDDC. Our desire to allow engineers to specify properties as code annotations and discharge proofs using push-button techniques further centers usability in the challenge of designing the per-component and compositional properties.

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

1. apply to system implementation features used by LionsOS, and
2. 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 the encoding of properties for LionsOS components and the incorporation of design features into our proof techniques based on concurrent separation logic, as well as methods for verifying that the use of atomic primitives in implementing inter-component communication is functionally correct under weak memory consistency models.

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