Certifying C program correctness with respect to CH2O with VeriFast
share
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.
READ FULL TEXT