Joomy Korkut will present his FPO "Foreign Function Verification Through Metaprogramming" on October 9th, 2024 at 3pm in Friend 202.

All are welcome to attend.

Abstract:

CertiCoq is a compiler from Coq to C that is verified in Coq. Thanks to CertiCoq’s mechanically checked proof of compiler correctness, users can be sure that programs they write and verify in Coq’s rich type system output the same results when compiled to C (and to machine language, via the CompCert verified compiler). However, in practice, large programs are rarely written in a single language; additional languages are used for better performance or for capabilities that the primary language lacks. In particular, because Coq lacks user-defined primitive types, mutation, and input/output actions, CertiCoq-compiled code must interact with another language to have those capabilities. Specifically, Coq code must be able to call C code and C code must be able to inspect and generate Coq values and call Coq code. But what happens to the correctness proofs when these two languages interact?

A foreign C function has to be memory-safe, return the expected result, and have the expected side effect (or no effect). A specification that expresses these requirements must combine plain Coq, for the functional parts, and a program logic for C (such as the Verified Software Toolchain [VST]), for the verification of C functions. While VST is embedded in Coq, its specification language is quite different. Bridging this gap by connecting plain Coq and VST theorems in both directions requires a system of techniques and methods, many of which are made feasible by using metaprogramming as a general methodological approach. In this dissertation, I describe these techniques and methods.

VST proofs about C foreign functions do not directly translate to proofs about Coq primitives. To bridge this gap, I propose a method of relating foreign functions and types to their functional models, allowing users to write proofs in plain Coq. I also provide examples of Coq programs with primitive types, mutation, and I/O actions, along with their correctness proofs, and demonstrate VeriFFI, the verified foreign function interface for CertiCoq.