Home  Registration  Program  Venue 
09:30  09:40  Opening 
09:40  10:40  20 Years of "20 Years of Covert Channel Modeling and Analysis" Boris Köpf 
Research on hyperproperties, and in particular on informationflow properties, has had a long and active history. However, around the year 2000 the community critically noticed that their results have not had the desired impact in practice. Several authors tried to identify reasons for this lack of success, among them Jon Millen in his remarkable paper "20 Years of Covert Channel Modeling and Analysis". Now, another 20 years later, we will reevaluate this situation: I will first give an example of a successful industrial application of hyperproperties for the automatic detection of microarchitectural vulnerabilities such as Spectre and Meltdown. I will then use this example to revisit the blockers identified 20 years ago and illustrate how they can be avoided now and in the future. 

10:40  11:00  Coffee Break 
11:00  12:30  Applications 
Marco Bozzano, Alessandro Cimatti and Stefano Tonetta 
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 selfcomposition, traditionally called twin plant, and verification of the existence of a critical pair, a pair of paths, one faulty and the other nonfaulty, 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 ribbonshape, with special looping conditions to represent the critical sets. Based on these findings, we provide algorithms to prove the diagnosability under fairness. 
Arthur Correnson, Tobias Nießen, Bernd Finkbeiner and Georg Weissenbacher 
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 finitestate 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 infinitestate systems (i.e., software systems). In particular, we focus on automated testing of asynchronous hyperproperties using symbolic execution. 
TzuHan Hsu, Borzoo Bonakdarpour, Bernd Finkbeiner and César Sánchez 
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 AHLTL 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 AHLTL based on QBFsolving for a fragment of AHLTL 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 AHLTL. 
12:30  14:00  Lunch Break 
14:00  15:00  Security Properties through the Lens of Modal Logic  Musard Balliu 
We introduce a framework for reasoning about the security of computer systems using modal logic. This framework is sufficiently expressive to capture a variety of known security properties, while also being intuitive and independent of syntactic details and enforcement mechanisms. We show how to use our formalism to represent various progress and termination(in)sensitive variants of confidentiality, integrity, robust declassification and transparent endorsement. In the second part of the talk, we focus on a specific modal logic, epistemic temporal logic, and show how to verify a range of properties by means of epistemic model checking and SMT solving. 

15:00  15:30  Coffee Break 
15:30  17:00  Formalisms I 
Norine Coenen 
The temporal logic AHyperLTL 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 socalled 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 AHyperLTL and study its modelchecking problem. While the general problem is undecidable, we identify two decidable fragments and present corresponding modelchecking 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. 
César Sánchez 
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 informationflow 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. 
Jens Oliver Gutsfeld 
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üllerOlm and Christoph Ohrem. 
17:00  17:30  Break 
17:30  18:30  Formalisms II 
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 nonregular 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üllerOlm. 
Jonni Virtema 
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 firstorder 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 variabletuple 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 noninference 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. 
Ana Oliveira da Costa 
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 modelchecking problem for hypernode automata is decidable over actionlabeled 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 multithreaded programs. This talk presents joint work with Ezio Bartocci, Thomas A. Henzinger, Dejan Nickovic and Marek Chalupa. 
19:00  Workshop Dinner  Wieden Brau (Waaggasse 5, 1040 Wien) 
09:3010:30  Expanding Horizons: Hyperproperties in CPS, Fairness, and Legal Compliance Requirements Ashutosh Trivedi 
In recent years, the study of hyperproperties has provided profound insights into complex system behaviors, yet many practical fields remain unexplored territories for these concepts. This talk aims to highlight the connection between hyperproperty research and realworld applications, drawing from my work in related domains such as cyberphysical systems (CPS), software fairness, legal compliance, and metamorphic testing. I will illustrate how concepts developed for hyperproperties can be effectively applied to ensure system confidentiality, equitable outcomes, regulatory adherence, and robust software testing. By exploring these practical settings, I hope to invite hyperproperty researchers to venture into new areas, offering fresh challenges and groundbreaking possibilities for the application of their innovative research. Join me as we discuss these diverse fields, uncovering the potential for hyperproperties to revolutionize approaches and solutions across various disciplines. 

10:30  11:00  Coffee Break 
11:00  12:00  Probabilistic Hyperproperties 
Roman Andriushchenko, Ezio Bartocci, Milan Ceska, Francesco Pontiggia and Sarah Sallinger 
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 systemlevel 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 stateoftheart SMTbased model checking tool for HyperPCTL. Moreover, our approach is the first one that is able to effectively combine probabilistic hyperproperties with additional intracontroller constraints (e.g. partial observability) as well as intercontroller constraints (e.g. agreements on a common action). 
Carolina Gerlach, Oyendrila Dobe, Erika Abraham, Ezio Bartocci and Borzoo Bonakdarpour 
We propose a new asynchronous hyperlogic called AHyperPCTL, which extends HyperPCTL by explicit quantification over stutterschedulers. Stutterschedulers 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 informationflow security policies and subsequently present a modelchecking algorithm for a decidable fragment of AHyperPCTL. To our knowledge, this is the first asynchronous extension of a probabilistic branchingtime hyperlogic. 