×

zbMATH — the first resource for mathematics

safeDpi: a language for controlling mobile code. (English) Zbl 1081.68003
Summary: 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.

MSC:
68M14 Distributed systems
68N15 Theory of programming languages
Keywords:
pi-calculus
Software:
SafeDpi; TALx86
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Boreale, M., Sangiorgi, D.: Bisimulation in name-passing calculi without matching. In Proceedings of 13th LICS Conf, IEEE Computer Society Press (1998) · Zbl 0908.68103
[2] Cardelli, L., Ghelli, G., Gordon, A.: Ambient groups and mobility types. In Proceedings of IFIP TCS 2000, vol. 1872 of Lecture Notes in Computer Science, Springer-Verlag (2000) · Zbl 0998.68536
[3] Cardelli, L., Gordon, A.: Mobile ambients. In Proceedings of FoSSaCS ’98, LNCS, Springer-Verlag (1998) · Zbl 0954.68108
[4] Castagna, G., Nardelli, F.Z.: The Seal calculus revisited: Contextual equivalences and bisimilarity. In Proceedings of FSTTCS, Lecture Notes in Computer Science (2002) · Zbl 1027.68088
[5] Castagna, G., Vitek, J., Zappa, F.: The Seal calculus. Available from ftp://ftp.di.ens.fr/pub/users/castagna/seal.ps.gz. · Zbl 1101.68060
[6] Fournet, C., Gonthier, G., Levy, J.-J., Maranget, L., Remy, D.: A calculus of mobile agents. In Proceedings of CONCUR, vol. 1119 of Lecture notes in computer science, Springer-Verlag (1996)
[7] Hennessy, M., Merro, M.: Bisimulation congruences in safe ambients. In Proceedings of POPL 02, ACM Press (2002) · Zbl 1323.68412
[8] Hennessy, M., Merro, M., Rathke, J.: Towards a behavioural theory of access and mobility control in distributed systems. Theoretical Computer Science 322, 615–669 (2003) · Zbl 1071.68009 · doi:10.1016/j.tcs.2003.12.024
[9] Hennessy, M., Rathke, J.: Typed behavioural equivalences for processes in the presence of subtyping. Mathematical Structures in Computer Science 14, 651–684 (2004) · Zbl 1093.68062 · doi:10.1017/S0960129504004281
[10] Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. Information and Computation 173, 82–120 (2002) · Zbl 1009.68081 · doi:10.1006/inco.2001.3089
[11] Honda, K., Yoshida, N.: On reduction-based process semantics. Theoretical Computer Science 152(2), 437–486 (1995) · Zbl 0871.68122 · doi:10.1016/0304-3975(95)00074-7
[12] Igarashi, A., Kobayashi, N.: Resource usage analysis. In Proceedings of ACM Symposium on Principles of Programming Languages (POPL’02), pp. 331–342 (2002) · Zbl 1323.68377
[13] Jeffrey, A., Rathke, J.: Contextual equivalence for higher-order \(\pi\)-calculus revisited. In Proceedings MFPS XIX, Montreal (2003) · Zbl 1125.68084
[14] Lhoussaine, C.: Type inference for a distributed pi-calculus. In ESOP’02, vol. 2618 of LNCS, Springer-Verlag, pp. 253–269 (2002) · Zbl 1032.03027
[15] Merro, M., Nardelli, F.Z.: Bisimulation proof techniques for mobile ambients. In Proceedings of 30th International Colloquium on Automata, Languages, and Programming (ICALP 2003), Eindhoven, Lecture Notes in Computer Science, Springer-Verlag, 2003 · Zbl 1039.68085
[16] Merro, M., Sassone, V.: Typing and subtyping mobility in boxed ambients. In Proceedings CONCUR 02, vol. 1644 of Lecture Notes in Computer Science, Springer-Verlag (2002) · Zbl 1012.68529
[17] Morrisett, G., Crary, K., Glew, N., Walker, D.: Stack-based typed assembly language. In Types in Compilation, vol. 1473 of Lecture notes in Computer Science, Springer-Verlag, pp. 25–35 (1998) · Zbl 0998.68037
[18] Necula, G.C.: Proof-carrying code. In Conference Record of POPL’97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Program- ming Languages (Paris, France), pp. 106–119 (1997)
[19] Pierce, B., Sangiorgi, D.: Behavioral equivalence in the polymorphic pi-calculus. Journal of the ACM 47(3), 531–584, (2000) · Zbl 1094.68591 · doi:10.1145/337244.337261
[20] Riely, J., Hennessy, M.: Trust and partial typing in open systems of mobile agents. Journal of Automated Reasoning 31, 335–370 (2003) · Zbl 1069.68076 · doi:10.1023/B:JARS.0000021016.61054.3b
[21] Sangiorgi, D., Walker, D.: The \(\pi\)-calculus. Cambridge University Press (2001) · Zbl 0981.68116
[22] Schmitt, A., Stefani, J.-B.: The M-calculus: A higher-order distributed process calculus. In POPL2003 (2003) · Zbl 1321.68365
[23] Walker, D.: A type system for expressive security properties. In the twenty seventh ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, pp. 254–267 (2000) · Zbl 1323.68233
[24] Yoshida, N.: Channel dependent types for higher-order mobile processes. In Conference Record of POPL ’04: The 24th ACM SIGPLAN-SIGACT Sym- posium on Principles of Programming Languages, Venice, Italy (2004) · Zbl 1325.68162
[25] Yoshida, N., Hennessy, M.: Subtyping and locality in distributed higher order processes. In Proceedings of CONCUR, vol. 1664 of Lecture notes in computer science, Springer-Verlag (1999) · Zbl 0940.68024
[26] Yoshida, N., Hennessy, M.: Assigning types to processes. Information and Computation 172, 82–120 (2002) · Zbl 1009.68085
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.