Logics and Algorithms for a Unified Theory of Hyperproperties

Introduction

The central role of information technology in all aspects of our private and professional lives has led to a fundamental change in the type of program properties we care about. Up to now, the focus has been on functional correctness; in the future, requirements that reflect our societal values, like privacy, fairness, and explainability will be far more important.

Hyperproperties

These properties belong to the class of hyperproperties, which represent sets of sets of execution traces and can therefore specify the relationship between different computations of a reactive system. Previous work has focused on individual hyperproperties like noninterference or restricted classes such as k-hypersafety.

Project Goals

This project sets out to develop a unified theory for general hyperproperties. We will:

1. Develop a formal specification language.
2. Create effective algorithms for logical reasoning, verification, and program synthesis.

Methodology

The central idea is to use the type and alternation structure of the logical quantifiers, ranging from classic first-order and second-order quantification to quantifiers over rich data domains and quantitative operators for statistical analysis. This structure will serve as the fundamental basis that partitions the broad concept of hyperproperties into specific property classes. Each particular class will then be supported by algorithms that provide a uniform solution for all the properties within the class.

Impact

The project will bring the analysis of hyperproperties to the level of traditional notions of safety and reliability. It will also provide a rigorous foundation for the debate about standards for privacy, fairness, and explainability that future software-based systems will be measured against.