CS Special Seminar: Simon Gregersen "Formal Verification for Secure Software Systems"

Formal Verification for Secure Software Systems

Simon Gregersen
New York University
Google Scholar

Abstract: Bugs and security breaches in software systems can be costly. Testing is often insufficient to uncover all errors because some may only appear under certain circumstances. In response, researchers have developed formally verified systems that come with machine-checked mathematical proofs. These proofs rule out entire classes of bugs and security issues that would be difficult to catch with testing alone. In recent years, multiple realistic software systems have been formally verified, including compilers, microkernels, and cryptographic primitives. Despite these successes, formal verification of many important kinds of programs and properties remains challenging, if not impossible, with known techniques.

In this talk, I will introduce my research on formal verification techniques for correct and secure software systems. In particular, I will give an overview of my work on two long-standing problems: modular verification of distributed systems and probabilistic programs. I will then discuss how I plan to develop and use these techniques in the future to reason about cryptographic protocol security, model type- and language-based constructions for security and privacy, and develop new abstractions for compositional reasoning.

Bio: Simon Oddershede Gregersen is a postdoctoral fellow at the Courant Institute of Mathematical Sciences of New York University. His research interests lie in programming languages, formal verification, and security. His work currently focuses on program logics for reasoning about security properties, distributed systems, and probabilistic programs. His work regularly appears at top conferences such as CCS, POPL, OOPSLA, ICFP, and ESOP. Simon received his PhD in Computer Science from Aarhus University, Denmark, in March 2023 and is the recipient of a Carlsberg Foundation Internationalization fellowship and an ACM SIGPLAN Distinguished Paper Award.