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 noninterference still holds, while remaining in a nonprobabilistic setting.

[PostScript, .ps.gz]