Probabilistic Opacity in Refinement-Based Modeling
This work addresses security analysis for probabilistic systems, providing a formal method to assess and guarantee opacity, but it is incremental as it builds on existing refinement-based modeling.
The paper tackles the problem of measuring information leakage in probabilistic systems under partial observation, specifically computing the worst-case disclosure of a secret property across all implementations of an underspecified Markov chain, and proves that refinement improves opacity.
Given a probabilistic transition system (PTS) $\cal A$ partially observed by an attacker, and an $ω$-regular predicate $\varphi$over the traces of $\cal A$, measuring the disclosure of the secret $\varphi$ in $\cal A$ means computing the probability that an attacker who observes a run of $\cal A$ can ascertain that its trace belongs to $\varphi$. In the context of refinement, we consider specifications given as Interval-valued Discrete Time Markov Chains (IDTMCs), which are underspecified Markov chains where probabilities on edges are only required to belong to intervals. Scheduling an IDTMC $\cal S$ produces a concrete implementation as a PTS and we define the worst case disclosure of secret $\varphi$ in ${\cal S}$ as the maximal disclosure of $\varphi$ over all PTSs thus produced. We compute this value for a subclass of IDTMCs and we prove that refinement can only improve the opacity of implementations.