A simple view of type-secure information flow in the π-calculus

One way of enforcing an information flow control policy is to use a static type system capable of guaranteeing a noninterference property. Noninterference requires that two processes with distinct "high"-level components, but common "low"-level structure, cannot be distinguished by "low"-level observers. We state this property in terms of a rather strict notion of process equivalence, namely weak barbed reduction congruence. Because noninterference is not a safety property, it is often regarded as more difficult to establish than a conventional type safety result. This paper aims to provide an elementary noninterference proof in the setting of the π-calculus. This is done by reducing the problem to subject reduction - a safety property - for a nonstandard, but fairly natural, extension of the π-calculus, baptized the <π>-calculus.