Reasoning about Quality in Hyperproperties

TL;DR

This paper introduces a qualitative reasoning extension to HyperLTL for hyperproperties, enabling approximate model checking and handling large fragments, thus improving the analysis of system security properties.

Contribution

It extends HyperLTL with qualitative reasoning inspired by LTL, providing decidability results for approximate and large fragment model checking.

Findings

Decidability of approximate model checking for HyperLTL.

Model checking of large fragments is feasible.

Qualitative measures improve hyperproperty analysis.

Abstract

Hyperproperties allow one to specify properties of systems that inherently involve not single executions of the system, but several of them at once: observational determinism and non-inference are two examples of such properties used to study the security of systems. Logics like HyperLTL have been studied in the past to model check hyperproperties of systems. However, most of the time, requiring strict security properties is actually ineffective as systems do not meet such requirements. To overcome this issue, we introduce qualitative reasoning in HyperLTL, inspired by a similar work on LTL by Almagor, Boker and Kupferman where a formula has a value in the interval [0, 1], obtained by considering either a propositional quality (how much the specification is satisfied), or a temporal quality (when the specification is satisfied). We show decidability of the approximated model checking problem, as well as the model checking of large fragments.