Jana Hofmann

I’m a tenure-track faculty at Max-Planck Institute for Security and Privacy (MPI-SP), where I lead the group for Formal Security Engineering. I am also a principle investigator at the CASA Cluster of Excellence at Ruhr University, Bochum. Previously, I was a researcher at Azure Research, Microsoft. I obtained my PhD from Saarland University while working at CISPA.

I develop techniques to establish strong security guarantees at the hardware-software interface, with a focus on information flow security. Much of my work addresses microarchitectural side channels, where I design methods to detect, formally specify, and ultimately prevent information leakage. My research combines techniques from formal methods, programming languages, and systems security research. I am working on both verification approaches for smaller, white-box hardware designs and model-based testing for larger-scale software and black-box hardware.

open positions

I am hiring! I welcome applications for PhD and postdoc positions. Write me an email if you are interested in systems security and/or formal methods! Please include your CV and your university transcripts. I also offer Bachelor’s and Master’s theses.

news

Jun 10, 2026	Our paper Principled Design of Indexing Functions for Memory Coloring was accepted at Usenix Security’26! In this paper, we investigate how to make simultaneous partitioning of multiple shared microarchitectural components practical - by synthesizing new indexing functions.
May 20, 2026	Our paper Enter, Exit, Page Fault, Leak: Testing Isolation Boundaries for Microarchitectural Leaks was awarded a Distinguished Paper Award at S&P!
May 05, 2026	I’m very proud to announce that Clara Schneidewind’s and my course Functional Programming was nominated for the RUB Excellent Teaching Award! Update (June’26): We actually won the award! Yay!
Apr 13, 2026	Our paper A Deductive System for Contract Satisfaction Proofs will appear at PLDI’26. The preprint is available on ArXiv.

older news

recent publications

USENIX Security

Principled Design of Indexing Functions for Memory Coloring

Stephan Dübler, Jana Hofmann, Boris Köpf, and Stavros Volos

In 35th USENIX Security Symposium (USENIX Security 26), Aug 2026

Distinguished Artifact Award Bib PDF

The artifact accompanying the paper received a distinguished artifact award.

@inproceedings{dbler2026principled,
  author = {D{\"u}bler, Stephan and Hofmann, Jana and K{\"{o}}pf, Boris and Volos, Stavros},
  title = {Principled Design of Indexing Functions for Memory Coloring},
  booktitle = {35th USENIX Security Symposium (USENIX Security 26)},
  year = {2026},
  address = {Baltimore, MD},
  publisher = {USENIX Association},
  month = aug,
}

PLDI

A Deductive System for Contract Satisfaction Proofs

Arthur Correnson, Haoyi Zeng, and Jana Hofmann

Proc. ACM Program. Lang., Jun 2026

DOI Bib PDF

@article{deductiveProofSystem,
  author = {Correnson, Arthur and Zeng, Haoyi and Hofmann, Jana},
  title = {A Deductive System for Contract Satisfaction Proofs},
  year = {2026},
  publisher = {{ACM}},
  url = {https://doi.org/10.1145/3808251},
  doi = {10.1145/3808251},
  journal = {Proc. ACM Program. Lang.},
  month = jun,
  articleno = {173},
  numpages = {25}
}

S&P

Enter, Exit, Page Fault, Leak: Testing Isolation Boundaries for Microarchitectural Leaks

Oleksii Oleksenko, Flavien Solt, Cédric Fournet, Jana Hofmann, Boris Köpf, and 1 more author

In IEEE Symposium on Security and Privacy, May 2026

Accepted at IEEE SP 2025, publication delayed due to embargo.

Distinguished Paper Award Bib PDF

Received distinguished paper award at S&P’26 (retroactively for S&P’25).

@inproceedings{oleksenko2026enter,
  author = {Oleksenko, Oleksii and Solt, Flavien and Fournet, Cédric and Hofmann, Jana and K{\"{o}}pf, Boris and Volos, Stavros},
  title = {Enter, Exit, Page Fault, Leak: Testing Isolation Boundaries for Microarchitectural Leaks},
  booktitle = {IEEE Symposium on Security and Privacy},
  year = {2026},
  month = may,
  url = {https://www.microsoft.com/en-us/research/publication/enter-exit-page-fault-leak-testing-isolation-boundaries-for-microarchitectural-leaks/},
  note = {Accepted at IEEE SP 2025, publication delayed due to embargo.},
}

more publications