HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata

Cited literature [34 references]  Display  Hide  Download

Contributor : Ilaria Castellani Connect in order to contact the contributor
Submitted on : Wednesday, October 17, 2007 - 7:37:41 PM
Last modification on : Wednesday, November 17, 2021 - 12:30:15 PM
Long-term archiving on: : Monday, September 24, 2012 - 1:37:56 PM


Files produced by the author(s)


  • HAL Id : inria-00180168, version 1


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



Record views


Files downloads