1 citations · 2 across the 4 of their papers we have counts for
4 papers
Verifying Device Drivers with Pancake
Junming Zhao, Miki Tanaka, Johannes Åman Pohjola +10
Device driver bugs are the leading cause of OS compromises, and their formal verification is therefore highly desirable. To the best of our knowledge, no realistic and performant d…
Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms (Extended Version)
Pengbo Yan, Toby Murray, Olga Ohrimenko +2
We consider the problem of how to verify the security of probabilistic oblivious algorithms formally and systematically. Unfortunately, prior program logics fail to support a numbe…
Proving the Absence of Microarchitectural Timing Channels
Scott Buckley, Robert Sison, Nils Wistoff +4
Microarchitectural timing channels are a major threat to computer security. A set of OS mechanisms called time protection was recently proposed as a principled way of preventing in…
Verified Secure Compilation for Mixed-Sensitivity Concurrent Programs
Robert Sison, Toby Murray
Proving only over source code that programs do not leak sensitive data leaves a gap between reasoning and reality that can only be filled by accounting for the behaviour of the com…