Certifying C program correctness with respect to CompCert with VeriFast
Stefan Wils, Bart Jacobs

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Security and Verification in Computing · Formal Methods in Verification
