[PriSC'26] Towards formally secure compilation of verified F* programs against unverified ML(…)

Описание: Towards formally secure compilation of verified F* programs against unverified ML contexts (Video, PriSC 2026)
Cezar-Constantin Andrici, Danel Ahman, Cătălin Hriţcu, Guido Martínez, Abigail Pribisova, Exequiel Rivas, and Théo Winterhalter
(MPI-SP; University of Ljubljana; MPI-SP; Microsoft Research; MPI-SP and MPI-SWS; Tallinn University of Technology; Ahrefs; INRIA)

Abstract: We are working towards a formally secure compilation framework to compile verified F* programs to an ML language. The framework, itself written and verified in F*, aims to compile verified F* programs and link them with unverified ML programs securely, so that any unverified code cannot inadvertently or maliciously break the internal invariants of the verified code. In previous work on this project we have built formally secure compilation frameworks between shallowly embedded subsets of F*—i.e., we used shallow embeddings not only for the verified code (which is standard in F*) but also for the unverified code. To compile further to OCaml, we relied on F*’s extraction mechanism, which is, however, unverified. In this extended abstract, we present ongoing work on extending our framework with a formally secure compilation step to an ML language deeply embedded in F*, thus achieving end-to-end security guarantees.


Presentation at the PriSC 2026 workshop, Jan 11, 2026, https://popl26.sigplan.org/home/prisc...
Sponsored by ACM SIGPLAN.