3rd Workshop on Hyperproperties: Advances in Theory and Applications
23 July @ CAV 2024
Montreal, Canada
The study of hyperproperties has recently gained a great deal of attention in the formal methods, security, and cyber-physical systems communities. They have become a widely-used formalism for expressing system properties such as information-flow policies, symmetry in hardware design, robustness in cyber-physical systems, as well as properties of learning-enabled systems. The goal of this workshop is to foster the exchange of ideas on the topic of hyperproperties between researchers from these diverse communities and to present and discuss recent advances in formalisms and methods for specifying and analyzing hyperproperties. Topics of interest include, but are not limited to, developments on logical formalisms for specifying hyperproperties, algorithmic methodologies for the verification, synthesis, and runtime verification of hyperproperties, as well as applications related to the fields of cyber-physical systems, security and machine learning.
Invited Speakers
Fred Schneider
Cornell, USA
Fred B. Schneider has been on Cornell's faculty since 1978. He is
known for his research in trustworthy systems, spanning fault-tolerant
distributed systems, formal methods, and cybersecurity. He is author
of two formal methods textbooks: "Logical Approach to Discrete Math"
(co-authored with David Gries) and "On Concurrent Programming". And
along with Bowen Alpern he devised the now standard formal definition
of "liveness properties" along with a proof that safety and liveness
are a fundamental basis for all trace-properties; that work received
the 2018 Edsger W. Dijkstra Prize in Distributed Computing. Schneider
is a member of the US National Academy of Engineering and the American
Academy of Arts & Sciences; he is a foreign member of the Norges
Tekniske Vitenskapsakademi (Norwegian Academy of Technological
Sciences).
Hagit Attiya
Technion, Israel
Hagit Attiya is a professor at the department of Computer Science at the Technion,
Israel Institute of Technology, and holds the
Harry W. Labov and Charlotte Ullman Labov Academic Chair.
She is the editor-in-chief of Springer's journal Distributed Computing.
She won the Dijkstra award in Distributed Computing 2011 and is a fellow of the ACM.
She received all her academic degrees, in Computer Science, from the Hebrew University
of Jerusalem, and was a post-doctoral fellow at MIT.
Jana Hofmann
Azure Research, UK
Jana Hofmann is a researcher at Azure Research, Microsoft. She obtained her PhD in 2022 at CISPA/Saarland University, for which she received the university’s Dr.-Eduard-Martin Prize for best computer science thesis of the year. She develops logics, formal methods, and testing techniques for hyperproperties. In particular, she works on principled methods to detect, model, and prevent information leakage through microarchtectural side channels.
Xiang Yin
Shanghai Jiao Tong University, China
Xiang Yin received the B.Eng degree from Zhejiang University in 2012, the M.S. degree from the University of Michigan, Ann Arbor, in 2013, and the Ph.D degree from the University of Michigan, Ann Arbor, in 2017, all in electrical engineering. Since 2017, he has been with the Department of Automation, Shanghai Jiao Tong University, where he is an Associate Professor. His research interests include formal methods, discrete-event systems and cyber-physical systems. Dr. Yin is serving as the chair of the IEEE CSS Technical Committee on Discrete Event Systems, an Associate Editor for the Journal of Discrete Event Dynamic Systems: Theory & Applications, and a member of the IEEE CSS Conference Editorial Board. Dr. Yin received the IEEE Conference on Decision and Control (CDC) Best Student Paper Award Finalist in 2016.
Program
8:55 Kick-off
9:00 Session 1
09:00 - 09:50 Invited talk
Fred Schneider
Historical Context for Hyperproperties
This talk discusses the needs and context that led to the
initial formulation of a new class of characterizations for system
behaviors: hyperproperties. We also discuss the extent to which the
original goals for this abstraction are being realized.
09:50 - 10:10 Contributed talk
Tzu-Han Hsu, Ana Oliveira da Costa, Andrew Wintenberg, Borzoo Bonakdarpour and Ezio Bartocci
Gray-box Runtime Enforcement of Hyperproperties
10:10 - 10:30 Contributed talk
Arthur Correnson, Tobias Nießen, Bernd Finkbeiner and Georg Weissenbacher
Automated Hyperbug Finding
Most of the research in hyperproperties has focused on proving that a system satisfies a given hyperproperty. On the other hand, methods to automatically test hyperproperties in order to locate specification violations have thus far received much less attention. Further, traditional automated testing methods such as symbolic execution cannot immediately be applied to the analysis of hyperproperties. This presentation goes over the challenges of lifting existing bug finding techniques to the analysis of hyperproperties, and proposes a novel approach to automated hyperbug finding based on symbolic execution.
10:30 Coffee/Tea break
11:00 Session 2
11:00 - 11:50 Invited talk
Xiang Yin
A Unified Framework for Verification of Observational Properties for Partially-Observed Discrete-Event Systems using HyperLTL
In this talk, we discuss property verification problems in partially-observed discrete-event systems (DES). Particularly, we are interested in verifying observational properties that are related to the information-flow of the system. Observational properties considered here include diagnosability, predictability, detectability and opacity, which have drawn considerable attentions in the literature. However, in contrast to existing results, where different verification procedures are developed for different properties case-by-case, in this talk, we introduce a unified framework for verifying all these properties by reducing each of them as an instance of HyperLTL model checking. Our approach is based on the construction of a Kripke structure that effectively captures the issue of unobservability as well as the finite string semantics in partially- observed DES so that HyperLTL model checking techniques can be suitably applied. Then for each observational property considered, we explicitly provide the HyperLTL formula to be checked over the Kripke structure for the purpose of verification. Our approach is uniform in the sense that all different properties can be verified with the same model checking engine. Furthermore, our unified framework also brings new insights for classifying observational properties for partially-observed DES in terms of their verification complexity. Also, we will briefly discuss our recent work on path planning with HyperSTL.
11:50 - 12:10 Contributed talk
Julian Siber
Specifying and Verifying Counterfactual Explainability
12:10 Lunch
14:00 Session 3
14:00 - 14:50 Invited talk
Hagit Attiya
Preserving Hyperproperties when Using Concurrent Objects
Linearizability, a consistency condition for concurrent objects, is known to preserve trace properties. This suffices for modular usage of concurrent objects in applications, deriving their safety properties from the abstract object they implement. However, other desirable properties, like average complexity and information leakage, are not trace properties. These hyperproperties are not preserved by linearizable concurrent objects, especially when randomization is used. This talk will discuss formal ways to specify concurrent objects that preserve hyperproperties and their relation with verification methods. We will show that certain concurrent objects cannot satisfy such specifications, and describe ways to mitigate these limitations. This is a joint work with Constantin Enea and Jennifer Welch.
14:50 - 15:10 Contributed talk
Adwait Godbole and Sanjit A. Seshia
Hyperproperty-based Security Verification for Hardware RTL: Invariants and Abstractions
15:10 - 15:30 Contributed talk
Anagha Athavale, Ezio Bartocci, Maria Christakis, Matteo Maffei, Dejan Nickovic and Georg Weissenbacher
Verifying Global Two-Safety Properties in Neural Networks with Confidence
15:30 Coffee/Tea break
16:00 Session 4
16:00 - 16:50 Invited talk
Jana Hofmann
Testing for Microarchitectural Information Flow Security
Noninterference is a hyperproperty whose relational nature makes reasoning inherently complicated. For this reason, the practicality of information flow techniques has been questioned in the past. In this talk, I demonstrate that relational reasoning can indeed be practical – with the right tools and trade-offs. Specifically, I discuss our recent work on analyzing microarchitectural information leakage in black-box CPUs.
16:50 - 17:10 Contributed talk
Raven Beutner, Tzu-Han Hsu, Borzoo Bonakdarpour and Bernd Finkbeiner
Syntax-Guided Automated Program Repair For Hyperproperties
17:10 - 17:30 Contributed talk
Ludovico Fusco and Alessandro Aldini
Hyperproperties for Safe and Secure RFID Systems
17:45 End
Call for Presentations
The HYPER workshop aims to bring together researchers interested in the broad area of hyperproperties and working in the areas of formal methods and control, cybersecurity, and machine learning. HYPER 2024 is co-located with CAV 2024, and will take place in Montreal, Canada, on July 23, 2024. Topics of interest include, but are not limited to:
Specification formalisms for hyperproperties
Algorithms for verification, synthesis, and runtime verification for hyperproperties
Information-flow control
Privacy
Fairness
Causality
Robustness
Explainability
Presentation proposals shall be submitted in form of an extended abstract of up to three pages in LNCS format (not including references) via the easychair link https://easychair.org/my/conference?conf=hyper24. Submissions can overlap with previously published work and will be judged based on their relevance to the topic of the workshop. The review process will be single blind and the deadline for submission is May 16, 2024 AoE.
Selected submissions will be invited for a topical collection on Hyperproperties at Acta Informatica.
The registration for the workshop can be found at the CAV 2024 website https://i-cav.org/2024/registration. The early registration deadline is June 23, 2024.
