I would like to announce the release of Security Foundations, a new volume in the Software Foundations textbook series that studies the security of programs by setting clear security goals and developing provable enforcement mechanisms. Topics include noninterference, security type systems, secure multi-execution, cryptographic constant time, and speculative load hardening. https://softwarefoundations.cis.upenn.edu/secf-current/index.html

Cătălin Hrițcu is a tenured faculty at the Max Planck Institute for Security and Privacy (MPI-SP) where he leads the Formally Verified Security group. He is also an Adjunct Professor (APL) in the Faculty of Computer Science of Ruhr Uni Bochum (RUB), as well as a member of HGI and the CASA Cluster of Excellence at RUB. Before joining MPI-SP, Catalin was a Tenured Researcher at Inria Paris, a Visiting Researcher at Microsoft Research, and a PostDoc at University of Pennsylvania. He received a PhD from Saarland University and a Habilitation from ENS Paris.

Catalin is interested in formal methods for security (secure compilation, compartmentalization, memory safety, speculative execution defenses, information flow control, security protocols), programming languages (program verification, proof assistants, dependent types, formal semantics, property-based testing), and the design and verification of security-critical systems (compilation chains, reference monitors, tagged architectures, high-assurance crypto). He was awarded an ERC Starting Grant on formally secure compilation and was also involved in the design of the F* verification system. His research received Distinguished Paper Awards at the Computer Security Foundations (CSF) symposium in 2019, 2021, and 2025.