Misquoted No More: Securely Extracting F* Programs with IO

TL;DR

The paper addresses the challenge of securely extracting shallowly embedded $IO^{\star}$ programs from the dependently typed language $F^{\star}$ into a deeply embedded $\lambda_{io}$ calculus, while preserving security in the presence of arbitrary unverified contexts. It introduces SEIO$^{\star}$, combining relational quotation (a typing-derivation based translation validation) with a pure, verified syntax-generation step, and proves Robust Relational Hyperproperty Preservation (RrHP) via two cross-language logical relations and machine-checked proofs in $F^{\star}$. The main contributions are the formalization of relational quotation, the trace-producing semantics linking $IO^{\star}$ and $\lambda_{io}$, and the instantiation of a secure extraction model that ensures end-to-end security guarantees, including full abstraction and trace/hyperproperty preservation. The work advances the state of certified extraction by reducing reliance on translation validation and enabling secure linking with unverified code, with practical implications for verified cryptographic and AI-enabled components and a pathway toward broader integration with existing secure compilation stacks.

Abstract

Shallow embeddings that use monads to represent effects are popular in proof-oriented languages because they are convenient for formal verification. Once shallowly embedded programs are verified, they are often extracted to mainstream languages like OCaml or C and linked into larger codebases. The extraction process is not fully verified because it often involves quotation -- turning the shallowly embedded program into a deeply embedded one -- and verifying quotation remains a major open challenge. Instead, some prior work obtains formal correctness guarantees using translation validation to certify individual extraction results. We build on this idea, but limit the use of translation validation to a first extraction step that we call relational quotation and that uses a metaprogram to construct a typing derivation for the given shallowly embedded program. This metaprogram is simple, since the typing derivation follows the structure of the original program. Once we validate, syntactically, that the typing derivation is valid for the original program, we pass it to a verified syntax-generation function that produces code guaranteed to be semantically related to the original program. We apply this general idea to build SEIO*, a framework for extracting shallowly embedded F* programs with IO to a deeply embedded lambda-calculus while providing formal secure compilation guarantees. Using two cross-language logical relations, we devise a machine-checked proof in F* that SEIO* guarantees Robust Relational Hyperproperty Preservation (RrHP), a very strong secure compilation criterion that implies full abstraction as well as preservation of trace properties and hyperproperties against arbitrary adversarial contexts. This goes beyond the state of the art in verified and certifying extraction, which so far has focused on correctness rather than security.

Figures (4)

• Figure 1: An overview of extraction using SEIO$^{\star}$. Solid lines are verified pure F$^{\star}$ functions. The dashed arrow represents the relational quotation metaprogram, the result of which is checked by F$^{\star}$ to be a typing derivation for the original verified program.
• Figure 2: Running example: a validation wrapper for unverified agents.
• Figure 3: The typing relation for $^\star$.
• Figure 4: Compilation pipeline from $\lambda_{io}$ to executable.

Theorems & Definitions (5)

• theorem 1: Robust Relational Hyperproperty Preservation (RrHP)
• theorem 2: RrHP $\Rightarrow$
• proof : Proof sketch
• theorem 3: RrHP $\Leftarrow$
• proof : Proof sketch