Verifying Asynchronous Hyperproperties in Reactive Systems
Hyperproperties are system properties that relate multiple execution traces and commonly occur when specifying information-flow and security policies. Logics like HyperLTL can express temporal hyperproperties in reactive systems, i.e., hyperproperties that reason about the temporal behavior along infinite executions, by utilizing explicit quantification over execution traces of a system. An often unwanted side-effect of such logics is that they enforce a lock-step traversal on traces, i.e., all traces are evaluated \emph{synchronously}. This prohibits the logics from expressing properties that compare multiple traces in a non-lock-step alignment, such as Zdancewic and Myers’s \emph{observational determinism}, McLean’s \emph{non-inference}, or (stuttering) \emph{refinement}. We study the model-checking problem for \emph{asynchronous HyperLTL} (A-HLTL), an established temporal logic that can express hyperproperties where multiple traces are compared across timesteps. In addition to quantifying over system traces (as, e.g., in HyperLTL), A-HLTL features secondary quantification over trajectories (i.e., stutterings) of these traces. Consequently, A-HLTL allows for succinct specification for many widely used hyperproperties that cannot be captured in previous temporal logics. Model-checking A-HLTL requires finding suitable trajectories, which, thus far, was only possible for very restricted fragments and \emph{terminating} systems. In this paper, we propose a novel game-based approach for the verification of $\forall^\exists^$ A-HLTL formulas that, for the first time, supports infinite executions of \emph{reactive} systems. In our method, we consider the verification as a game played between a verifier and a refuter, who challenge each other by controlling parts of the underlying system and stuttering. A winning strategy for the verifier then corresponds to concrete witnesses for existentially quantified traces and asynchronous stutterings for existentially quantified trajectories. We identify fragments for which our game-based interpretation is complete and thus constitutes a decision procedure. We contribute a prototype implementation for finite-state systems based on parity games and report on encouraging experimental results.