Hyper Separation Logic (extended version)

TL;DR

This paper introduces Hyper Separation Logic (HSL), a novel program logic that enables modular reasoning about complex hyperproperties involving multiple program executions and heap manipulation.

Contribution

HSL is the first logic supporting quantifier alternation over hyperproperties for heap-manipulating programs, extending Hyper Hoare Logic with a new hyper separating conjunction.

Findings

HSL is proven sound in Isabelle/HOL.

HSL can express hyperproperties beyond existing separation logics.

HSL generalizes Hyper Hoare Logic with a novel hyper separating conjunction.

Abstract

Many important functional and security properties--including non-interference, determinism, and generalized non-interference (GNI)--are hyperproperties, i.e., properties relating multiple executions of a program. Existing separation logics allow one to reason about specific classes of hyperproperties, e.g., $\forall\forall$-hyperproperties such as non-interference and $\exists\exists$-properties such as non-determinism. However, they do not support quantifier alternation, which is for instance needed to express GNI. The only existing logic that can reason about such properties is Hyper Hoare Logic, but it does not support heap-manipulating programs and, thus, is not applicable to common imperative programs. This paper introduces Hyper Separation Logic (HSL), the first program logic that supports modular reasoning about hyperproperties with arbitrary quantifier alternation over programs that manipulate the heap. HSL generalizes Hyper Hoare Logic with a novel hyper separating conjunction that lifts the standard separating conjunction to sets of states, enabling a generalized frame rule for hyperproperties. We prove HSL sound in Isabelle/HOL and demonstrate its expressiveness for hyperproperties that lie beyond the reach of existing separation logics.