Colloquium Details
Verifying Security Across Hardware & Software
Speaker: Klaus v. Gleissenthall, University of California, San Diego
Location: TBA
Date: April 1, 2020, 2 p.m.
Host: Michael Overton
Synopsis:
To keep our data secure, we have to make sure hat safety-critical code operates correctly, for example by verifying its correctness through mathematical proof. Even though such verified infrastructure has seen considerable success and real-world deployment, correctness guarantees today
focus on software and rely on simplified assumptions about the hardware. Unfortunately, real-world hardware is full of fast-paths and performance optimizations like speculative execution. As a result, the simple assumptions about the hardware on which our proofs rely often don't hold in the real world causing even verified software to leak.
My goal is to provide end-to-end guarantees for real-world systems by validating assumptions across the stack. I will discuss my approach to proving that hardware doesn't leak through timing side-channels, how to model speculative execution semantics and finally how to automatically fix speculative execution based vulnerabilities.
Speaker Bio:
Klaus v. Gleissenthall is a postdoctoral scholar at the University of California, San Diego where he works with Ranjit Jhala and Deian Stefan. Klaus research interests lie at the intersection of Programming Languages, Verification and Security, focusing on providing end-to-end assurance across the stack. Klaus completed his Ph.D. at the Technical University of Munich, where he was advised by Andrey Rybalchenko. During his Ph.D., Klaus also spent time at Microsoft Research Cambridge, both as an intern and as a visitor. Klaus has received a Microsoft Research Scholarship and was awarded the distinction summa cum laude for his Ph.D. research.