Cezar-Constantin Andrici

PhD working on ways to practically verify code and to securely compile it.

I’m a Ph.D. candidate at MPI-SP, Bochum, Germany working with Cătălin Hriţcu. My Ph.D. project is about secure interoperability between verified F* programs and unverified ML code. I earned my Bachelor’s and Master’s degrees in Computer Science from Alexandru Ioan Cuza University of Iași, Romania. I also hold a Master’s degree in Regional Development from the same university.

Research interests

Verification of effectful code. In a pure dependently-typed language, like Rocq or F*, one can write pure terminating computations and verify them. If one wants to write effectful computations (e.g., with state, non-termination, input/output (IO), etc.), then one has to give a representation to those computations. One common way is to do a shallow embedding, by embedding the effect in the language using a monad. F* has this idea at its core and uses a construction called the Dijkstra monad. Such constructions were used successfully to verify big developments and realistic projects. My work in this space was involved into finding the pre-conditional effect (specific to F*), and building Dijkstra monads for terminating/non-terminating IO and Monotonic State. These results are interesting because the effects F* supports out of the box do not have a monadic representation (are axiomatized), and if one finds a representation for each of them, the TCB of F* would be minimized. Right now, I am interested in finding a monadic representation for the effects Div, Ghost, Monotonic State with higher-order stores, and Concurrency with IO.

Secure Compilation of F*. The language F* was used successfully in the verification of some big projects, some of them milestones in the verification community. One convenient feature of F* is primitive extraction to OCaml of effectful computations, meaning that the monadic representation of the computation is erased during extraction and the monad’s operations are replaced with the corresponding OCaml operations. This extraction, however, it is part of the TCB of F* so it is not verified to be correct. Moreover, if the verified extracted code gets linked to unverified code, then there is a chance of a bug, or an attack, so it may be even insecure (the logical invariants proved about the verified code are broken by the unverified code). To bring some trust to this, my work proposes SCIO* and SecRef*, two secure compilation frameworks for verified IO programs, and respectively stateful programs, that can be safely linked with unverified code. The long-term goal of the project is to have secure interoperability between F* and OCaml.

Publications, drafts and extended abstracts

Talks

  • Securing Verified IO Programs Against Unverified Code in F*.
    At the 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), January 2024 (Video),
    and an extended version at the F* PoP Up Seminar, July 2023 - (video).
  • Verifying non-terminating programs with IO in F* (Extended Abstract).
    At the 10th ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE), September 2022.
    Slides. Video.
  • Gradual Enforcement of IO Trace Properties at Student Research Competition,
    At the 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), August 2020.
    Video
  • Verification of IO programs in F* at Faculty of Computer Science, UAIC, January 2020.

Teaching Assistant

  • Proofs are Programs, RUB, Bochum, WS 2024-2025
  • Functional Programming, RUB, Bochum, SS 2023-2024
  • Logics in Computer Science, UAIC, Iași, WS 2020-2021

Scientific Service

  • Sub-reviewer at ICFP’25, POPL’24, SP’21
  • Member in Artifact Evaluation Committee at POPL’23
  • Student Volunteer at POPL’24, POPL’23, ICFP’22, PLDI’20, POPL’20, ETAPS’19, FROM’18