Beteiligte:
Parthasarathy, Gaurav;
Müller, Peter;
Summers, Alexander J.
Erschienen:
Springer International Publishing, 2021
Erschienen in:
Computer Aided Verification (2021), Seite 704-727
Sprache:
Nicht zu entscheiden
DOI:
10.1007/978-3-030-81688-9_33
ISSN:
0302-9743;
1611-3349
Entstehung:
Anmerkungen:
Beschreibung:
<jats:title>Abstract</jats:title><jats:p>A program verifier produces reliable results only if both the <jats:italic>logic</jats:italic> used to justify the program’s correctness is sound, and the <jats:italic>implementation</jats:italic> of the program verifier is itself correct. Whereas it is common to formally prove soundness of the logic, the implementation of a verifier typically remains unverified. Bugs in verifier implementations may compromise the trustworthiness of successful verification results. Since program verifiers used in practice are complex, evolving software systems, it is generally not feasible to formally verify their implementation.</jats:p><jats:p>In this paper, we present an alternative approach: we <jats:italic>validate successful runs</jats:italic> of the widely-used Boogie verifier by producing a <jats:italic>certificate</jats:italic> which proves correctness of the obtained verification result. Boogie performs a complex series of program translations before ultimately generating a verification condition whose validity should imply the correctness of the input program. We show how to certify three of Boogie’s core transformation phases: the elimination of cyclic control flow paths, the (SSA-like) replacement of assignments by assumptions using fresh variables (passification), and the final generation of verification conditions. Similar translations are employed by other verifiers. Our implementation produces certificates in Isabelle, based on a novel formalisation of the Boogie language.</jats:p>