Dobe, O., Ábrahám, E., Bartocci, E., & Bonakdarpour, B. (2022). Model checking hyperproperties for Markov decision processes. Information and Computation, 289(Part B), Article 104978. https://doi.org/10.1016/j.ic.2022.104978
E191-01 - Forschungsbereich Cyber-Physical Systems
Information and Computation
ACADEMIC PRESS INC ELSEVIER SCIENCE
Hyperproperties; Information leakage; Markov models; Model checking; Policy synthesis
We study the problem of formalizing and checking probabilistic hyperproperties for Markov decision processes (MDPs). We introduce the temporal logic HyperPCTL that allows explicit and simultaneous quantification over schedulers as well as probabilistic computation trees. We show that the logic can express important quantitative requirements in security and privacy such as probabilistic noninterference, differential privacy, timing side-channel countermeasures, and probabilistic conformance testing. We show that HyperPCTL model checking over MDPs is in general undecidable, but restricting the domain of scheduler quantification to memoryless non-probabilistic schedulers turns the model checking problem decidable. Subsequently, we propose an SMT-based encoding for model checking this language. Finally, we demonstrate the applicability of our method by providing experimental results for verification, and we show how it can be used to solve even certain synthesis problems.
Computer Engineering and Software-Intensive Systems: 100%