Learning Hyperproperties

Lennart Haas

Hyperproperties formalize an important class of specifications including information-flow policies and symmetry requirements that are not expressible as traditional trace properties. They generalize trace properties to sets of sets of computation traces. In this thesis, we study an automata-theoretic approach for hyperproperties. We introduce a canonical automata representation for regular k-safety hyperproperties; the class of specifications for which violating systems contain a bad-prefix of size at most k and their k-folds form a regular language. And complement this approach by framework for learning our automata representations from unknown hyperproperties. In general, such hyperproperties can be represented by different automata using the k-fold self-composition of the alphabet. However this construction imposes an order on the traces in a set. Thus the representations are not unique. We define a notion of automata that are resistant under reordering of trace components; they are denoted permutation-complete. We investigate the construction of permutation-complete automata from various representations, such as HyperLTL, nondeterministic safety automata, and deterministic bad-prefix automata. Our first construction is based on automata-transformations and our second one relies on a learning framework called L∗Hyper that extends the L∗-framework for regular languages. In addition to the learner, we provide an implementation of the teacher deciding membership and equivalence queries for specifications given in HyperLTL. We conclude our work by presenting new decidability results concerning the learnability of hyper- and trace properties from queries and counterexamples. These include the undecidability of member- ship queries for safety languages and k-safety hyperproperties and the undecidability of the problem whether a HyperLTL formula expresses a k-safety hyperproperty.

Bachelor Thesis.

(pdf)