Jana Hofmann is a postdoctoral researcher at Azure Research, Microsoft. She obtained her PhD in 2022 at CISPA/Saarland University, for which she was awarded the university’s Dr.-Eduard-Martin Prize for best computer science thesis of the year. Her research interests lie in the intersection of formal methods and security with publications at LICS, CAV, USENIX Security, and CSF. She develops formal algorithms and testing methods for relational properties with a current focus on microarchitectural information leakage.

AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI   Info

AG Audience

English

60 Minutes

Bochum

Establishing strong guarantees for security-critical systems has never been more challenging. On the one hand, systems become increasingly complex and intricate. On the other hand, many security requirements are relational, i.e., they compare several execution traces. Examples are noninterference properties, program indistinguishability, and even algorithmic fairness. Due to their relational nature, formal reasoning about such properties quickly blows up in complexity. In this talk, I discuss the necessity to scale relational reasoning to larger software and black-box systems and present two of our recent contributions to tackle this challenge. In the first part, I focus on formal algorithms for white-box systems and show how to combine relational reasoning with non-relational specifications to enable the synthesis of smart contract control flows. In the second part, I focus on relational testing of black-box systems and illustrate its use in modeling and detecting microarchitectural information leakage in modern CPUs.

Annika Meiser

+49 681 9303 9105

--email hidden

Zoom

668 9092 0474

passcode not visible

logged in users only