Metamorphic Hyperproperty Testing

Hyperproperties are quickly becoming a very popular way to define correctness requirements for computing systems, due to their expressive power. They differ from classical trace properties since they are represented by sets of sets of executions instead of sets of executions. This allows, for instance, to capture information flow security policies, which cannot be expressed as trace properties, namely as predicates over single executions. Unfortunately, to assess the correctness of a program with respect to a given hyperproperty is a very complex and challenging task. In this respect, actual approaches based on static analysis are very often too imprecise or unfeasible to be used in practice. Even in the context of testing, actually there are no approaches that target hyperproperties. Such lack of tools/methodologies to practically check hyperproperties poses serious limitations to the development of correct software.The goal of the project is to fill this gap: we aim at developing a systematic approach for testing hyperproperties, dubbed metamorphic hypertesting. In particular, the contribution of the work will be both foundational and practical. On the theoretical side, we plan to define a framework for automatically synthesizing (metamorphic) tests for hyperproperties. On the practical side, we plan to implement the proposed framework into a prototype tool for a particular hyperproperty (e.g., for security), in order to assess its effectiveness.