A Typed Process Calculus for Fine-Grained Resource Access Control in Distributed Computation
We propose the πD-calculus, a process calculus that can flexibly model fine-grained control of resource access in distributed computation, with a type system that statically prevents access violations. Access control of resources is important in distributed computation, where resources themselves or their contents may be transmitted from one domain to another and thereby vital resources may be exposed to unauthorized processes. In πD, a notion of hierarchical domains is introduced as an abstraction of protection domains, and considered as the unit of access control. Domains are treated as first-class values and can be created dynamically. In addition, the hierarchal structure of domains can be extended dynamically as well. These features are the source of the expressiveness of πD. This paper presents the syntax, the operational semantics, and the type system of πD, with examples to demonstrate its expressiveness.
KeywordsAccess Control Type System Mobile Agent Operational Semantic Typing Rule
Unable to display preview. Download preview PDF.
- 1.M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. In Proceedings of the Fourth ACM Conference on Computer and Communications Security. ACM Press, 1997.Google Scholar
- 2.M. Bugliesi and G. Castagna. Secure safe ambients. In POPL’01. ACM Press, 2001.Google Scholar
- 3.L. Cardelli and A. D. Gordon. Mobile ambients. In FoSSaCS’98. Springer-Verlag, 1998.Google Scholar
- 4.L. Cardelli and A. D. Gordon. Secrecy and group creation. In CONCUR’2000. Springer-Verlag, 2000.Google Scholar
- 5.R. De Nicola, G. Ferrari, and R. Pugliese. Klaim: a kernel language for agents interaction and mobility. IEEE Trans. on Software Engineering, 24(5), 1998.Google Scholar
- 6.M. Dezani-Ciancaglini and I. Salvo. Security types for mobile safe ambients. In ASIAN’00, 2000.Google Scholar
- 7.C. Fournet, G. Gonthier, J. J. Levy, L. Maranget, and D. Remy. A calculusof mobile agents. In CONCUR’96. Springer-Verlag, 1996.Google Scholar
- 8.J. Gosling, B. Joy, and G. Steele. The Java language specification. Addison-Wesley, 1996.Google Scholar
- 9.N. Heintze and J. G. Riecke. The SLam calculus: Programming with secrecy and integrity. In POPL’98. ACM Press, 1998.Google Scholar
- 10.M. Hennessy and J. Riely. Resource access control in systems of mobile agents. In HLCL’98. Elsevier, 1998.Google Scholar
- 11.M. Hennessy and J. Rily. Information flow vs. resource access in the asynchronous pi-calculus(extended abstract). In ICALP’00, January 2000.Google Scholar
- 12.D. Hoshina, E. Sumii, and A. Yonezawa. A typed process calculus for fine-grained resource access control in distributed computation (full version), 2001. Available from http://www.yl.is.s.u-tokyo.ac.jp/~hoshina/papers/tacs01full.ps.gz.
- 13.N. Kobayashi, B. Pierce, and D. Turner. Linearity and the pi-calculus. In POPL’96. ACM Press, 1996.Google Scholar
- 14.F. Levi and D. Sangiorgi. Controlling interference in ambients. In POPL’00. ACM Press, 2000.Google Scholar
- 15.R. Milner. The polyadic π-calculus: a tutorial. Technical Report ECS-LFCS-91-180, Laboratory for Foundationsof Computer Science,Department of Computer Science, University of Edinburgh, Octorber 1991.Google Scholar
- 17.B. Pierce and D. Sangiorgi. Behavioral equivalence in the polymorphic pi-calculus. In POPL’97. ACM Press, 1997.Google Scholar
- 18.J. Riely and M. Hennessy. A typed language for distributed mobile processes. In POPL’98. ACM Press, 1998.Google Scholar
- 19.J. Riely and M. Hennessy. Trust and partial typing in open systems of mobile agents. In POPL’99. ACM Press, 1999.Google Scholar
- 20.P. Sewell. Global/local subtyping and capability inference for a distributed π-calculus. In ICALP’98. Springer-Verlag, 1998. LNCS 1433.Google Scholar
- 22.N. Yoshida and M. Hennessy. Assigning types to processes. In LICS’00. IEEE, 2000.Google Scholar