Asynchronous Hyperproperties: from Theory to Practice

The workshop highlighted the crucial role of these frameworks in the industrial detection of critical vulnerabilities, such as Spectre and Meltdown. Participants explored both the theoretical base and practical applications of diagnosability and fault detection, employing sophisticated formalisms like epistemic temporal logic, and expanded these discussions to include asynchronous system operations. Additional topics covered included advanced methods for symbolic bug finding, bounded model checking in asynchronous contexts, and the application of modal and temporal logics for a rigorous definition and analysis of security properties. The event also introduced new logical frameworks and formalisms intended to enhance the expressive power and practical utility of hyperproperties in analyzing complex systems like recursive programs and probabilistic models.

This comprehensive review not only revisited the historical challenges associated with hyperproperties but also charted future directions for their application in diverse and rapidly evolving technological landscapes. The workshop format emphasized interactivity, promoting open discussions and exchanges of ideas across different fields. This collaborative setting aimed to cultivate deeper insights and foster advancements in the field through interdisciplinary efforts. Notable keynote speakers included Boris Köpf, Musard Balliu, and Ashutosh Trivedi, whose expertise contributed significantly to the richness of the discussions.

Keynote speaker - Boris Köpf (Azure Research)
Topic: 20 Years of “20 Years of Covert Channel Modeling and Analysis”
Date: 6.07.2024
Time: 9:40
Abstract - 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.

Keynote speaker - Musard Balliu (KTH, Sweden)
Topic: Security Properties through the Lens of Modal Logic
Date: 6.07.2024
Time: 14:00
Abstract - 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.
Video of the talk

Keynote speaker - Ashutosh Trivedi (CU Boulder, USA)
Topic: Expanding Horizons: Hyperproperties in CPS, Fairness, and Legal Compliance Requirements
Date: 7.07.2024
Time: 9:30
Abstract - 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.
Video of the talk