Hyperproperties

Traditional specification languages for systems usually refer to single execution traces and are therefore insufficient in many security-critical applications. This is because attackers may use comparisons between several different system traces to infer hidden secrets. Hyperproperties address this problem: Instead of specifying permitted behavior on single traces, they do so for sets of traces. The importance of research on hyperproperty specification and verification methods has recently been demonstrated by high-profile attacks such as Spectre and Meltdown, which exploit systems that violate certain information-flow policies. Further details on these attacks and their relation to hyperproperties can be found in this blog post.

In this seminar, we will have a look at state-of-the-art research on hyperproperties. This ranges from research on logics that describe hyperproperties, over verification algorithms, which check whether a system satisfies a property, to practical applications such as (runtime) monitoring.

The seminar will start with a group phase where students will present basic concepts in informal presentations. Subsequently, students will give individual talks on a research paper and hand in a summary at the end of the semester.

Requirements

This seminar is open to Bachelor or Master students. There are no formal requirements to take this seminar. You should have an interest in logic and related topics (as discussed in lectures like “Verification,” “Semantics,” “Automata, Games and Verification,” or “Automated Reasoning,” although none of these lectures is a prerequisite). The seminar will take place in person.