Fine-grained and coarse-grained reactive noninterference

Pejman Attar 1 Ilaria Castellani 1
1 INDES - Secure Diffuse Programming
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We study the security property of noninterference in a core synchronous reactive language that we call CRL. In the synchronous reactive paradigm, programs communicate by means of broadcast events, and their parallel execution is regulated by a notion of instant. We first show that CRL programs are indeed reactive, namely that they always converge to a state of termination or suspension ("end of instant") in a finite number of steps. We define two bisimulation equivalences on CRL programs, corresponding respectively to a fine-grained and to a coarse-grained observation of programs. We show that coarse-grained bisimilarity is more abstract than fine-grained bisimilarity, as it is insensitive to the order of generation of events and to repeated emissions of the same event during an instant. Based on these bisimulations, two properties of Reactive Noninterference (RNI) are introduced, formalising secure information flow. Both properties are time-insensitive and termination-insensitive. Again, coarse-grained RNI is more abstract than fine-grained RNI. Finally, a type system guaranteeing both security properties is presented. Thanks to a design choice of CRL, which offers two separate constructs for loops and iteration, and to refined typing rules, this type system allows for a precise treatment of termination leaks, which are an issue in parallel languages.
Type de document :
Communication dans un congrès
Trustworthy Global Computing 2013 - 8th International Symposium, Revised Selected Papers, Aug 2013, Buenos Aires, Argentina. Springer, Lecture Notes in Computer Science, 8358, pp.21, 2014, 〈http://dx.doi.org/10.1007/978-3-319-05119-2〉. 〈10.1007/978-3-319-05119-2_10〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00915241
Contributeur : Ilaria Castellani <>
Soumis le : vendredi 6 décembre 2013 - 18:25:10
Dernière modification le : jeudi 11 janvier 2018 - 16:42:52
Document(s) archivé(s) le : samedi 8 avril 2017 - 05:20:15

Fichier

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

Identifiants

Collections

Citation

Pejman Attar, Ilaria Castellani. Fine-grained and coarse-grained reactive noninterference. Trustworthy Global Computing 2013 - 8th International Symposium, Revised Selected Papers, Aug 2013, Buenos Aires, Argentina. Springer, Lecture Notes in Computer Science, 8358, pp.21, 2014, 〈http://dx.doi.org/10.1007/978-3-319-05119-2〉. 〈10.1007/978-3-319-05119-2_10〉. 〈hal-00915241〉

Partager

Métriques

Consultations de la notice

404

Téléchargements de fichiers

118