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.

翻译：VeriFast是一款利用符号执行验证C程序各类正确性属性的强大工具，但其自身尚未经过验证。我们提出一种概念验证扩展方案，可为每次成功的验证运行独立生成正确性证书。该证书以Coq脚本形式呈现，当该脚本被Coq成功检查后，即可消除对VeriFast自身正确性的信任需求。该Coq脚本通过应用一系列可靠性结果，在Coq中基于符号执行证明程序正确性，进而依据第三方CH2O小步语义（针对C11）验证程序正确性。该证明链包含两个中间辅助大步语义，其中最重要的语义描述了VeriFast对C语言的解释。最后，Coq中的符号执行通过将程序导出的抽象语法树转换为表示VeriFast自身所执行符号执行的Coq命题来实现。