Abstract
We propose a model for specifying, analysing and enforcing safe usage of resources. Our usage policies allow for parametricity over resources, and they can be enforced through finite state automata. The patterns of resource access and creation are described through a basic calculus of usages. In spite of the augmented flexibility given by resource creation and by policy parametrization, we devise an efficient (polynomial-time) model-checking technique for deciding when a usage is resource-safe, i.e. when it complies with all the relevant usage policies.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Fournet, C.: Access control based on execution history. In: Proc. 10th Annual Network and Distributed System Security Symposium (2003)
Acciai, L., Boreale, M.: Spatial and behavioral types in the π-calculus. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 372–386. Springer, Heidelberg (2008)
Bartoletti, M., Degano, P., Ferrari, G.L.: Static analysis for stack inspection. In: International Workshop on Concurrency and Coordination (2001)
Bartoletti, M., Degano, P., Ferrari, G.L.: History-based access control with local policies. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 316–332. Springer, Heidelberg (2005)
Bartoletti, M., Degano, P., Ferrari, G.L.: Types and effects for secure service orchestration. In: Proc. 19th CSFW (2006)
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Types and effects for resource usage analysis. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 32–47. Springer, Heidelberg (2007)
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Model checking usage policies. Technical Report TR-08-06, Dip. Informatica, Univ. Pisa (2008)
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Semantics-based design for secure web services. IEEE Transactions on Software Engineering 34(1) (2008)
Bartoletti, M., Zunino, R.: LocUsT: a tool for checking usage policies. Technical Report TR-08-07, Dip. Informatica, Univ. Pisa (2008)
Bauer, L., Ligatti, J., Walker, D.: More enforceable security policies. In: Foundations of Computer Security (FCS) (2002)
Bauer, L., Ligatti, J., Walker, D.: Composing security policies with Polymer. In: Proc. PLDI (2005)
Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theoretical Computer Science 37, 77–121 (1985)
Brewer, D.F.C., Nash, M.J.: The chinese wall security policy. In: Proc. of Symp. on Security and Privacy (1989)
Bruni, R., Mezzina, L.G.: Types and deadlock freedom in a calculus of services, sessions and pipelines. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 100–115. Springer, Heidelberg (2008)
Caires, L., Vieira, H.T.: Typing conversations in the conversation calculus. Technical Report 3/08, DI/FCT/UNL (2008)
Christensen, S.: Decidability and Decomposition in Process Algebras. PhD thesis, Edinburgh University (1993)
Colcombet, T., Fradet, P.: Enforcing trace properties by program transformation. In: Proc. 27th ACM SIGPLAN-SIGACT PoPL (2000)
Erlingsson, Ú., Schneider, F.B.: SASI enforcement of security policies: a retrospective. In: Proc. 7th New Security Paradigms Workshop (1999)
Esparza, J.: On the decidability of model checking for several μ-calculi and Petri nets. In: Tison, S. (ed.) CAAP 1994. LNCS, vol. 787. Springer, Heidelberg (1994)
Fong, P.W.: Access control by tracking shallow execution history. In: IEEE Symposium on Security and Privacy (2004)
Igarashi, A., Kobayashi, N.: Type reconstruction for linear -calculus with i/o subtyping. Inf. Comput. 161(1), 1–44 (2000)
Igarashi, A., Kobayashi, N.: Resource usage analysis. In: Proc. 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2002)
Jalapa: Securing Java with Local Policies, http://jalapa.sourceforge.net
Marriott, K., Stuckey, P.J., Sulzmann, M.: Resource usage verification. In: Proc. First Asian Programming Languages Symposium (2003)
Mayr, R.: Decidability and Complexity of Model Checking Problems for Infinite-State Systems. PhD thesis, Technischen Universität München (1998)
Thiemann, P.: Enforcing safety properties using type specialization. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, p. 62. Springer, Heidelberg (2001)
Wang, J., Takata, Y., Seki, H.: HBAC: A model for history-based access control and its model checking. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 263–278. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R. (2009). Model Checking Usage Policies. In: Kaklamanis, C., Nielson, F. (eds) Trustworthy Global Computing. TGC 2008. Lecture Notes in Computer Science, vol 5474. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00945-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-00945-7_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00944-0
Online ISBN: 978-3-642-00945-7
eBook Packages: Computer ScienceComputer Science (R0)