State-oriented noninterference for CCS

Ilaria Castellani 1
1 MIMOSA - Migration and mobility : semantics and applications
CRISAM - Inria Sophia Antipolis - Méditerranée , Université de Provence - Aix-Marseille 1, MINES ParisTech - École nationale supérieure des mines de Paris
Abstract : We address the question of typing noninterference (NI) in Milner's Calculus of Communicating Systems (CCS), in such a way that Milner's translation of a standard parallel imperative language into CCS preserves both an existing NI property and the associated type system. Recently, Focardi, Rossi and Sabelfeld have shown that a variant of Milner's translation, restricted to the sequential fragment of the language, maps a time-sensitive NI property to that of Persistent Bisimulation-based Non Deducibility on Compositions (PBNDC) on CCS. However, since CCS was not equipped with a security type system, the question of whether the translation preserves types could not be addressed. We extend Focardi, Rossi and Sabelfeld's result by showing that a slightly different variant of Milner's translation preserves a time-insensitive NI property on the full parallel language, by mapping it again to PBNDC. As a by-product, we formalise a folklore result, namely that Milner's translation preserves a natural behavioural equivalence on programs. We present a type system ensuring the PBNDC-property on CCS, inspired from type systems for the pi-calculus. Unfortunately, this type system as it stands is too restrictive to grant the expected type preservation result. We sketch a solution to overcome this problem.
Type de document :
Rapport
[Research Report] RR-6322, INRIA. 2007, pp.58
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00180168
Contributeur : Ilaria Castellani <>
Soumis le : mercredi 17 octobre 2007 - 19:37:41
Dernière modification le : jeudi 18 janvier 2018 - 02:09:54
Document(s) archivé(s) le : lundi 24 septembre 2012 - 13:37:56

Fichier

RR-6322.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00180168, version 1

Citation

Ilaria Castellani. State-oriented noninterference for CCS. [Research Report] RR-6322, INRIA. 2007, pp.58. 〈inria-00180168〉

Partager

Métriques

Consultations de la notice

228

Téléchargements de fichiers

109