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.

翻译：许多重要的功能和安全性属性——包括非干涉性、确定性和广义非干涉性（GNI）——都是超属性，即涉及程序多次执行的属性。现有的分离逻辑允许推理特定类别的超属性，例如非干涉性等 $\forall\forall$-超属性以及非确定性等 $\exists\exists$-属性。然而，它们不支持量词交替，而量词交替是表达GNI等属性所必需的。目前唯一能推理此类属性的逻辑是超霍尔逻辑，但它不支持堆操作程序，因此不适用于常见的命令式程序。本文引入超分离逻辑（HSL），这是首个支持对操作堆的程序进行任意量词交替超属性模块化推理的程序逻辑。HSL通过一种新颖的超分离合取将标准分离合取提升至状态集合层面，从而泛化了超霍尔逻辑，并实现了针对超属性的广义框架规则。我们在Isabelle/HOL中证明了HSL的可靠性，并展示了其在处理现有分离逻辑所无法触及的超属性方面的表达能力。