Formally Validating Translational Program Verifiers
OPEN ACCESS
Loading...
Author / Producer
Date
2024
Publication Type
Doctoral Thesis
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
Automated program verifiers automatically check whether a software program conforms to a user-provided specification.
This includes checking whether the program will not crash and whether the program will compute the results specified by the user for every feasible program execution.
Such verifiers perform this automatic check by analysing the input program statically (i.e. without executing the program) using techniques based on foundations in formal program verification.
For successful verification results to be meaningful, it is crucial that automated program verifiers are sound: that is, whenever the verifier reports success, then the input program must indeed conform to the user-provided specification.
Unfortunately, there are no formal soundness guarantees for many verifier implementations used in practice, which are themselves complex software programs.
Thus, software bugs in these implementations can and do arise, which compromises the trustworthiness of successful verification results.
Translational program verifiers form one large class of automated program verifiers whose implementations typically do not come with formal soundness guarantees.
These verifiers apply a series of program-to-program translations before ultimately producing a set of logical formulas, whose validity is automatically discharged via external tools such as SMT solvers.
Such verifiers are sound only if the validity of the produced logical formulas implies that the input program conforms to its specification.
In this dissertation, we develop techniques with which one can establish this soundness requirement for translational program verifier implementations used in practice.
In particular, one need not implement a verifier from scratch to use our techniques: our techniques can be applied to existing implementations used in practice.
Given a formal semantics of the input program, our techniques use a formal per-run validation approach: for each run of the verifier implementation, we automatically generate a certificate, which formally proves the soundness requirement.
Our generated certificates are expressed in terms of a formal operational semantics of the input program.
Moreover, these certificates are expressed in an interactive theorem prover (Isabelle, in our case), and thus can be automatically checked in a trustworthy way.
We have applied our techniques to two existing verifier implementations used in practice: (1) the Boogie verifier implementation, which applies a series of complex Boogie-to-Boogie transformations before ultimately producing logical conditions, and (2) the Viper verifier implementation, which translates Viper programs to Boogie programs.
As a result of our work, both of these verifier implementations are able to automatically generate certificates.
Our techniques are designed in a general way such that they could be adapted to other translational program verifiers.
In particular, our technique for the Viper verifier is designed more generally for translations into intermediate verification languages such as Boogie, which form the core of translational program verifiers.
Permanent link
Publication status
published
External links
Editor
Contributors
Book title
Journal / series
Volume
Pages / Article No.
Publisher
ETH Zurich
Event
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
VERIFICATION (SOFTWARE ENGINEERING); Automated Verification; Deductive verification; Interactive theorem proving
Organisational unit
03653 - Müller, Peter / Müller, Peter
Notes
Funding
197065 - Formal Foundations of Translational Program Verifiers (SNF)