The Community for Technology Leaders
Computer Security Foundations Workshop, IEEE (2002)
Cape Breton, Nova Scotia, Canada
June 24, 2002 to June 26, 2002
ISSN: 1063-6900
ISBN: 0-7695-1689-0
pp: 320
ABSTRACT
<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>
INDEX TERMS
null
CITATION
François Pottier, "A Simple View of Type-Secure Information Flow in the π-Calculus", Computer Security Foundations Workshop, IEEE, vol. 00, no. , pp. 320, 2002, doi:10.1109/CSFW.2002.1021826
97 ms
(Ver 3.3 (11022016))