Probabilistic Hyperproperties with Nondeterminism
This work addresses formal verification challenges for security and privacy in systems with probabilistic and nondeterministic behavior, representing an incremental extension of existing logic.
The authors tackled the problem of formalizing and checking probabilistic hyperproperties for models with nondeterministic actions, extending HyperPCTL to Markov decision processes to express quantitative security and privacy requirements. They showed that model checking is undecidable in general but becomes decidable with restrictions, and proposed an SMT-based encoding with evaluated performance.
We study the problem of formalizing and checking probabilistic hyperproperties for models that allow nondeterminism in actions. We extend the temporal logic \HyperPCTL, which has been previously introduced for discrete-time Markov chains, to enable the specification of hyperproperties also for Markov decision processes. We generalize HyperPCTL by allowing explicit and simultaneous quantification over schedulers and probabilistic computation trees and show that it can express important quantitative requirements in security and privacy. We show that HyperPCTL model checking over MDPs is in general undecidable for quantification over probabilistic schedulers with memory, but restricting the domain to memoryless non-probabilistic schedulers turns the model checking problem decidable. Subsequently, we propose an SMT-based encoding for model checking this language and evaluate its performance.