Program 6th of July

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 information-flow 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 re-evaluate 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

Hyperproperties for diagnosability and fault detection

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 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.

Symbolic Bug Finding for Asynchronous Hyperproperties

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 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.

Bounded Model Checking for Asynchronous Hyperproperties

Tzu-Han 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 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.

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

A-HyperLTL: A Temporal Logic for Asynchronous Hyperproperties

Norine Coenen

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.

Temporal logics for Asynchronous Hyperproperties

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 (HyperLTLS) and Context HyperLTL (HyperLTLC). 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 HyperLTLS fragment, coincides with that of the strictly less expressive logic HyperLTL.

Automata and Fixpoints for Asynchronous Hyperproperties

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üller-Olm and Christoph Ohrem.

17:00 - 17:30 Break
17:30 - 18:30 Formalisms II

Deciding Asynchronous Hyperproperties for Recursive Programs

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.

Asynchronicity in temporal team semantics

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 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.

Hypernode Automata

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 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.

19:00 Workshop Dinner - Wieden Brau (Waaggasse 5, 1040 Wien)

Program 7th of July

09:30-10: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 real-world applications, drawing from my work in related domains such as cyber-physical 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

Deductive Controller Synthesis for 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 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).

Introducing Asynchronicity to Probabilistic Hyperproperties

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 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.