Software Verification of Hyperproperties Beyond k-Safety

TL;DR

This paper introduces an automated verification method for complex hyperproperties in infinite-state software systems, extending beyond traditional k-safety properties to include more expressive properties like non-interference.

Contribution

It presents a novel approach for verifying $orall^korall^l$-safety properties in infinite-state systems, enabling analysis of properties beyond k-safety such as non-interference.

Findings

Supports verification of properties beyond k-safety

Uses strategy-based instantiation and program reduction

Applicable to infinite-state systems with predicate abstraction

Abstract

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 $\forall^k\exists^l$-safety properties in infinite-state systems. A $\forall^k\exists^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 enables 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. Notably, our framework allows for mutual dependence of strategy and reduction.