Verifying Observational Determinism

Abstract : This paper proposes an approach to verify information flow security of concurrent programs. It discusses a hyperproperty called observational determinism which aims to ensure secure information flow in concurrent programs, and proves how this hyperproperty can be verified by stutter equivalence checking. More precisely, it defines observational determinism in terms of stutter equivalence of all traces having the same low initial value and shows how stutter trace equivalence can be verified by computing a divergence stutter bisimulation quotient. The approach is illustrated by verifying a small example.
Type de document :
Communication dans un congrès
Hannes Federrath; Dieter Gollmann. 30th IFIP International Information Security Conference (SEC), May 2015, Hamburg, Germany. IFIP Advances in Information and Communication Technology, AICT-455, pp.82-93, 2015, ICT Systems Security and Privacy Protection. 〈10.1007/978-3-319-18467-8_6〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01345097
Contributeur : Hal Ifip <>
Soumis le : mercredi 13 juillet 2016 - 10:52:57
Dernière modification le : mercredi 13 juillet 2016 - 11:18:42

Fichier

337885_1_En_6_Chapter.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Jaber Karimpour, Ayaz Isazadeh, Ali Noroozi. Verifying Observational Determinism. Hannes Federrath; Dieter Gollmann. 30th IFIP International Information Security Conference (SEC), May 2015, Hamburg, Germany. IFIP Advances in Information and Communication Technology, AICT-455, pp.82-93, 2015, ICT Systems Security and Privacy Protection. 〈10.1007/978-3-319-18467-8_6〉. 〈hal-01345097〉

Partager

Métriques

Consultations de la notice

39

Téléchargements de fichiers

7