Temporal Stream Logic for Hyperproperties
Temporal logics are commonly used in verification and synthesis to formally specify the desired behavior of a system. While the most popular temporal logics, LTL and CTL-star, can express properties on systems with finite data, they cannot specify properties on systems with infinite data. This is because they discretize data and encode it using atomic propositions. Temporal Stream Logic, TSL, on the other hand, abstracts from concrete data by using predicates and functions instead of atomic propositions. Therefore, it can express properties on systems with infinite data. Recent years have shown that temporal logics sometimes do not suffice to specify the desired behavior of a system because many important information flow properties in software are hyperproperties. Hyperproperties specify relationships between multiple execution traces and are commonly specified using temporal hyperlogics as standard temporal logics like LTL or CTL-star cannot reason about several traces. Popular temporal hyperlogics are HyperLTL and HyperCTL-star, which extend LTL and CTL-star with explicit quantification over traces. As they are based on LTL and CTL-star, they cannot specify hyperproperties on systems with infinite data. Therefore, information flow properties in software with infinite data cannot be expressed using HyperLTL or HyperCTL-star. In this thesis, we introduce the hyperlogic HyperTSL which extends TSL with explicit quantification over traces. Since it is based on TSL, HyperTSL can express hyperproperties on software with infinite data. We identify a syntactical fragment of HyperTSL, HyperTSL-, and develop a sound bounded synthesis approach for the universal fragment of HyperTSL-. Furthermore, we present an application of HyperTSL in the field of software doping, where we use the hyperlogic to spot deliberate manipulation of software by the provider to perform against the best interest of the user.