Abstract
safeDpi is a distributed version of the Picalculus, in which processes are located at dynamically created sites. Parametrised code may be sent between sites using so-called ports, which are essentially higher-order versions of Picalculus communication channels. A host location may protect itself by only accepting code which conforms to a given type associated to the incoming port.
We define a sophisticated static type system for these ports, which restrict the capabilities and access rights of any processes launched by incoming code. Dependent and existential types are used to add flexibility, allowing the behaviour of these launched processes, encoded as process types, to depend on the host’s instantiation of the incoming code.
We also show that a natural contextually defined behavioural equivalence can be characterised coinductively, using bisimulations based on typed actions. The characterisation is based on the idea of knowledge acquisition by a testing environment and makes explicit some of the subtleties of determining equivalence in this language of highly constrained distributed code.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Boreale, M., Sangiorgi, D.: Bisimulation in name-passing calculi without matching. In: Proc. 13th LICS Conf. IEEE Computer Society Press, Los Alamitos (1998)
Cardelli, L., Ghelli, G., Gordon, A.: Ambient groups and mobility types. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, p. 333. Springer, Heidelberg (2000)
Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)
Castagna, G., Nardelli, F.Z.: The Seal calculus revisited: Contextual equivalences and bisimilarity. In: Proc. of FSTTCS. LNCS (2002)
Castagna, G., Vitek, J., Nardelli, F.Z.: The Seal calculus (2003), Available from ftp://ftp.di.ens.fr/pub/users/castagna/seal.ps.gz
Fournet, C., Gonthier, G., Levy, J.-J., Maranget, L., Remy, D.: A calculus of mobile agents. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119. Springer, Heidelberg (1996)
Hennessy, M., Merro, M.: Bisimulation congruences in safe ambients. In: Proc. POPL 2002, the 29th ACM Symposium on Principles of Programming Languages. ACM Press, New York (2002)
Hennessy, M., Merro, M., Rathke, J.: Towards a behavioural theory of access and mobility control in distributed systems. Technical Report 2002:01, COGS, University of Sussex (2002), Extended Abstract published in the Proc. of FoSSaCS (2003)
Hennessy, M., Rathke, J.: Typed behavioural equivalences for processes in the presence of subtyping. In: Harland, J. (ed.) Proc. CATS 2002, Computing: Australasian Theory Symposium. Electronic Notes in Computer Science, vol. 61, Elsevier Science Publishers, Amsterdam (2002), To appear in Mathematical Structures in Computer Science
Hennessy, M., Rathke, J., Yoshida, N.: The full version of this paper. Technical Report 2003:02, Department of Informatics, University of Sussex (2003), available from www.cogs.susx.ac.uk/julianr/
Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. Information and Computation 173, 82–120 (2002)
Honda, K., Yoshida, N.: On reduction-based process semantics. Theoretical Computer Science 152(2), 437–486 (1995)
Igarashi, A., Kobayashi, N.: Resource usage analysis. In: Proc. of POPL 2002, the 29th ACM Symposium on Principles of Programming Languages, pp. 331–342 (2002)
Lhoussaine, C.: Type inference for a distributed pi-calculus. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 253–268. Springer, Heidelberg (2003)
Merro, M., Nardelli, F.Z.: Bisimulation proof techniques for mobile ambients. In: Proc. 30th International Colloquium on Automata, Languages, and Programming (ICALP 2003), Eindhoven. LNCS, Springer, Heidelberg (2003)
Merro, M., Sassone, V.: Typing and subtyping mobility in boxed ambients. In: Proc. CONCUR 2002. LNCS, vol. 1644. Springer, Heidelberg (2002)
Morrisett, G., Crary, K., Glew, N., Walker, D.: Stack-based typed assembly language. In: Leroy, X., Ohori, A. (eds.) TIC 1998. LNCS, vol. 1473, pp. 28–52. Springer, Heidelberg (1998)
Necula, G.C.: Proof-carrying code. In: Proc. of POPL 1997, the 24th ACM Symposium on Principles of Programming Languages, Paris, pp. 106–119 (1997)
Pierce, B., Sangiorgi, D.: Behavioral equivalence in the polymorphic pi-calculus. Journal of the ACM 47(3), 531–584 (2000)
Riely, J., Hennessy, M.: Trust and partial typing in open systems of mobile agents (extended abstract). In: Proc. of POPL 1999, the 26th ACM Symposium on Principles of Programming Languages, pp. 93–104 (1999) (To appear in the Journal of Automated Reasoning)
Sangiorgi, D., Walker, D.: The π-calculus. Cambridge University Press, Cambridge (2001)
Walker, D.: A type system for expressive security properties. In: Proc. Popl 2000, the 27th ACM Symposium on Principles of Programming Languages, Boston, pp. 254–267 (2000)
Yoshida, N., Hennessy, M.: Assigning types to processes. Information and Computation 172, 82–120 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hennessy, M., Rathke, J., Yoshida, N. (2004). safeDpi: A Language for Controlling Mobile Code. In: Walukiewicz, I. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2004. Lecture Notes in Computer Science, vol 2987. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24727-2_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-24727-2_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21298-0
Online ISBN: 978-3-540-24727-2
eBook Packages: Springer Book Archive