Certifying C program correctness with respect to CH2O with VeriFast

TL;DR

This paper introduces a method to generate correctness certificates for C programs verified by VeriFast, using Coq to ensure trustworthiness and formal correctness with respect to C11 semantics.

Contribution

It presents a novel approach to certify VeriFast's verification results by producing Coq certificates, bridging symbolic execution with formal proof in Coq for C programs.

Findings

Successfully generated Coq certificates for verified C programs.

Proved correctness of VeriFast's symbolic execution against C11 semantics.

Enhanced trustworthiness of VeriFast 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 which, when successfully checked by Coq, removes the need for trusting in the correctness of VeriFast itself. The Coq script achieves this by applying a chain of soundness results, allowing us to prove correctness of the program with regards to the third-party CH2O small step semantics for C11 by proving correctness in terms of symbolic execution in Coq. This proof chain includes two intermediate auxiliary big step semantics, the most important of which describes VeriFast's interpretation of C. Finally, symbolic execution in Coq is implemented by transforming the exported AST of the program into a Coq proposition representing the symbolic execution performed by VeriFast itself.