Software Verification of Hyperproperties Beyond k-Safety

Raven Beutner, Bernd Finkbeiner

Temporal hyperproperties are system properties that relate multiple execution traces. For (finite-state) hardware, temporal hyperproperties are supported by model checking algorithms, and tools for general temporal logics like HyperLTL exist. For (infinite-state) software, the analysis of temporal hyperproperties has, so far, been limited to k-safety properties, i.e., properties that stipulate the absence of a bad interaction between any k traces. In this paper, we present an automated method for the verification of ∀k∃l-safety properties in infinite-state systems. A ∀k∃l-safety property stipulates that for any k traces, there exist l traces such that the resulting k+l traces do not interact badly. This combination of universal and existential quantification allows us to express many properties beyond k-safety, including, for example, generalized non-interference or program refinement. Our method is based on a strategy-based instantiation of existential trace quantification combined with a program reduction, both in the context of a fixed predicate abstraction. Importantly, our framework allows for mutual dependence of strategy and reduction.

34th International Conference on Computer Aided Verification (CAV 2022) (CAV 2022).

CAV Distinguished Paper Award 2022.

(pdf) (bib)