Hennessy, Matthew and Riely, James (2002) Information flow vs. resource access in the asynchronous pi-calculus. ACM Transactions on Programming Languages and Systems, 24 (5). pp. 566-591. ISSN 0164-0925
![]()
|
Postscript
Download (402kB) | Preview |
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.
Item Type: | Article |
---|---|
Additional Information: | Publisher's version available at official url |
Keywords: | Distributed process language, I/O subtyping, information flow, may testing, noninterference, pi-calculus, security, security types |
Schools and Departments: | School of Engineering and Informatics > Informatics |
Subjects: | Q Science > QA Mathematics > QA0075 Electronic computers. Computer science |
Depositing User: | Chris Keene |
Date Deposited: | 27 Feb 2008 |
Last Modified: | 07 Jun 2012 08:49 |
URI: | http://srodev.sussex.ac.uk/id/eprint/1383 |
Google Scholar: | 93 Citations |
View download statistics for this item
📧 Request an update