EECS Faculty Candidate Seminar: Farzaneh Derakhshan

Quantitative Reasoning for Concurrent and Interactive Programs

Abstract

Modern software is built from components that interact: threads sharing GPU memory, processes exchanging messages, and AI agents coordinating with one another. Classical security guarantees for such systems are all-or-nothing: a program either leaks secret information or it does not, and a component either is fully verified or contributes nothing to the guarantee of the whole. Real systems can rarely afford such absolutes. Almost every system leaks something, and most combine a few verified components with many that are only tested.

In this talk, I will present a compositional approach that makes these guarantees quantitative: measuring how much a component leaks or how far it can be trusted, and composing those measures into a guarantee for the whole system. The centerpiece is our work on message-passing programs. I will show how well-typed probabilistic programs give rise to distributions over communication traces, and how these distributions let us measure the gain of an active attacker. I will then briefly discuss how similar ideas apply to GPU programs, where execution cost is observable to an attacker. I will close with my research vision: extending these guarantees to systems that mix verified, tested, and machine-generated components, and to opaque participants such as AI agents whose internals we cannot inspect.

Biography

Farzaneh Derakhshan is a Research Assistant Professor in the Department of Computer Science at Northwestern University. Her research spans programming languages, formal methods, and language-based security, with a focus on making the guarantees of concurrent systems quantitative and compositional. She received her PhD in pure and applied logic from Carnegie Mellon University, advised by Frank Pfenning, and was a postdoctoral fellow at CMU’s CyLab Security and Privacy Institute. She is the PI on an NSF award on compositional reasoning about systems with different assurance levels. Her work has appeared at POPL, LICS, CSF, ESOP, OOPSLA, and TOPLAS, and her ESOP 2026 paper received the EATCS Best Theoretical Paper Award at ETAPS.