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 :
Liste complète des métadonnées

Littérature citée [34 références]  Voir  Masquer  Télécharger
Contributeur : Ilaria Castellani <>
Soumis le : mercredi 17 octobre 2007 - 19:37:41
Dernière modification le : mercredi 18 décembre 2019 - 17:32:43
Archivage à long terme le : lundi 24 septembre 2012 - 13:37:56


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00180168, version 1


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



Consultations de la notice


Téléchargements de fichiers