Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)

TL;DR

The paper tackles the challenge of establishing trust in translational program verifiers by proposing a formal front-end validation approach that, for each verifier run, automatically generates an Isabelle proof linking the input language semantics to the IVL translation. It uses forward simulation to relate Viper input programs to Boogie IVL programs, addressing semantic gaps, diverse translations, and non-local checks. The method is instantiated for the Viper-to-Boogie translation within the Carbon toolchain, with formal semantics in Isabelle and automatic proof generation that can be independently checked. This end-to-end approach enhances the reliability of practical verifiers by ensuring front-end soundness and enabling composition with back-end validation for strong overall guarantees.

Abstract

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.

Figures (1)

• Figure 1: The syntax of our formalised Viper subset (top, blue keywords) and corresponding Boogie subset (bottom, with subscript $b$, orange keywords) without top-level declarations. $\tau$ ($\tau_b$), $\mathit{bop}$, and $\mathit{uop}$ denote types, binary and unary operations, respectively.