In this talk, we review our previous work on the design and verification of Fault, Detection, Identification (FDI) components. We show that requirements such as fault detection and diagnosability are hyperproperties that can be formalized in epistemic temporal logic, both in the synchronous and asynchronous settings. We review the standard approach to diagnosability based on self-composition, traditionally called twin plant, and verification of the existence of a critical pair, a pair of paths, one faulty and the other non-faulty, that are observationally equivalent. We generalize the problem adopting a comprehensive framework that encompasses fair transition systems, temporally extended fault models, delays between the occurrence of a fault and its detection, and rich operational contexts. We show that in presence of fairness the definition of diagnosability has several interesting variants, and discuss the relative strengths and the mutual relationships. We prove that the existence of critical pairs is not always sufficient to analyze diagnosability, and needs to be generalized to critical sets. We define new notions of critical pairs, called ribbon-shape, with special looping conditions to represent the critical sets. Based on these findings, we provide algorithms to prove the diagnosability under fairness.

Hyperproperties relate multiple executions of one or more systems, and can specify important security requirements that other formalisms cannot. In the context of software systems, multiple executions of the same (or different) programs can progress at different paces. Therefore, most hyperproperties that we wish to express for software systems are in fact asynchronous hyperproperties: they require to align the executions appropriately before comparing them. Asynchronicity adds to the difficulty of both verification and testing of hyperproperties. While approaches to the verification of asynchronous hyperproperties have already been proposed the refutation of asynchronous hyperproperties received far less attention. Methods exist for refuting hyperproperties of finite-state systems, but they are restricted to the analysis of synchronous hyperproperties. In this presentation, we do a tour of the challenges of applying known automated testing methods to asynchronous hyperproperties of infinite-state systems (i.e., software systems). In particular, we focus on automated testing of asynchronous hyperproperties using symbolic execution.

Many types of attacks on confidentiality stem from the nondeterministic nature of the environment that computer programs operate in. We focus on verification of confidentiality in nondeterministic environments by reasoning about asynchronous hyperproperties. We generalize the temporal logic A-HLTL to allow nested trajectory quantification, where a trajectory determines how different execution traces may advance and stutter. We propose a bounded model checking algorithm for A-HLTL based on QBF-solving for a fragment of A-HLTL and evaluate it by various case studies on concurrent programs, scheduling attacks, compiler optimization, speculative execution, and cache timing attacks. We also rigorously analyze the complexity of model checking A-HLTL.

The temporal logic A-HyperLTL is an extension of HyperLTL to express asynchronous hyperproperties. While HyperLTL has a synchronous semantics that advances the traces it relates with each other in lockstep, the asynchronous variant of HyperLTL introduces so-called trajectories that determine which traces advance and which traces stutter. This enables the analysis of systems whose traces can proceed at different speeds and that allow that different traces take stuttering steps independently. In this talk, we introduce the logic A-HyperLTL and study its model-checking problem. While the general problem is undecidable, we identify two decidable fragments and present corresponding model-checking algorithms that reduce our problem to that of synchronous HyperLTL. This talk presents joint work with Jan Baumeister, Borzoo Bonakdarpour, Bernd Finkbeiner, and César Sánchez which was first presented at CAV 2021.

Hyperproperties are a modern specification paradigm that extends trace properties to express properties of sets of traces. Temporal logics for hyperproperties studied in the literature, including HyperLTL, assume a synchronous semantics and enjoy a decidable model checking problem. In this paper, we introduce two asynchronous and orthogonal extensions of HyperLTL, namely Stuttering HyperLTL (HyperLTL_S) and Context HyperLTL (HyperLTL_C). Both of these extensions are useful, for instance, to formulate asynchronous variants of information-flow security properties. We show that for these logics, model checking is in general undecidable. On the positive side, for each of them, we identify a fragment with a decidable model checking that subsumes HyperLTL and that can express meaningful asynchronous requirements. Moreover, we provide the exact computational complexity of model checking for these two fragments which, for the HyperLTL_S fragment, coincides with that of the strictly less expressive logic HyperLTL.

We study asynchronous analyses for hyperproperties by introducing both a novel automata model (Alternating Asynchronous Parity Automata) and the temporal fixpoint calculus Hµ, the first fixpoint calculus that can systematically express hyperproperties in an asynchronous manner and at the same time subsumes the existing logic HyperLTL. We discuss how 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. This talk is based on joint work with Markus Müller-Olm and Christoph Ohrem.

