Computer Security Foundations Workshop, IEEE (2002)
Cape Breton, Nova Scotia, Canada
June 24, 2002 to June 26, 2002
François Pottier , INRIA
<p>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.</p> <p>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 roof 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.</p>
F. Pottier, "A Simple View of Type-Secure Information Flow in the π-Calculus," Computer Security Foundations Workshop, IEEE(CSFW), Cape Breton, Nova Scotia, Canada, 2002, pp. 320.