Hostname: page-component-cc8bf7c57-hbs24 Total loading time: 0 Render date: 2024-12-11T22:19:46.956Z Has data issue: false hasContentIssue false
  • English
  • Français

A type system for Discretionary Access Control†

Published online by Cambridge University Press:  01 August 2009

MICHELE BUGLIESI ,
DARIO COLAZZO ,
SILVIA CRAFA  and
DAMIANO MACEDONIO
MICHELE BUGLIESI
Affiliation:
Dipartimento di Informatica, Università Ca' Foscari, Via Torino 155, 30172 Venezia-Mestre, Italy Email: michele@dsi.unive.it, mace@dsi.unive.it
DARIO COLAZZO
Affiliation:
LRI, Université Paris Sud, 91405 Orsay Cedex - France Email: dario.colazzo@lri.fr
SILVIA CRAFA
Affiliation:
Dipartimento di Matematica Pura e Applicata, Università di Padova, Via Trieste 63, 35121 Padova, Italy Email: crafa@math.unipd.it
DAMIANO MACEDONIO
Affiliation:
Dipartimento di Informatica, Università Ca' Foscari, Via Torino 155, 30172 Venezia-Mestre, Italy Email: michele@dsi.unive.it, mace@dsi.unive.it
Get access Rights & Permissions [Opens in a new window]

Abstract

Discretionary Access Control (DAC) systems provide powerful resource management mechanisms based on the selective distribution of capabilities to selected classes of principals. We study a type-based theory of DAC models for a process calculus that extends Cardelli, Ghelli and Gordon's pi-calculus with groups (Cardelli et al. 2005). In our theory, groups play the role of principals and form the unit of abstraction for our access control policies, and types allow the specification of fine-grained access control policies to govern the transmission of names, bound the (iterated) re-transmission of capabilities and predicate their use on the inability to pass them to third parties. The type system relies on subtyping to achieve a selective distribution of capabilities to the groups that control the communication channels. We show that the typing and subtyping relationships of the calculus are decidable. We also prove a type safety result, showing that in well-typed processes all names:

  1. (i) flow according to the access control policies specified by their types; and

  2. (ii) are received at the intended sites with the intended capabilities.

