I am a tenure-track researcher at the Max Planck Institute for Security and Privacy (MPI-SP). I investigate how to establish trust in information systems by giving strong security and privacy guarantees, for both hardware and software. My work focuses on detecting, specifying, and preventing information leakage through microarchitectural side-channels. I develop specifiaction languages and models, verification and synthesis algorithms, as well as testing techniques for black-box systems.

Previously, I was a researcher at Azure Research, Microsoft, where I worked on detection mechanisms and defenses for microarchitectural side-channels. I obtained my PhD from Saarland University (while working at CISPA) in 2022, where I was advised by Bernd Finkbeiner. My thesis was awarded with Saarland University’s Dr.-Eduard-Martin prize for the best computer science dissertation of the year. A 10-page summary of my thesis (with a focus on logics) can be found here.

News!

• Our paper Principled Microarchitectural Isolation on Cloud CPUs won a distinguished paper award at CCS’24!
• I will serve as Sponsorship Chair at CAV’25. I’ve also joined the PC of the Formal Methods & Programming Languages track at CCS’25.
• July’24: We have two papers accepted at CCS’24! One titled Gaussian Elimination of Side-Channels: Linear Algebra for Memory Coloring and the other titled Principled Microarchitectural Isolation on Cloud CPUs.
• April’24: I will start as a tenure-track faculty at MPI-SP in October 2024.

Publications

• Gaussian Elimination of Side-Channels: Linear Algebra for Memory Coloring
  With Stavros Volos, Cédric Fournet, and Boris Köpf
  ACM Conference on Computer and Communications Security 2024 (CCS 2024).
• Principled Microarchitectural Isolation on Cloud CPUs
  With Stavros Volos, Cédric Fournet, Boris Köpf, and Oleksii Oleksenko
  ACM Conference on Computer and Communications Security 2024 (CCS 2024).
  Distinguished Paper Award
• Reactive Synthesis of Smart Contract Control Flows
  With Bernd Finkbeiner, Noemi Passing, and Florian Kohn
  21st International Symposium on Automated Technology for Verification and Analysis (ATVA 2023).
• Speculation at Fault: Modeling and Testing Microarchitectural Leakage of CPU Exceptions
  With Emanuele Vannacci, Cédric Fournet, Boris Köpf, and Oleksii Oleksenko
  USENIX Security 2023.
• Automata-Based Software Model Checking of Hyperproperties
  With Bernd Finkbeiner, Hadar Frenkel and Janine Lohse
  NASA Formal Methods (NFM 2023).
• Smart Contract Synthesis Modulo Hyperproperties
  With Norine Coenen, Bernd Finkbeiner and Julia Tillman
  36th IEEE Computer Security Foundations Symposium (CSF 2023).
  Distinguished Paper Award
• Logical Methods for the Hierarchy of Hyperlogics
  Dissertation, Saarland University, 2022.
  10-page summaries: English, German
  Dr.-Eduard-Martin prize
• Deciding Hyperproperties Combined with Functional Specifications
  With Raven Beutner, David Carral, Bernd Finkbeiner and Markus Krötzsch
  37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022).
• Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity
  With Jonni Virtema, Bernd Finkbeiner, Juha Kontinen, and Fan Yang
  41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021).
• Runtime Enforcement of Hyperproperties
  With Norine Coenen, Bernd Finkbeiner, Christopher Hahn and Yannick Schillo
  19th International Symposium on Automated Technology for Verification and Analysis (ATVA 2021).
• The Hierarchy of Hyperlogics: A Knowledge Reasoning Perspective
  With Norine Coenen, Bernd Finkbeiner and Christopher Hahn
  17th International Conference on Principles of Knowledge Representation and Reasoning, Recently Published Research Track (KR 2020).
• Realizing Omega-regular Hyperproperties
  With Bernd Finkbeiner, Christopher Hahn and Leander Tentrup
  32nd International Conference on Computer-Aided Verification (CAV 2020).
• The Hierarchy of Hyperlogics
  With Norine Coenen, Bernd Finkbeiner and Christopher Hahn
  34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019).

Presentations

• Gaussian Elimination of Side-Channels: Linear Algebra for Memory Coloring
  Paper presentation at CCS’24
