Hyperproperties

Doctoral Privatissimum

Trace properties, i.e., sets of execution traces, have long been used to specify the correctness of computer systems. There are, however, important properties that are impossible to describe by referring to individual execution traces. Information flow policies, which characterize the circumstances under which an external observer can distinguish two executions, are of this type. Other examples include symmetric access to a shared resource, and the correctness of encoders and decoders for error resistant codes. Because these properties are properties of sets of execution traces, rather than properties of individual traces, they are called hyperproperties.

In this doctoral privatissimum, we will survey and criticize different ways to specify and verify hyperproperties. Previous exposure to information flow control and/or automated verification is helpful but not a requirement. If you are interested, please send a quick message to Bernd Finkbeiner.