Certifying C program correctness with respect to CompCert with VeriFast

TL;DR

This paper introduces a method to generate formal correctness certificates for C programs verified by VeriFast, linking VeriFast's symbolic execution with Coq proofs and the CompCert semantics to enhance trustworthiness.

Contribution

It presents a novel extension that produces Coq certificates for VeriFast verification results, bridging VeriFast, Coq, and CompCert semantics for verified C program correctness.

Findings

Generated Coq certificates can verify VeriFast's correctness proofs.

The certificates relate VeriFast's symbolic execution to formal semantics.

The approach increases trust in VeriFast's verification results.

Abstract

VeriFast is a powerful tool for verification of various correctness properties of C programs using symbolic execution. However, VeriFast itself has not been verified. We present a proof-of-concept extension which generates a correctness certificate for each successful verification run individually. This certificate takes the form of a Coq script containing two proofs which, when successfully checked by Coq, together remove the need for trusting in the correctness of VeriFast itself. The first proves a lemma expressing the correctness of the program with respect to a big step operational semantics developed by ourselves, intended to reflect VeriFast's interpretation of C. We have formalized this semantics in Coq as cbsem. This lemma is proven by symbolic execution in Coq, which in turn is implemented by transforming the exported AST of the program into a Coq proposition representing the symbolic execution performed by VeriFast itself. The second proves the correctness of the same C program with respect to CompCert's Clight big step semantics. This proof simply applies our proof of the soundness of cbsem with respect to CompCert Clight to the first proof.