• Testing for Microarchitectural Information Flow Security
  Invited talk at HYPER@CAV workshop, July 2024
• Formal Reasoning for the Detection of Microarchitectural Side Channels
  Invited talk at Woman@CL at Cambridge University, October 2023
• Smart Contract Synthesis Modulo Hyperproperties
  Paper presentation at CSF’23
• Speculation at Fault: Modeling and Testing Microarchitectural Leakage of CPU Exceptions
  
  • Invited talk at Seoul National University, October 2023
  • Invited talk at Stanford University, August 2023
  • Invited talk at CISPA Helmholtz Center for Information Security, May 2023
• Deciding Hyperproperties Combined with Functional Specifications
  Paper presentation at LICS’22
• Logics for the Specification of Hyperproperties
  Speaker at the 4th CISPA-LORIA workshop, April 2022
• The Hierarchy of Hyperlogics: A Knowledge Reasoning Perspective
  Recently published research track at KR’22, YouTube recording
• Logics for Hyperproperties
  
  • Invited talk at IST Austria, July 2020
  • Invited talk at Tel Aviv University, September 2019
  • Invited talk at Yale University, July 2019
  • Invited talk at UC Berkeley, July 2019
• The Hierarchy of Hyperlogics
  Paper presentation at LICS’19

Teaching

Supervised Students

• Janine Lohse, Bachelor’s thesis: Model Checking for (Hyper) Temporal Stream Logic (2022)
• Yannick Schillo, Research project: Specifying Android Apps with TSL (2020 - 2022)
• Frederik Scheerer, Bachelor’s thesis: Monitoring Smart Contracts with RTLola (2021)
• Julia Tillman, Bachelor’s thesis: Temporal Stream Logic for Hyperproperties (2020)
• Matthias Cosler, Bachelor’s thesis: Towards Synthesizing Smart Contracts: Reducing ATL* Synthesis to HyperLTL Synthesis (2019)

Assisted Lectures

During PhD

• Winter 2020/2021: Assistant for Basic Course Programmierung 1
  received Busy Beaver award for outstanding teaching performance
• Winter 2019/2020: Assistant for Core Course Verification
• Summer 2019: Advisor for Proseminar Softwarezuverlässigkeit (Software Reliability)
• Winter 2018/2019: Assistant for Seminar Hyperproperties

Before PhD

• Summer 2018: Coach for Mathematics Precourse at Saarland University
• Summer 2017: Lecturer and Coach for Mathematics Precourse at Saarland University
  BeStE award for student initiatives and extraordinary commitment
• Summer 2017: Student TA for Theoretical Computer Science at the School of Informatics, University of Edinburgh
• Winter 2016/2017: Student TA for Informatics I – Functional Programming at the School of Informatics, University of Edinburgh
• Summer 2016: Coach for Mathematics Precourse, Saarland University
• Summer 2016: Student TA for Concurrent Programming, Saarland University
• Winter 2015/2016: Organizer of Didactic Seminar for Re-exam Student TAs
• Winter 2015/2016: Supervision Student TA for Programming 1, Saarland University
• Summer 2015: Coach for Mathematics Precourse at Saarland University, Saarland University
• Winter 2014/2015: Organizer of Didactic Seminar for Re-exam Student TAs, Saarland University
• Winter 2014/2015: Student TA for Programming 1, Saarland University
• Winter 2013/2014: Re-exam Student TA for Programmierung 1, Saarland University

Scientific Service

• Program Committee: CSF’25, CAV’24, CSF’24, ICTAC’23, CAV’22 Artifact Evaluation
• External Reviewer: LICS’22, TACAS’21, MFCS’21, CONCUR’21, ATVA’21, CAV’21, LICS’21, CONCUR’20, KR’20, ICALP’20, TACAS’20, CSL’20, ATVA’19

Short CV

• Since Oct’2024: Tenure-Track Faculty at MPI-SP
• 2022 - 2024: Postdoctoral Researcher at Microsoft Research / Azure Research
• 2018 - 2022: Dr. rer. nat. at Saarland University / CISPA
• 2016 - 2017: M.Sc. in Computer Science at University of Edinburgh
• 2013 - 2016: B.Sc. in Computer Science at Saarland University