I’m a Ph.D. candidate at MPI-SP, Bochum, Germany working with Cătălin Hriţcu. My research focuses on building the first secure compiler for verified code, by developing a secure compiler from the proof-oriented programming language F* to OCaml. Existing (insecure) compilers erase all the annotations with which the code was verified, thus, making the resulting compiled code vulnerable when linked against adversarial code. To fix this, a secure compiler exploits available mechanisms to enforce the assumptions made in the annotations. In my most recent paper, POPL’24, we present a secure compiler for verified IO programs that converts the assumptions into dynamic checks.

News

• Our most recent paper was accepted at POPL 2024!