Logics for Hyperproperties (Part 1)

8^th December 2020, 11:00
Martin Zimmermann
University of Liverpool

Abstract

Hyperproperties, as introduced by Clarkson and Schneider, generalize trace properties, which are sets of traces, to sets of sets of traces. The most prominent application of hyperproperties is information flow security: information flow policies characterize the secrecy and integrity of a system by comparing two or more execution traces, for example by comparing the observations made by an external observer on execution traces that result from different values of a secret variable. HyperLTL, the extension of LTL with trace quantifiers, has recently been introduced to specify hyperproperties. We survey four foundational aspects of HyperLTL: the expressiveness of HyperLTL, the satisfiability problem, the model-checking problem, and equivalent first-order logics for hyperproperties.