We introduce a novel logic for asynchronous hyperproperties with a new mechanism to identify relevant positions on traces. While the new logic is more expressive than a related logic presented recently by Bozzelli et al., we obtain the same complexity of the model checking problem for finite state models. Beyond this, we study the model checking problem of our logic for pushdown models. We argue that the combination of asynchronicity and a non-regular model class presented in this talk constitutes the first suitable approach for hyperproperty model checking against recursive programs. The talk is based on the paper "Deciding Asynchronous Hyperproperties for Recursive Programs" presented at POPL 2024. This is joint work with Jens Gutsfeld and Markus Müller-Olm.

TeamLTL is a logical formalism introduced in 2018 for specifying hyperproperties. The distinctive feature of TeamLTL, that separates it from prior logics designed for hyperproperties (such as HyperLTL), is the adoption of team semantics. While HyperLTL, an similar logics, are obtained from LTL by extending their syntax with first-order quantifiers ranging over traces, team semantics of LTL is defined directly over sets of traces. Without extensions the asynchronous variant of TeamLTL coincides both syntactically and semantically with LTL. However, the power of logics with team semantics arise from extensions; since formulae are evaluated directly on sets of traces, fundamental building blocks of hyperproperties of interest can be added directly as atomic statements in the logic. In the team semantics literature, the most prominent of these atomic statements are the dependence atom dep(x,y) (stating that the values of the variable-tuple x functionally determine the values of y) and inclusion atom x ⊆ y (expressing the inclusion dependency that all the values occurring for x must also occur as a value for y). As an example, let o1, ..., on be public observables and assume that c reveals confidential information. The atom (o1,...on,c) ⊆ (o1,...on,¬c) expresses a form of non-inference by stating that an observer cannot infer the value of the confidential bit from the outputs. In this talk, I discuss recent developments in temporal team semantics, and focus on the developments related to forms of asynchronicity.

We introduce hypernode automata as a new specification formalism for hyperproperties of concurrent systems. They are finite automata with nodes labeled with hypernode logic formulas and transitions labeled with actions. A hypernode logic formula specifies relations between sequences of variable values in different system executions. Unlike HyperLTL, hypernode logic takes an asynchronous view on execution traces by constraining the values and the order of value changes of each variable without correlating the timing of the changes. Different execution traces are synchronized solely through the transitions of hypernode automata. Hypernode automata naturally combine asynchronicity at the node level with synchronicity at the transition level. We show that the model-checking problem for hypernode automata is decidable over action-labeled Kripke structures, whose actions induce transitions of the specification automaton. For this reason, hypernode automaton is a suitable formalism for specifying and verifying asynchronous hyperproperties, such as declassifying observational determinism in multi-threaded programs. This talk presents joint work with Ezio Bartocci, Thomas A. Henzinger, Dejan Nickovic and Marek Chalupa.

Probabilistic hyperproperties extend the concept of hyperproperties to probabilistic systems. In a nutshell, they specify quantitative relations between the probabilities of reaching different target sets of states from different initial sets of states. This class of behavioral properties is suitable for capturing important security, privacy, and system-level requirements. In this talk we describe a novel approach to solve the controller synthesis problem for Markov decision processes (MDPs) and probabilistic hyperproperties. The specification language we consider builds on top of the logic HyperPCTL and enhances it with structural constraints over the synthesized controllers. Our approach starts from a family of controllers represented symbolically and defined over the same copy of an MDP. We then introduce an abstraction refinement strategy that can relate multiple computation trees and that we employ to prune the search space deductively. The experimental evaluation demonstrates that the proposed approach outperforms HyperProb, a state-of-the-art SMT-based model checking tool for HyperPCTL. Moreover, our approach is the first one that is able to effectively combine probabilistic hyperproperties with additional intra-controller constraints (e.g. partial observability) as well as inter-controller constraints (e.g. agreements on a common action).

We propose a new asynchronous hyperlogic called AHyperPCTL, which extends HyperPCTL by explicit quantification over stutter-schedulers. Stutter-schedulers are associated with a specific computation tree variable and determine when the traces in the corresponding computation tree should stutter. Stuttering decisions can be probabilistic and may depend on the current state, the chosen action and the history of the trace. We show that AHyperPCTL can express interesting information-flow security policies and subsequently present a model-checking algorithm for a decidable fragment of AHyperPCTL. To our knowledge, this is the first asynchronous extension of a probabilistic branching-time hyperlogic.