Proving Confidentiality and Its Preservation for Mixed-Sensitivity Concurrent Programs

Proving Confidentiality and Its Preservation for Mixed-Sensitivity Concurrent Programs

The University of Melbourne via YouTube Direct link

Does your OS really enforce confidentiality?

12 of 15

12 of 15

Does your OS really enforce confidentiality?

Class Central Classrooms beta

YouTube videos curated by Class Central.

Classroom Contents

Proving Confidentiality and Its Preservation for Mixed-Sensitivity Concurrent Programs

Automatically move to the next video in the Classroom when playback concludes

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

Never Stop Learning.

Get personalized course recommendations, track subjects and courses with reminders, and more.

Someone learning on their laptop while sitting on the floor.