Information flow vs resource access in the asynchronous pi-calculus.
Citation:
Matthew Hennessy and James Riely., Information flow vs resource access in the asynchronous pi-calculus., ACM Transactions on Programming Languages and Systems, 24, 5, 2002, 556-591Download Item:
information.pdf (Published (author's copy) - Peer Reviewed) 263.3Kb
Abstract:
We propose an extension of the asynchronous ?-calculus in which a variety of security properties may be captured using types. These are an extension of the input/output types for the ?-calculus in which I/O capabilities are assigned specific security levels. The main innovation is a uniform typing system that, by varying slightly the allowed set of types, captures different notions of security.We first define a typing system that ensures that processes running at security level ? cannot access resources with a security level higher than ?. The notion of access control guaranteed by this system is formalized in terms of a Type Safety Theorem.We then show that, by restricting the allowed types, our system prohibits implicit information flow from high-level to low-level processes. We prove that low-level behavior can not be influenced by changes to high-level behavior. This is formalized as a noninterference theorem with respect to may testing.
Author's Homepage:
http://people.tcd.ie/mcbhenneDescription:
PUBLISHED
Author: HENNESSY, MATTHEW
Publisher:
ACMType of material:
Journal ArticleSeries/Report no:
ACM Transactions on Programming Languages and Systems;24;
5;
Availability:
Full text availableKeywords:
Computer science, ?-calculusLicences: