Advertisement

A Calculus for Modeling Floating Authorizations

  • Jovanka Pantović
  • Ivan Prokić
  • Hugo Torres Vieira
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10854)

Abstract

Controlling resource usage in distributed systems is a challenging task given the dynamics involved in access granting. Consider, e.g., the setting of floating licenses where access can be granted if the request originates in a licensed domain and if the number of active users is within the license limits. Access granting in such scenarios is given in terms of floating authorizations, addressed in this paper as first class entities of a process calculus model, encompassing the notions of domain, accounting and delegation. We present the operational semantics of the model in two equivalent alternative ways, each informing on the specific nature of authorizations. We also introduce a typing discipline to single out systems that never get stuck due to lacking authorizations, addressing configurations where authorization assignment is not statically prescribed in the system specification.

Notes

Acknowledgments

We thank anonymous reviewers for useful remarks and suggestions. This work has been partially supported by the Ministry of Education and Science of the Republic of Serbia, project ON174026, and EU COST Action IC1405 (Reversible Computation).

References

  1. 1.
    Acciai, L., Boreale, M.: Spatial and behavioral types in the pi-calculus. Inf. Comput. 208(10), 1118–1153 (2010).  https://doi.org/10.1016/j.ic.2009.10.011MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Armstrong, W.J., Nayar, N., Stamschror, K.P.: Management of a concurrent use license in a logically-partitioned computer. US Patent 6,959,291 (2005)Google Scholar
  3. 3.
    Baratti, P., Squartini, P.: License management system. US Patent 6,574,612 (2003)Google Scholar
  4. 4.
    Bodei, C., Dinh, V.D., Ferrari, G.L.: Checking global usage of resources handled with local policies. Sci. Comput. Program. 133, 20–50 (2017).  https://doi.org/10.1016/j.scico.2016.06.005CrossRefGoogle Scholar
  5. 5.
    Das, A., Hoffmann, J., Pfenning, F.: Work analysis with resource-aware sessiontypes. CoRR abs/1712.08310 (2017). http://arxiv.org/abs/1712.08310
  6. 6.
    Ferris, J.M., Riveros, G.E.: Offering additional license terms during conversion of standard software licenses for use in cloud computing environments. US Patent 9,053,472 (2015)Google Scholar
  7. 7.
    Freeman, T.S., Pfenning, F.: Refinement types for ML. In: Wise, D.S. (ed.) Proceedings of the PLDI 1991, pp. 268–277. ACM (1991).  https://doi.org/10.1145/113445.113468
  8. 8.
    Ghilezan, S., Jakšić, S., Pantović, J., Pérez, J.A., Vieira, H.T.: Dynamic role authorization in multiparty conversations. Formal Asp. Comput. 28(4), 643–667 (2016).  https://doi.org/10.1007/s00165-016-0363-5MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Giunti, M., Palamidessi, C., Valencia, F.D.: Hide and new in the pi-calculus. In: Proceedings of EXPRESS/SOS 2012, EPTCS, vol. 89, pp. 65–79 (2012).  https://doi.org/10.4204/EPTCS.89.6
  10. 10.
    Gorla, D., Pugliese, R.: Dynamic management of capabilities in a network aware coordination language. J. Log. Algebr. Program. 78(8), 665–689 (2009).  https://doi.org/10.1016/j.jlap.2008.12.001MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Hüttel, H., Lanese, I., Vasconcelos, V.T., Caires, L., Carbone, M., Deniélou, P., Mostrous, D., Padovani, L., Ravara, A., Tuosto, E., Vieira, H.T., Zavattaro, G.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3:1–3:36 (2016).  https://doi.org/10.1145/2873052CrossRefGoogle Scholar
  12. 12.
    Kobayashi, N., Suenaga, K., Wischik, L.: Resource usage analysis for the p-calculus. Log. Methods Comput. Sci. 2(3) (2006).  https://doi.org/10.2168/LMCS-2(3:4)2006
  13. 13.
    Pantovic, J., Prokic, I., Vieira, H.T.: A calculus for modeling floating authorizations. CoRR abs/1802.05863 (2018). https://arxiv.org/abs/1802.05863
  14. 14.
    Sangiorgi, D., Walker, D.: The Pi-Calculus - A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  15. 15.
    Swamy, N., Chen, J., Chugh, R.: Enforcing stateful authorization and information flow policies in Fine. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 529–549. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-11957-6_28CrossRefGoogle Scholar
  16. 16.
    Vivas, J., Yoshida, N.: Dynamic channel screening in the higher order pi-calculus. Electr. Notes Theor. Comput. Sci. 66(3), 170–184 (2002).  https://doi.org/10.1016/S1571-0661(04)80421-3CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2018

Authors and Affiliations

  1. 1.Faculty of Technical SciencesUniversity of Novi SadNovi SadSerbia
  2. 2.IMT School for Advanced Studies LuccaLuccaItaly

Personalised recommendations