We illustrate the expressive power and the flexibility of the typing system using several examples.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 19 , Issue 4 , August 2009 , pp. 839 - 875
Copyright
Copyright © Cambridge University Press 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abadi, M. and Gordon, A. D. (1997) Reasoning about cryptographic protocols in the Spi calculus. In: Proceedings CONCUR'97. Springer-Verlag Lecture Notes in Computer Science 1243 59–73.CrossRefGoogle Scholar
Brandt, M. and Henglein, F. (1998) Coinductive axiomatization of recursive type equality and subtyping. Fundaenta Informaticae 33 (4)309–338.CrossRefGoogle Scholar
Bugliesi, M., Colazzo, D. and Crafa, S. (2004) Type based Discretionary Access Control. In: Proceedings CONCUR'04. Springer-Verlag Lecture Notes in Computer Science 3170 225–239.CrossRefGoogle Scholar
Bugliesi, M. and Giunti, M. (2007) Secure implementations of typed channel abstractions. In: POPL'07, ACM Press 251–262.CrossRefGoogle Scholar
Carbone, M., Honda, K. and Yoshida, N. (2007) Structured communication-centred programming for web services. In: Proceedings ESOP'07. Springer-Verlag Lecture Notes in Computer Science 4421 2–17.CrossRefGoogle Scholar
Cardelli, L., Ghelli, G. and Gordon, A. D. (2005) Secrecy and group creation. Information and Computation 196 (2)127–155.CrossRefGoogle Scholar
Chothia, T., Duggan, D. and Vitek, J. (2003) Type-based Distributed Access Control. In: CSFW'03, IEEE Computer Society 170–184.Google Scholar
De Nicola, R., Ferrari, G., Pugliese, R. and Venneri, B. (2000) Types for access control. Theoretical Computer Science 240 (1)215–254.CrossRefGoogle Scholar
De Nicola, R., Gorla, D. and Pugliese, R. (2006) Confining data and processes in global computing applications. Sci. Comput. Program. 63 (1)57–87.CrossRefGoogle Scholar
Fournet, C., Gordon, A. and Maffeis, S. (2007) A type discipline for authorization in distributed systems. In: CSF'07, IEEE Computer Society 31–48.Google Scholar
Gapeyev, V., Levin, M. Y. and Pierce, B. C. (2002) Recursive subtyping revealed. Journal of Functional Programming 12 (6)511–548.CrossRefGoogle Scholar
Gordon, A. and Jeffrey, A. (2004) Types and effects for asymmetric cryptographic protocols. Journal of Computer Security 12 (3–4)435–483.CrossRefGoogle Scholar
Gorla, D. and Pugliese, R. (2003) Resource access and mobility control with dynamic privileges acquisition. In: Proceedings ICALP'03. Springer-Verlag Lecture Notes in Computer Science 2719 119–132.CrossRefGoogle Scholar
Hennessy, M., Rathke, J. and Yoshida, N. (2005) SafeDpi: a language for controlling mobile code. Acta Informatica 42 (4–5) 227–290.CrossRefGoogle Scholar
Hennessy, M. and Riely, J. (2002a) Information flow vs resource access in the asynchronous π-calculus. ACM Transactions on Programming Languages and Systems 24 (5)566–591.CrossRefGoogle Scholar
Hennessy, M. and Riely, J. (2002b) Resource access control in systems of mobile agents. Information and Computation 173 82–120.CrossRefGoogle Scholar
Honda, K., Vasconcelos, V. and Kubo, M. (1998) Language primitives and type discipline for structured communication-based programming. In: Proceedings ESOP '98. Springer-Verlag Lecture Notes in Computer Science 1381 122–138.CrossRefGoogle Scholar
Honda, K., Vasconcelos, V. and Yoshida, N. (2000) Secure information flow as typed process behaviour. In: Proceedings ESOP '00. Springer-Verlag Lecture Notes in Computer Science 1782 188–199.Google Scholar
Honda, K., Yoshida, N. and Carbone, M. (2008) Multiparty asynchronous session types. In: POPL'08, ACM Press 273–284.CrossRefGoogle Scholar
Kobayashi, N. (2005) Type-based information flow analysis for the pi-calculus. Acta Informatica 42 (4)291–347.CrossRefGoogle Scholar
Lampson, B. (1974) Protection. ACM Operating Systems Review 8 (1)18–24.CrossRefGoogle Scholar
McCollum, C., Messing, J. R. and Notargiacomo, L. (1990) Beyond the pale of MAC and DAC – defining new forms of access control. Proceedings of IEEE Symposium on Security and Privacy 190–200.CrossRefGoogle Scholar
Myers, A. C. and Liskov, B. (2000) Protecting privacy using the decentralized label model. ACM Trans. Softw. Eng. Methodol 9 (4)410–442.CrossRefGoogle Scholar
Pierce, B. and Sangiorgi, D. (1996) Typing and subtyping for mobile processes. Mathematical Structures in Computer Science 6 (5)409–453.CrossRefGoogle Scholar
Pottier, F. (2002) A simple view of type-secure information flow in the π-calculus. In: CSFW'02, IEEE Computer Society 320–330.Google Scholar
Riely, J. and Hennessy, M. (1998) A typed language for distributed mobile processes. In: POPL '98, ACM Press 378–390.CrossRefGoogle Scholar
Samarati, P. and De Capitani di Vimercati, S. (2001) Access control: Policies, models, and mechanisms. In: Focardi, R. and Gorrieri, R. (eds.) Foundations of Security Analysis and Design. Springer-Verlag Lecture Notes in Computer Science 2171 137–196.CrossRefGoogle Scholar
Sandhu, R. S. and Munawer, Q. (1998) How to do discretionary access control using roles. In: ACM Workshop on Role-Based Access Control 47–54.CrossRefGoogle Scholar
Schneider, F. B. (2000) Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3 (1)30–50.CrossRefGoogle Scholar
Sewell, P. and Vitek, J. (2003) Secure composition of untrusted code: Box π, wrappers and causality types. Journal of Computer Security 11 (2)135–188.CrossRefGoogle Scholar