Two for the Price of One: Lifting Separation Logic Assertions

TL;DR

This paper introduces a semantic analysis of separation logic-based data abstraction using Reynolds's relational parametricity, providing a new way to verify client-side proofs that respect module abstraction.

Contribution

It presents a novel semantic framework with lifting theorems that connect standard and relational interpretations of separation logic assertions.

Findings

Lifting theorems establish sound and complete conditions for implication transfer.

Algorithm for identifying abstraction-respecting client proofs.

Ensures clients cannot distinguish between related module implementations.

Abstract

Recently, data abstraction has been studied in the context of separation logic, with noticeable practical successes: the developed logics have enabled clean proofs of tricky challenging programs, such as subject-observer patterns, and they have become the basis of efficient verification tools for Java (jStar), C (VeriFast) and Hoare Type Theory (Ynot). In this paper, we give a new semantic analysis of such logic-based approaches using Reynolds's relational parametricity. The core of the analysis is our lifting theorems, which give a sound and complete condition for when a true implication between assertions in the standard interpretation entails that the same implication holds in a relational interpretation. Using these theorems, we provide an algorithm for identifying abstraction-respecting client-side proofs; the proofs ensure that clients cannot distinguish two appropriately-related module implementations.