Formal Foundations for Translational Separation Logic Verifiers (extended version)

TL;DR

The paper addresses the challenge of soundly linking input programs written with rich separation-logic verification concepts to diverse verification back-ends through a unified intermediate IVL. It introduces CoreIVL, a core SL-based IVL whose state is modeled by IDF algebras and which supports dual nondeterminism (demonic and angelic) to capture back-end proof search and heuristics. The authors define both an operational semantics and an axiomatic semantics for CoreIVL, prove their equivalence, and instantiate CoreIVL with Viper (as ViperCore), proving soundness for two back-ends (symbolic execution and THSem VC generation) as well as soundness of a concurrent front-end translation based on an IDF-based CSL (ParImp). All formalizations and proofs are mechanized in Isabelle/HOL, demonstrating a practical, mechanized framework to reason about translational SL verifiers and enabling end-to-end correctness proofs from front-ends to back-ends. The work provides a flexible, reusable foundation for analyzing and extending translational verification pipelines across multiple back-ends and front-ends, with potential to accommodate further logics and verification algorithms.

Abstract

Program verification tools are often implemented as front-end translations of an input program into an intermediate verification language (IVL) such as Boogie, GIL, Viper, or Why3. The resulting IVL program is then verified using an existing back-end verifier. A soundness proof for such a translational verifier needs to relate the input program and verification logic to the semantics of the IVL, which in turn needs to be connected with the verification logic implemented in the back-end verifiers. Performing such proofs is challenging due to the large semantic gap between the input and output programs and logics, especially for complex verification logics such as separation logic. This paper presents a formal framework for reasoning about translational separation logic verifiers. At its center is a generic core IVL that captures the essence of different separation logics. We define its operational semantics and formally connect it to two different back-end verifiers, which use symbolic execution and verification condition generation, resp. Crucially, this semantics uses angelic non-determinism to enable the application of different proof search algorithms and heuristics in the back-end verifiers. An axiomatic semantics for the core IVL simplifies reasoning about the front-end translation by performing essential proof steps once and for all in the equivalence proof with the operational semantics rather than for each concrete front-end translation. We illustrate the usefulness of our formal framework by instantiating our core IVL with elements of Viper and connecting it to two Viper back-ends as well as a front-end for concurrent separation logic. All our technical results have been formalized in Isabelle/HOL, including the core IVL and its semantics, the semantics of two back-ends for a subset of Viper, and all proofs.

Figures (11)

• Figure 1: Overview of our framework and its application to Viper. The yellow boxes represent components of our framework (such as semantics and logics), while the arrows show the theorems that connect them. The dashed arrows and the unlabeled yellow boxes represent potential additional front-ends and back-ends that could be connected to ViperCore. CSL stands for concurrent separation logic, and VCG for verification condition generation. VCG has been formally connected to VCGSem by THSem.
• Figure 2: Syntax of statements in CoreIVL. $A$ is an assertion, $x$ a variable, $b$ a Boolean expression, $e$ an arbitrary expression. Assertions and expressions are represented semantically as sets of states and partial functions from states to values, respectively. $C'$ represents custom statements and is a parameter of the language.
• Figure 3: A simple parallel program (left), annotated with a method precondition, as well as pre- and postconditions for the parallel branches, and its encoding into CoreIVL (instantiated to model Viper), consisting of a main IVL method (middle) and two further methods (right) modeling the parallel branches (that is, the premises of CSL's parallel composition rule). We use the shorthands $P_l \triangleq {\texttt{\bfseries acc}}(p.v,\_) * {\texttt{\bfseries acc}}(q.v)$, $Q_l \triangleq {\texttt{\bfseries acc}}(p.v,\_) * {\texttt{\bfseries acc}}(q.v) * {\texttt{p.v}} = {\texttt{q.v}}$, $P_r \triangleq {\texttt{\bfseries acc}}(p.v,\_)$, and $Q_r \triangleq {\texttt{\bfseries acc}}(p.v,\_) * {\texttt{tmp}} = {\texttt{p.v}}$, where the IDF assertion ${\texttt{\bfseries acc}}(e,\_)$ expresses non-zero permission to $e$ (corresponding to the SL assertion $\exists p, v \ldotp {e}\overset{{p}}{\mapsto}{v}$).
• Figure 4: Selected simplified operational and axiomatic semantic rules.
• Figure 5: Selected CSL rules. In the rule \ref{['FrameKey']}, $\mathit{fv}(F)$ and $\mathit{mod}(C)$ denote the set of variables free in $F$ and the set of variables potentially modified by $C$, respectively.

Theorems & Definitions (13)

• Definition 1
• Theorem 2: Operational-to-Axiomatic Soundness.
• Lemma 1: Exhale-havoc-inhale
• Definition 3
• Definition 4
• Lemma 2
• Theorem 5: Completeness
• Theorem 6: Soundness of $\textsf{sexec}$
• Theorem 7: Soundness of VCGSem
• Theorem 8: Adequacy