Location: WebEx
Meeting number: 120 580 7845
Password: kTq5pJMGg22
Techniques for Efficient Model Checking of Probabilistic Hyperproperties
Traditionally, the model checking community has focused on verification of trace properties to ensure the correctness of programs. Temporal logics such as LTL and CTL have been proposed for model checking trace properties. For checking trace properties in probabilistic settings, logics like PCTL and PCTL* have been proposed. However, it turns out that essential properties in information-flow security policies like non-interference, differential privacy, observational determinism, and causality are not trace properties. These are system-wide policies and stipulate properties of two or more execution traces. Such requirements are called hyperproperties. Temporal logics HyperLTL and HyperCTL* have been proposed for model checking hyperproperties. Analgously, HyperPCTL and HyperPCTL* have been introduced to reason about hyperproperties in probabilistic settings. Despite recent advances on verification of hyperproperties, we still lack efficient model checking algorithms for verifying probabilistic hyperproperties.
Our goal is to develop efficient model checking algorithms for probabilistic hyperproperties. We are studying different techniques for discrete-time Markov chains (DTMCs). We have designed and implemented methods based on constraint solving, probability mass function (PMF), and self composition. We compared the performance of these verification algorithms. The approach based on constraint solving generates parameterized nonlinear inequalities, whose satisfiability implies a counterexample. The PMF-based algorithm uses numerical approach to calculate the probability to reach target states mentioned in the HyperPCTL formula. Both techniques bypass self-composition of the original model, which incurs significant overhead. We have validated our approach through different case studies including probabilisitic scheduling attacks, the dining cryptographers protocol, and probabilistic conformance.
Committee: Gianfranco Ciardo (major professor), Borzoo Bonakdarpour (major professor), Samik Basu, Jack Lutz, and Farzad Sabzikar