SHF: Small: VeriFFI -- Formally Verified Functional+C programs

Princeton University, Princeton NJ

Investigators

Abstract

Formal deductive verification -- machine-checked proofs of program correctness using tools such as proof assistants -- is an effective way of building very high assurance secure components, such as operating-system kernels and cryptographic communications primitives. Existing logics, tools, and methods for program verification apply either to low-level languages (such as C) or high-level functional languages. But real-world systems are programmed in a mix of languages: low-level imperative languages for components such as operating-system (OS) kernels and cryptographic primitives; high-level languages for most applications, for OS-management code, for cryptographic protocols, and for the runtime systems of the high-level languages. This project develops methods and tools for formal verification of high-level language programs linked with low-level programs, proved correct to a unified specification that crosses the boundary with no gaps. The high-level language is the functional programming language inside the Coq proof assistant, verified using Coq’s logic, and compiled (provably correctly) with the CertiCoq compiler. The low-level language is C, verified using the Verified Software Toolchain (VST), and compiled (provably correctly) using the CompCert verified C compiler. The new Verified Foreign Function Interface (VeriFFI) exploits synergies between CertiCoq’s toolchain and VST/CompCert to enable such unified verifications. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.