Automata and Fixpoints for Asynchronous Hyperproperties

TL;DR

This paper introduces novel automata and fixpoint calculus models for analyzing hyperproperties asynchronously, expanding the scope beyond traditional synchronous methods and addressing their high undecidability.

Contribution

It presents the first systematic study of asynchronous hyperproperty analysis through new automata and fixpoint calculus models that generalize existing frameworks.

Findings

Automata and calculus models have equivalent expressive power over fixed path assignments.

Decision problems for these models are highly undecidable, not even arithmetical.

Proposed approximations yield decidable fragments for practical analysis.

Abstract

Hyperproperties have received increasing attention in the last decade due to their importance e.g. for security analyses. Past approaches have focussed on synchronous analyses, i.e. techniques in which different paths are compared lockstepwise. In this paper, we systematically study asynchronous analyses for hyperproperties by introducing both a novel automata model (Alternating Asynchronous Parity Automata) and the temporal fixpoint calculus $\Hmu$, the first fixpoint calculus that can systematically express hyperproperties in an asynchronous manner and at the same time subsumes the existing logic HyperLTL. We show that the expressive power of both models coincides over fixed path assignments. The high expressive power of both models is evidenced by the fact that decision problems of interest are highly undecidable, i.e. not even arithmetical. As a remedy, we propose approximative analyses for both models that also induce natural decidable fragments.