BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:How formal reasoning enables the detection of microarchitectural s
 ide channels - Jana Hofmann (Microsoft)
DTSTART:20231027T120000Z
DTEND:20231027T130000Z
UID:TALK206254@talks.cam.ac.uk
CONTACT:Yuting Shang
DESCRIPTION:**Abstract**: In this talk I will discuss how a transition fro
 m a theory-heavy PhD to more application-oriented research in industry mig
 ht look like\, and why for me\, that step did not feel so big after all. D
 uring my PhD\, I worked on so-called ‘hyperproperties’\, an abstract c
 lass of properties that relate multiple execution traces of a system. I de
 veloped logics for hyperproperties\, studied their decidability\, and prop
 osed algorithms for their verification and synthesis problems. Today\, in 
 my role as researcher at Microsoft\, I focus on modelling information leak
 age through microarchitectural side channels. I will show how these two to
 pics connect and how hyperproperty reasoning techniques enable an efficien
 t modelling and testing process to detect information leakage in modern CP
 Us.\n\n**Bio**: Jana Hofmann is a postdoctoral researcher at Azure Researc
 h\, Microsoft\, where she works on detecting and preventing information le
 akage through microarchitectural side channels. Before joining Microsoft\,
  Jana obtained a Ph.D. from Saarland University/CISPA Helmholtz Center for
  Information Security (Germany)\, where she was advised by Bernd Finkbeine
 r. She also holds a Master’s degree in Computer Science from the Univers
 ity of Edinburgh.\n
LOCATION:Computer Laboratory\, William Gates Building\, LT2
END:VEVENT
END:VCALENDAR