Sound State Encodings in Translational Separation Logic Verifiers (Extended Version)

Abstract

Automated program verifiers are often organized into a front-end, which encodes an input program into an intermediate verification language (IVL), and a back-end, which proves that the IVL program is correct. Soundness of such translational verifiers requires that the back-end verification is sound and that correctness of the IVL program implies correctness of the input program. Existing formalizations for translational verifiers based on separation logic target the former, but support the latter only under the strong assumption that there exists a separation logic for the input program with the same state model as the IVL. This assumption is unrealistic in practice, especially since the state model also defines the supported separation logic resources. We present the first formal framework for proving the soundness of translational separation logic verifiers with non-trivial state encodings. To be applicable to various front-ends and IVLs, our framework only assumes the existence of a homomorphic encoding relation between the front-end and IVL state models. At the core of our framework is a novel condition, backward satisfiability, which is crucial to guarantee the soundness of the front-end translation. We formalize our framework for front-end verifiers based on concurrent separation logic and separation logic IVLs, such as Raven, VeriFast, and Viper. We demonstrate its expressiveness by proving soundness for three common state encodings. Our framework and all proofs are formalized in Isabelle/HOL.

Figures (10)

• Figure 1: An example front-end translation.
• Figure 2: Decomposing the soundness proof via a front-end SL. The dashed arrow represents the goal and the three solid arrows represent the decomposition. Existing work does the decomposition, but assumes that the two SLs have the same state model, which is unrealistic in practice. Our work lifts this key restriction, and enables full soundness proofs for front-ends with different state models to their IVLs.
• Figure 3: An illustration of our setting (in black), the problem of spurious splittability (in red), and the backward satisfiability solution (in blue). The black dashed arrows represent the state encoding function $\left\llbracket\cdot\right\rrbracket_{\textsf{S}}$ from front-end states to IVL states, and the black dashed ellipse represents the image of $\left\llbracket\cdot\right\rrbracket_{\textsf{S}}$. The red arrows represent a possible spurious split of the IVL state $\left\llbracket\omega\right\rrbracket_{\textsf{S}}$ into $\Omega_A$ (that satisfies the translated assertion $\left\llbracket A\right\rrbracket_{\textsf{A}}$) and $\Omega_F$ (the frame), that have no front-end counterparts. The blue arrows show how the backward satisfiability of $A$ guarantees the existence of front-end states $\omega_A$ and $\omega_F$, such that $\omega_A$ satisfies $A$, $\left\llbracket\omega_A\right\rrbracket_{\textsf{S}}$ is smaller or equal to $\Omega_A$, and $\left\llbracket\omega_F\right\rrbracket_{\textsf{S}}$ is larger or equal to $\Omega_F$.
• Figure 4: Encoding counting permissions $k \cdot \epsilon$ as fractions $1 - \frac{1}{2^k}$ is unsound. The front-end program on the left permits the three inputs to be aliased, but the IVL program on the right does not.
• Figure 5: Encoding binary permissions using fractional permissions is generally unsound. The IVL program on the right allows reading x.f after the fork because of the use of fractional permissions), and thus is correct. In contrast, the front-end program uses binary permissions, and thus should not be verified.

Theorems & Definitions (9)

• Definition 1: IDF algebra
• Definition 2
• Definition 3: Backward satisfiability
• Lemma 1: Extending requirements to all front-end assertions
• Lemma 2: Translation of separating conjunctions
• Lemma 3: Soundness of the exhale-havoc-inhale translation pattern
• Theorem 4: Soundness
• Definition 5: Generalized backward satisfiability
• Theorem 6: Generalization