Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper introduces Hyper Separation Logic (HSL), a novel program logic enabling modular reasoning about hyperproperties with arbitrary quantifier alternation for heap-manipulating programs. HSL extends Hyper Hoare Logic by introducing a hyper separating conjunction that lifts the standard separating conjunction to sets of states. The soundness of HSL is proven in Isabelle/HOL, and its expressiveness is demonstrated for hyperproperties beyond the scope of existing separation logics.
Finally, a separation logic handles heap-manipulating programs while reasoning about hyperproperties with arbitrary quantifier alternation, like generalized non-interference.
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.