nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

01.10.2016 | PV 2014

Parameterized model checking for security policy analysis

verfasst von: Silvio Ranise, Anh Truong, Riccardo Traverso

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 5/2016

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We explain how a parameterized model checking technique can be exploited to mechanize the analysis of access control policies. The main advantage of the approach is to reason regardless of the number of users of the system in which the policy is enforced. This permits to obtain more useful results from the analysis; for instance, ensuring that sensitive permissions cannot be leaked regardless of the number of users in the system. We also briefly discuss how some heuristics make the technique scalable to handle (very) large policies. This is demonstrated by a comparative experimental evaluation with state-of-the-art tools for the analysis of access control policies.

Vorheriger Artikel Soundness of data-aware, case-centric processes

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

This definition is different from that in the seminal paper [2] introducing the safety problem. In [2], unsafety is characterized by checking for permission leakages with respect to the policy immediately before the operation leaking the permission and not with respect to the initial policy as above. According to [3], such a notion of permission leakage creates several difficulties and (almost) all works proposing techniques to handle the safety problem have used the one reported above.

We thank Martin Suda for pointing out this example.

We thank the authors of Mohawk, Vac, and Pms for making available to us the latest version of their tools. We also thank the support team of NuSMV for their help with the installation of the tool, a necessary pre-requisite for using Mohawk.

The module \({{\mathtt {Filter}}}\) and the slicing technique in [5] share the goal of removing administrative actions which are irrelevant to the user-role reachability problem under consideration. The hope is to reduce the state space to be explored by the search procedure (in our case, the backward reachability procedure) invoked afterwards. In principle, \({{\mathtt {Filter}}}\) can be used in place of slicing and vice versa; the main difference between the two approaches is the level of “aggressiveness”: the former performs a computationally cheap check for establishing if an action is relevant, whereas the latter is computationally more expensive.

De Capitani di Vimercati, S., Foresti, S., Jajodia, S., Samarati, P.: Access control policies and languages. Int J Comput Sci Eng (IJCSE) 3(2), 94–102 (2007)CrossRef

Harrison, M.A., Ruzzo, W.L., Ullman, J.D.: Protection in operating systems. CACM 19(8), 461–471 (1976)MathSciNetCrossRefMATH

Tripunitara, M., Li, N.: The foundational work of Harrison–Ruzzo–Ullman revisited. IEEE Trans Depend Sec Comput 10(1), 28–39 (2013)CrossRef

Armando, A., Ranise, S.: Scalable automated symbolic analysis of administrative role-based access control policies by SMT solving. J Comput Secur 20(4), 309–352 (2012)CrossRef

Ferrara, A.L., Madhusudan, P., Parlato, G.: Policy analysis for self-administrated role-based access control. In: TACAS. Springer, Berlin (2013)

Sandhu, R., Coyne, E., Feinstein, H., Youmann, C.: Role-based access control models. IEEE Comput 2(29), 38–47 (1996)CrossRef

Sandhu, R., Bhamidipati, V., Munawer, Q.: The ARBAC97 model for role-based control administration of roles. ACM TISSEC 1(2), 105–135 (1999)CrossRef

Jayaraman, K., Ganesh, V., Tripunitara, M., Rinard, M., Chapin, S.: Automatic error finding for access-control policies. In: CCS. ACM, New York (2011)

Li, N., Tripunitara, M.V.: Security analysis in role-based access control. ACM TISSEC 9(4), 391–420 (2006)CrossRef

10.

Stoller, S.D., Yang, P., Ramakrishnan, C.R., Gofman, M.I.: Efficient policy analysis for administrative role based access control. In: CCS. ACM Press, New York (2007)

11.

Yang, P., Gofman, M.l., Stoller, S., Yang, Z.: Policy analysis for administrative role based access control without separate administration. J Comput Secur (2014)

12.

Sasturkar, A., Yang, P., Stoller, S.D., Ramakrishnan, C.R.: Policy analysis for administrative role based access control. In: CSF. IEEE Press, New York (2006)

13.

Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: Proceedings of LICS, pp. 313–321 (1996)

14.

Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. In: LMCS, vol. 6, no 4 (2010)

15.

Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Proceedings of IJCAR’10. LNCS, New York (2010)

16.

Piskac, R., de Moura, L., Bjørner, N.: Deciding effectively propositional logic using DPLL and substitution sets. J Autom Reas 44(4), 401–424 (2010)MathSciNetCrossRefMATH

17.

Crampton, J.: Understanding and developing role-based administrative models. In: Proceedings of the 12th CCS. ACM Press, New York, pp. 158–167 (2005)

18.

Sasturkar, A., Yang, P., Stoller, S.D., Ramakrishnan, C.R.: Policy analysis for administrative role based access control. Theor Comput Sci 412(44), 6208–6234 (2011)MathSciNetCrossRefMATH

19.

