(2022) Software Verification of Hyperproperties Beyond k-Safety.
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 set of up to $k$ traces. In this paper, we present the first method to verify $\forall^k\exists^l$ HyperLTL properties in infinite-state systems. A $\forall^k\exists^l$-property stipulates that for any $k$ traces there \emph{exist} $l$ traces such that the resulting $k+l$ traces do not interact badly. The combination of universal and existential quantification is key to express many properties beyond $k$-safety including, for example, generalized non-interference or program refinement. Our method is based on a strategic instantiation of the existential quantification combined with a program reduction; both in the context of a fixed predicate abstraction. In our framework the strategy and reduction \emph{collaborate}, giving a very general proof system.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Bernd Finkbeiner (Reactive Systems Group, RSG) |
| Conference: | CAV Computer Aided Verification |
| Depositing User: | Raven Beutner |
| Date Deposited: | 01 Jun 2022 08:22 |
| Last Modified: | 01 Jun 2022 08:22 |
| Primary Research Area: | NRA1: Trustworthy Information Processing |
| URI: | https://publications.cispa.saarland/id/eprint/3706 |
Actions
Actions (login required)
 |
View Item |