Proving Confidentiality and Its Preservation for Mixed-Sensitivity Concurrent Programs

Explore the challenges and techniques for proving confidentiality in mixed-sensitivity concurrent programs and its preservation under compilation in this 37-minute seminar by Dr. Robert Sison from the University of Melbourne. Delve into the key contributions of his doctoral dissertation, using the seL4 component-based software design of the Cross Domain Desktop Compositor as a case study. Learn about the ongoing collaboration between CIS and UNSW Sydney addressing microarchitectural side-channel vulnerabilities like Spectre. Discover the complexities of ensuring confidentiality in multi-threaded environments with shared resources, and gain insights into program verification, compiler verification, and the challenges of proving operating system security. Examine topics such as implicit flow leaks, conditional branching on secrets, and the development of a generic OS security model for time protection.

Intro
Confidentiality in the face of scale The desk islava
Motivating use case
3 key challenges
A mixed-sensitivity concurrent program CDDC'S HID switch as software components
Program verification: Prior work
Program verification: My work
Compiler verification: Prior work
Compiler verification: My work
Case study
Dangers of conditional branching on secrets Implicit flow 1:"storage" leak
Does your OS really enforce confidentiality?
How to verify an OS enforces time protection?
So far: Generic OS security model for time protection . Modelled new requirements on
Currently: Challenges for integration into seL4 proofs