Satisfiability and Monitoring of Hyperproperties
Christopher Hahn
In this thesis, we revisit the satisfiability problem of hyperproperties from a practical point of view and study the runtime verification of hyperproperties. Hyperproperties, such as noninterference and observational determinism relate multiple execution traces with each other and are thus not expressible in standard temporal logics like LTL, CTL and CTL*. HyperLTL extends Linear-time Temporal Logic (LTL) with explicit trace quantification to express hyperproperties. We present the first practical satisfiability solver, called EAHyper, for hyperproperties expressed in the decidable fragment of HyperLTL. Applications of EAHyper include the automatic detection of specifications that are inconsistent or vacuously true, as well as the comparison of multiple formalizations of the same policy, such as different notions of observational determinism. Furthermore, we investigate the runtime verification problem of HyperLTL formulas. As hyperproperties relate multiple execution traces, it is necessary to store previously seen traces, and to relate new traces to the traces seen so far. If done naively, this causes the monitor to become slower and slower, before it inevitably runs out of memory. We present a technique that reduces the set of traces that new traces must be compared against to a minimal subset. We show that this leads to much more scalable monitoring with, in particular, significantly lower memory consumption. Additionally, we show the practical relevance of EAHyper in modern verification procedures. EAHyper can be used to avoid overhead during the monitoring process, by analyzing specifications given in HyperLTL.
Master Thesis.