Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)
CoRR(2024)
摘要
Automated program verifiers are typically implemented using an intermediate
verification language (IVL), such as Boogie or Why3. A verifier front-end
translates the input program and specification into an IVL program, while the
back-end generates proof obligations for the IVL program and employs an SMT
solver to discharge them. Soundness of such verifiers therefore requires that
the front-end translation faithfully captures the semantics of the input
program and specification in the IVL program, and that the back-end reports
success only if the IVL program is actually correct. For a verification tool to
be trustworthy, these soundness conditions must be satisfied by its actual
implementation, not just the program logic it uses.
In this paper, we present a novel validation methodology that, given a formal
semantics for the input language and IVL, provides formal soundness guarantees
for front-end implementations. For each run of the verifier, we automatically
generate a proof in Isabelle showing that the correctness of the produced IVL
program implies the correctness of the input program. This proof can be checked
independently from the verifier in Isabelle and can be combined with existing
work on validating back-ends to obtain an end-to-end soundness result. Our
methodology based on forward simulation employs several modularisation
strategies to handle the large semantic gap between the input language and the
IVL, as well as the intricacies of practical, optimised translations. We
present our methodology for the widely-used Viper and Boogie languages. Our
evaluation shows that it is effective in validating the translations performed
by the existing Viper implementation.
更多查看译文
关键词
Formal Semantics,Intermediate Verification Languages,Proof Certification,Software Verification
AI 理解论文
溯源树
样例
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要