BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium: Verifying Security Across Hardware & Software
DTSTART:20200220T101500
DTEND:20200220T111500
DTSTAMP:20260407T183942Z
UID:dd5e4d6ffc091ad1edd724bc2756da1af76f8aee9c84fdfcb27ef206
CATEGORIES:Conferences - Seminars
DESCRIPTION:By: Klaus von Gleissenthall - UC San Diego\nIC Faculty candida
 te\n\nAbstract:\nTo keep our data secure\, we have to make sure hat safety
 -critical code operates correctly\, for example by verifying its correctne
 ss through mathematical proof. Even though such verified infrastructure ha
 s seen considerable success and real-world deployment\, correctness guaran
 tees today focus on software and rely on simplified assumptions about the 
 hardware.\n\nUnfortunately\, real-world hardware is full of fast-paths and
  performance optimizations like speculative execution. As a result\, the s
 imple assumptions about the hardware on which our proofs rely often don't 
 hold in the real world causing even verified software to leak.\n\nMy goal 
 is to provide end-to-end guarantees for real-world systems by validating a
 ssumptions across the stack. I will discuss my approach to proving that ha
 rdware doesn't leak through timing side-channels\, how to model speculativ
 e execution semantics and finally how to automatically fix speculative exe
 cution based vulnerabilities.\n\nBio:\nKlaus v. Gleissenthall is a postdoc
 toral scholar at the University of California\, San Diego where he works w
 ith Ranjit Jhala and Deian Stefan. Klaus\nresearch interests lie at the in
 tersection of Programming Languages\, Verification and Security\, focusing
  on providing end-to-end assurance across the stack. Klaus completed his P
 h.D. at the Technical University of Munich\, where he was advised by Andre
 y Rybalchenko. During his Ph.D.\, Klaus also spent time at Microsoft Resea
 rch Cambridge\, both as an intern and as a visitor. Klaus has received a M
 icrosoft Research Scholarship and was awarded the highest distinction summ
 a cum laude for his Ph.D. research.\n\nMore information\n 
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR