Béatrice Bérard

Béatrice Bérard, Olga Kouchnarenko, John Mullins et al.

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.

Béatrice Bérard, John Mullins

Information flow properties express the capability for an agent to infer information about secret behaviours of a partially observable system. In a language-theoretic setting, where the system behaviour is described by a language, we define the class of rational information flow properties (RIFP), where observers are modeled by finite transducers, acting on languages in a given family $\mathcal{L}$. This leads to a general decidability criterion for the verification problem of RIFPs on $\mathcal{L}$, implying PSPACE-completeness for this problem on regular languages. We show that most trace-based information flow properties studied up to now are RIFPs, including those related to selective declassification and conditional anonymity. As a consequence, we retrieve several existing decidability results that were obtained by ad-hoc proofs.

Béatrice Bérard, Krishnendu Chatterjee, Nathalie Sznajder

Opacity is a generic security property, that has been defined on (non probabilistic) transition systems and later on Markov chains with labels. For a secret predicate, given as a subset of runs, and a function describing the view of an external observer, the value of interest for opacity is a measure of the set of runs disclosing the secret. We extend this definition to the richer framework of Markov decision processes, where non deterministic choice is combined with probabilistic transitions, and we study related decidability problems with partial or complete observation hypotheses for the schedulers. We prove that all questions are decidable with complete observation and $ω$-regular secrets. With partial observation, we prove that all quantitative questions are undecidable but the question whether a system is almost surely non opaque becomes decidable for a restricted class of $ω$-regular secrets, as well as for all $ω$-regular secrets under finite-memory schedulers.