Abstract
Traditional static typing systems for the pi-calculus are built around capability types that control the read/write access rights on channels and describe the type of the channels’ payload. While static typing has proved adequate for reasoning on process behavior in typed contexts, dynamic techniques have often been advocated as more effective for access control in distributed/untyped contexts.
We study the relationships between the two approaches – static versus dynamic – by contrasting two versions of the asynchronous pi-calculus. The former, aPi, comes with an entirely standard static typing system. The latter, aPi@, combines static and dynamic typing: a static type system associates channels with flat types that only express read/write capabilities and disregard the payload type, while a dynamically typed synchronization complements the static type system to guarantee type soundness.
We show that aPi@ can be encoded into aPi in a fully abstract manner, preserving the respective behavioral equivalences of the two calculi. Besides yielding an interesting expressivity result, the encoding also sheds light on the effectiveness of dynamic typing as a mechanism for access control.
Work partially supported by M.I.U.R (Italian Ministry of Education, University and Research) under contract n. 2005015785.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL, pp. 104–115. ACM Press, New York (2001)
Bugliesi, M., Giunti, M.: Typed processes in untyped contexts. In: De Nicola, R., Sangiorgi, D. (eds.) TGC 2005. LNCS, vol. 3705, pp. 19–32. Springer, Heidelberg (2005)
Bugliesi, M., Giunti, M.: Secure implementations of typed channel abstractions. In: POPL, pp. 251–262. ACM Press, New York (2007)
Bugliesi, M., Macedonio, D., Rossi, S.: Static vs dynamic typing for access control in pi-calculus (extended version). Technical Report CS-2007-5, Dipartimento di informatica, Università Ca’ Foscari di Venezia (2007), Also available at: http://www.dsi.unive.it/~mace/ASIAN07.pdf
Coppo, M., Cozzi, F., Dezani-Ciancaglini, M., Giovannetti, E., Pugliese, R.: A mobility calculus with local and dependent types. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, Springer, Heidelberg (2005)
Coppo, M., Dezani-Ciancaglini, M., Giovannetti, E., Pugliese, R.: Dynamic and local typing for mobile ambients. In: IFIP TCS, pp. 577–590. Kluwer Academic Publishers, Dordrecht (2004)
Gorla, D., Pugliese, R.: Resource access and mobility control with dynamic privileges acquisition. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 119–132. Springer, Heidelberg (2003)
Hennessy, M.: A Distributed Pi-Calculus. Cambridge University Press, Cambridge (2007)
Hennessy, M., Rathke, J.: Typed behavioural equivalences for processes in the presence of subtyping. Mathematical Structures in Computer Science 14(5), 651–684 (2004)
Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. Information and Computation 173(1), 82–120 (2002)
Nestmann, U., Pierce, B.C.: Decoding choice encodings. Information and Computation 163(1), 1–59 (2000)
Nicola, R.D., Ferrari, G.L., Pugliese, R., Venneri, B.: Types for access control. Theoretical Computer Science 240(1), 215–254 (2000)
Pierce, B.C., Sangiorgi, D.: Typing and subtyping for mobile processes. Mathematical Structures in Computer Science 6(5), 409–453 (1996)
Pierce, B.C., Sangiorgi, D.: Behavioral equivalence in the polymorphic pi-calculus. Journal of the ACM 47(3), 531–584 (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bugliesi, M., Macedonio, D., Rossi, S. (2007). Static vs Dynamic Typing for Access Control in Pi-Calculus. In: Cervesato, I. (eds) Advances in Computer Science – ASIAN 2007. Computer and Network Security. ASIAN 2007. Lecture Notes in Computer Science, vol 4846. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76929-3_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-76929-3_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-76927-9
Online ISBN: 978-3-540-76929-3
eBook Packages: Computer ScienceComputer Science (R0)