Hyperproperties are a general framework to reason about system requirements that relate multiple program executions. Specific hyperproperties have been studied in almost all branches of computer science, including noninterference in information flow security, epistemic properties in the design of distributed and multi-agent systems, and robustness/sensitivity requirements in cyber-physical systems. Research on formal reasoning about hyperproperties has primarily focused on developing decision procedures and verification algorithms, while domain-specific results on individual hyperproperties are often not well-known between different communities. The main goal of the seminar is to bring together researchers from communities working on different aspects of reasoning about hyperproperties. Together, we will explore the commonalities and differences between each community approach and debate the gap between the currently available reasoning frameworks and the needs of specific application areas.

This Dagstuhl Seminar will bring together researchers from core formal methods (FM) and programming languages (PL) along with three application areas: (1) computer security, (2) distributed computing, and (3) cyber-physical systems (CPS). To guide this exchange, the seminar will focus on a selected list of timely topics (presented below) that could not only reshape research on reasoning about hyperproperties but also impact other domains working with hyperproperties.

• Identify hyperproperty-related problems from each area. During this seminar, we will collect and discuss hyperproperty-related verification problems from each area. Our goal will be two-fold: to get familiar with hyperproperties of interest to each community and to familiarize the participants with the vocabulary and models used in each domain.
• Identify possibilities for knowledge and techniques transfer across different domains. Different areas have found and implemented tailored solutions to verify the hyperproperties of interest in their domain. These technical advances may benefit other areas that are facing similar problems. Bringing together experts from different areas and encouraging them to discuss their problems within a shared framework (hyperproperty verification) will promote finding common ground between seemingly unrelated problems, which may facilitate the transfer of research results between areas.
• Compare existing formalisms for the specification and verification of hyperproperties. The study of logics for hyperproperties has been an active field of research, with many formalisms proposed in the past decade to capture different aspects of hyperproperty verification. There is, however, no clear idea of what formalisms are best suited for practical applications. Drawing on feedback from the application areas, we will examine the current state of hyperlogics and take initial steps towards consolidating the landscape.
• Identify current technical limits of tools and solvers. While there has been some effort in implementing tools to support different aspects of verifying hyperproperties, other communities sparingly use them. We would like to discuss two orthogonal problems: (i) how to build stable tools (e.g., model-checkers, runtime monitors, enforcers) that researchers from different areas can more easily adopt; (ii) how to improve the performance of general tools for hyperproperties by promoting advances in other solvers, like SMT solvers or first-order theorem provers.

During this Dagstuhl Seminar, we will gather the information collected in the context of each of these topics, to be included in a report aimed at guiding future research in hyperproperty verification.

Creative Commons BY 4.0

Borzoo Bonakdarpour, Bernd Finkbeiner, David A. Naumann, and Ana Oliveira da Costa