Noninterference for Concurrent Programs and Thread Systems

Gérard Boudol 1 Ilaria Castellani
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 propose a type system to ensure the property of noninterference in a system of concurrent programs, described in a standard imperative language enriched with parallelism. Our proposal is in the line of some recent work by Irvine, Volpano and Smith. Our type system seems more natural and less restrictive than that originally presented by these authors for the concurrent case. Moreover, we show how to extend the language in order to formalise scheduling policies for systems of sequential threads. The type system is extended to the new constructs, and we show that noninterferenc- e still holds, while remaining in a nonprobabilistic setting.
Document type :
Reports
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00072334
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 8:25:30 PM
Last modification on : Wednesday, December 18, 2019 - 5:20:31 PM
Long-term archiving on: Sunday, April 4, 2010 - 11:04:12 PM

Identifiers

  • HAL Id : inria-00072334, version 1

Citation

Gérard Boudol, Ilaria Castellani. Noninterference for Concurrent Programs and Thread Systems. RR-4254, INRIA. 2001. ⟨inria-00072334⟩

Share

Metrics

Record views

193

Files downloads

442