  Hyperproperties have shown to be a powerful tool for expressing and reasoning
about information-flow security policies. In this paper, we investigate the
problem of statistical model checking (SMC) for hyperproperties. Unlike
exhaustive model checking, SMC works based on drawing samples from the system
at hand and evaluate the specification with statistical confidence. The main
benefit of applying SMC over exhaustive techniques is its efficiency and
scalability. To reason about probabilistic hyperproperties, we first propose
the temporal logic HyperPCLT* that extends PCTL* and HyperPCTL. We show that
HyperPCLT* can express important probabilistic information-flow security
policies that cannot be expressed with HyperPCTL. Then, we introduce SMC
algorithms for verifying HyperPCLT* formulas on discrete-time Markov chains,
based on sequential probability ratio tests (SPRT) with a new notion of
multi-dimensional indifference region. Our SMC algorithms can handle both
non-nested and nested probability operators for any desired significance level.
To show the effectiveness of our technique, we evaluate our SMC algorithms on
four case studies focused on information security: timing side-channel
vulnerability in encryption, probabilistic anonymity in dining cryptographers,
probabilistic noninterference of parallel programs, and the performance of a
randomized cache replacement policy that acts as a countermeasure against cache
flush attacks.
