用 VeriFast 证明 C 程序相对于 CompCert 的正确性并生成证书
计算机科学中的逻辑
2021-10-22 v1 编程语言
摘要
VeriFast 是一款利用符号执行验证 C 程序多种正确性属性的强大工具。然而 VeriFast 本身未经验证。我们给出一个概念验证扩展，其为每次成功的验证运行单独生成正确性证书。该证书采用 Coq 脚本形式，含两段证明；当 Coq 成功检查后，二者共同免除对 VeriFast 自身正确性的信任需求。第一段证明一个引理，表达程序相对于我们自行开发的大步操作语义的正确性，该语义意在反映 VeriFast 对 C 的解释。我们已在 Coq 中将此语义形式化为 cbsem。该引理通过在 Coq 中符号执行证明，而符号执行通过将导出的程序 AST 转换为表示 VeriFast 所执行符号执行的 Coq 命题来实现。第二段证明同一 C 程序相对于 CompCert 的 Clight 大步语义的正确性。该证明仅将我们关于 cbsem 相对于 CompCert Clight 可靠性的证明应用于第一段证明。
引用
@article{arxiv.2110.11034,
title = {Certifying C program correctness with respect to CompCert with VeriFast},
author = {Stefan Wils and Bart Jacobs},
journal= {arXiv preprint arXiv:2110.11034},
year = {2021}
}