Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals

Many security-related properties—such as non-interference—cannot be captured by traditional trace-based specification formalisms such as LTL. The reason is that they relate the events of two (or more) traces of the system, and LTL can only reason on one execution at a time. A number of hyper-property extensions of LTL have been proposed in the past few years, and case studies showing their ability to express interesting properties have also been shown. However, there has been less attention to hyper-properties for quantitative (timed) systems as well as very little work on developing a practically useful tool. Instead existing work focused on using ad-hoc implementations. In this paper we present a probabilistic hyper-property logic HPSTL for stochastic hybrid and timed systems and we show how to integrate the logic into existing statistical model checking tools. To show the feasibility of our approach we integrate the technique into a prototype implementation inside Uppaal SMC and apply it to the analysis of three side-channel attack examples. To our knowledge this is the first full implementation of a hyper logic inside a fully-fledged modelling environment.