Carolina Gerlach: Probabilistic Hyperproperties

 

Model checking is traditionally concerned with analyzing whether a certain model satisfies a specific trace property. A trace is a sequence of observable facts about the states visited along a system execution. A trace property, formally specified using temporal logics like LTL or CTL, can be viewed as a set of model traces, encoding requirements on the system executions.

However, many interesting requirements, such as information-flow security policies, cannot be expressed as trace properties. For example, the property of non-interference for a deterministic system requires that the values of secret input variables do not influence the observable values of public output variables. In order to check whether this property holds, we need to compare different program executions thar start in observationally equivalent initial configurations, i.e., with the same initial public variable values but possibly different secret inputs. Non-interference is satisfied if we can make the same observations along all executions with observationally equivalent initial configurations, i.e., generating the same public variable values. Hence, non-interference cannot be expressed as a set of traces and is therefore not a trace property. Instead, security policies like noninterference are hyperproperties, which are sets of sets of traces.

Since established temporal logics can only capture sets of traces, but not sets of sets of traces, several temporal logics have been extended to hyperlogics. Clarkson et al. generalized LTL and CTL* to HyperLTL and HyperCTL*, respectively, by adding explicit quantification over multiple traces. Even though CTL* already permits quantification over traces, it does not allow quantifying over several traces at the same time, which HyperCTL* now does.

Probabilistic Hyperlogics

HyperPCTL was the first temporal logic for probabilistic hyperproperties. HyperPCTL extends PCTL by quantification over states to express probabilistic relations between several computation trees. Like PCTL, HyperPCTL formulas are evaluated over Markov chains. They can express information-flow security policies like probabilistic noninterference, which stipulates that, for all possible values of the public variables, the probability of observing these values should be the same for all program executions with observationally equivalent initial states.

HyperPCTL was lifted to Markov decision processes (MDPs) by additionally adding quantification over schedulers that resolve nondeterministic choices probabilistically. Model checking HyperPCTL for discrete-time Markov chains is decidable. For MDPs, the model checking problem becomes in general undecidable, but restricting scheduler quantification to deterministic memoryless schedulers makes it decidable again.

Research

We are currently working on an asynchronous extension of HyperPCTL, where the traces in different quantified computation trees do not have to evolve in lockstep anymore. This extension allows to capture the asynchronous nature of concurrent programs more accurately. One area of possible future research is to consider probabilistic hyperproperties in the context of stochastic games.