Thibault Dardinier

Trayan Gospodinov, Peter Müller, Thibault Dardinier

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.

Hongyi Ling, Thibault Dardinier, Ellen Arlt et al.

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.