Ranise, S.: Symbolic backward reachability with effectively propositional logic-applications to security policy analysis. FMSD 42(1), 24–45 (2013)MATH

20.

Ramsey, F.P.: On a problem of formal logic. Proc Lond Math Soc s2–30(1), 264–286 (1930)MathSciNetCrossRefMATH

21.

Beckert, B., Hoare, C.A.R., Hähnle, R., Smith, R., Green, D.R., Ranise, S., Tinelli, C., Ball, T., Rajamani, S.K.: Intelligent systems and formal methods in software engineering. IEEE Int Syst 21(6), 71–81 (2006)CrossRef

22.

Enderton, H.B.: A mathematical introduction to logic. Academic Press Inc, New York (1972)MATH

23.

Alberti, F., Armando, A., Ranise, S.: ASASP: automated symbolic analysis of security policies. In: CADE. LNCS, vol. 6803. Springer, Berlin, pp 26–34 (2011)

24.

Ranise, S., Truong, T.A., Armando, A.: Boosting model checking to analyse large ARBAC policies. In: 8th STM Workshop, LNCS, vol. 7783. Springer, Berlin, pp 273–288 (2012)

25.

Gofman, M.I., Luo, R., Solomon, A.C., Zhang, Y., Yang, P., Stoller, S.D.: Rbac-pat: a policy analysis tool for role based access control. In: TACAS, LNCS, vol. 5505. Springer, Berlin, pp 46–49 (2009)

26.

Li, N., Tripunitara, M.V.: Security analysis in role-based access control. In: Symp. on Access Control Models and Technologies. ACM Press, New York, pp 126–135 (2004)

27.

Jha, S., Li, N., Tripunitara, M., Wang, Q., Winsborough, W.: Towards formal verification of role-based access control policies. IEEE TDSeC 5(4), 242–255 (2008)

28.

Alberti, F., Armando, A., Ranise, S.: Efficient symbolic automated analysis of administrative role based access control policies. In: ASIACCS. ACM Press, New York (2011)

29.

Jayaraman, K., Tripunitara, M.V., Ganesh, V., Rinard, M.C., Chapin, S.J.: Mohawk: abstraction-refinement and bound-estimation for verifying access control policies. ACM TISSeC 15(4) (2013)

30.

Clarke, E.M., Strichman, O., Zhu, Y., Biere, A., Cimatti, A.: Bounded model checking. Adv Comput 58, 117–148 (2003)CrossRef

31.

Ranise, S., Traverso, R.: ALPS: an action language for policy specification and automated safety analysis. In: STM Workshop, number 8743 in LNCS. Springer, Berlin, pp. 146–161 (2014)

32.

Fikes, Richard E., Nilsson, Nils J.: Strips: a new approach to the application of theorem proving to problem solving. Artif. Intell. 2(3), 189–208 (1972)MATH

33.

Erol, K., Nau, D.S., Subrahmanian, V.S.: Complexity, decidability and undecidability results for domain-independent planning: a detailed analysis. Artif. Intell. 76, 75–88 (1991)MathSciNetCrossRefMATH

34.

Ranise, S., Truong, A.: Incremental analysis of evolving administrative role based access control policies. In: 28th Annual IFIP WG 11.3 Working Conference DBSeC14, Vienna, Austria, 14-16 July 2014. LNCS, vol 8566. Springer, Berlin, pp. 260–275 (2014)

35.

Gofman, M., Yang, P.: Efficient policy analysis for evolving administrative role based access control. Int J Softw Inf (2014)

36.

Gofman, M.I., Luo, R., Yang, P.: User-role reachability analysis of evolving administrative role based access control. In: ESORICS, vol. 6345. LNCS, Berlin, pp. 455–471 (2010)

37.

Ranise, S., Truong, A., Armando, A.: Scalable and precise automated analysis of administrative temporal role-based access control. In: tACM SACMAT, London, Ontario, Canada, June 25–25 2014. ACM Press, New York, pp. 103–114 (2014)

38.

Uzun, E., Atluri, V., Sural, S., Vaidya, J, Parlato G, Ferrara AL (2012) Analyzing temporal role based access control models. In: SACMAT. ACM, New York, pp. 177–186 (2014)

39.

Ranise, S., Truong, A., Viganò, L.: Automated analysis of RBAC policies with temporal constraints and static role hierarchies. In: 30th ACM/SIGAPP SAC, Salamanca, Spain, April 13–17, 2015. ACM Press, New York (2015)

Titel: Parameterized model checking for security policy analysis
verfasst von: Silvio Ranise
Anh Truong
Riccardo Traverso
Publikationsdatum: 01.10.2016
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 5/2016
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-015-0410-1

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 5/2016

Counting dynamically synchronizing processes

Soundness of data-aware, case-centric processes

Parameterized verification

Parameterized verification through view abstraction

A unified view of parameterized verification of abstract models of broadcast communication