Opacity for Linear Constraint Markov Chains

Béatrice Bérard 1 Olga Kouchnarenko 2 John Mullins 3 Mathieu Sassolas 4
1 MoVe - Modélisation et Vérification
LIP6 - Laboratoire d'Informatique de Paris 6
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : On a partially observed system, a secret ϕ is opaque if an observer cannot ascertain that its trace belongs to ϕ. We consider specifications given as Constraint Markov Chains (CMC), which are underspec-ified Markov chains where probabilities on edges are required to belong to some set. The nondeterminism is resolved by a scheduler, and opacity on this model is defined as a worst case measure over all implementations obtained by scheduling. This measures the information obtained by a passive observer when the system is controlled by the smartest sched-uler in coalition with the observer. When restricting to the subclass of Linear CMC, we compute (or approximate) this measure and prove that refinement of a specification can only improve opacity.
Type de document :
Rapport
[Research Report] LIP6 UMR 7606 UPMC Sorbonne Universités, France; Univ. de Franche-Comté; Ecole Polytechnique de Montréal; LACL, Université Paris-Est. 2016
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.sorbonne-universite.fr/hal-01384153
Contributeur : Béatrice Bérard <>
Soumis le : mercredi 19 octobre 2016 - 14:36:15
Dernière modification le : samedi 24 novembre 2018 - 01:37:47

Fichier

bkms-hal.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01384153, version 1

Citation

Béatrice Bérard, Olga Kouchnarenko, John Mullins, Mathieu Sassolas. Opacity for Linear Constraint Markov Chains. [Research Report] LIP6 UMR 7606 UPMC Sorbonne Universités, France; Univ. de Franche-Comté; Ecole Polytechnique de Montréal; LACL, Université Paris-Est. 2016. 〈hal-01384153〉

Partager

Métriques

Consultations de la notice

424

Téléchargements de fichiers

220