zbMATH — the first resource for mathematics

Symbolic backward reachability with effectively propositional logic. Application to security policy analysis. (English) Zbl 1284.68520
Summary: We describe a symbolic procedure for solving the reachability problem of transition systems that use formulae of Effectively Propositional Logic to represent sets of backward reachable states. We discuss the key ideas for the mechanization of the procedure where fix-point checks are reduced to SMT problems. We also show the termination of the procedure on a sub-class of transition systems. Then, we discuss how reachability problems for this sub-class can be used to encode analysis problems of administrative policies in the Role-Based Access Control (RBAC) model that is one of the most widely adopted access control paradigms. An implementation of a refinement of the backward reachability procedure, called asasp, shows better flexibility and scalability than a state-of-the-art tool on a significant set of security problems.
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T27 Logic in artificial intelligence
68Q60 Specification and verification (program logics, model checking, etc.)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Full Text: DOI
[1] Alberti F, Armando A, Ranise S (2011) ASASP: Automated symbolic analysis of security policies. In: 23rd int conf on autom ded (CADE). LNCS, vol 6803. Springer, Berlin, pp 26–34 · Zbl 05934339
[2] Alberti F, Armando A, Ranise S (2011) Efficient symbolic automated analysis of administrative role based access control policies. In: 6th ACM symp on information, computer, and communications security (ASIACCS) · Zbl 05934339
[3] Abdulla PA, Cerans K, Jonsson B, Tsay Y-K (1996) General decidability theorems for infinite-state systems. In: Proc of LICS, pp 313–321
[4] Armando A, Ranise S (2010) Automated symbolic analysis of ARBAC policies. In: 6th int workshop on security and trust management (STM)
[5] Crampton J (2002) Authorization and antichains. PhD thesis, Birkbeck, University of London, London, England · Zbl 0983.06003
[6] Crampton J (2005) Understanding and developing role-based administrative models. In: Proc 12th ACM conf on comp and comm security (CCS). ACM, New York, pp 158–167
[7] De Capitani di Vimercati S, Foresti S, Jajodia S, Samarati P (2007) Access control policies and languages. Int J Comput Sci Eng (IJCSE) 3(2):94–102
[8] Dickson LE (1913) Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Am J Math 35(4):413–422 · JFM 44.0220.02 · doi:10.2307/2370405
[9] de Moura L (2011) Personal communication
[10] Enderton HB (1972) A mathematical introduction to logic. Academic Press, San Diego · Zbl 0298.02002
[11] Frohardt R, Chang B-YE, Sankaranarayanan S (2011) Access nets: modeling access to physical spaces. In: Proc of int conf on verification, model checking, and abstract interpretation (VMCAI) · Zbl 1317.68114
[12] Fontaine P, Gribomont EP (2003) Decidability of invariant validation for parameterized systems. In: TACAS. LNCS, vol 2619. Springer, Berlin, pp 97–112 · Zbl 1031.68049
[13] Gofman MI, Luo R, Solomon AC, Zhang Y, Yang P, Stoller SD (2009) Rbac-pat: a policy analysis tool for role based access control. In: Proc of the 15th int conf on tools and algorithms for the construction and analysis of systems (TACAS). LNCS, vol 5505. Springer, Berlin, pp 46–49
[14] Ghilardi S, Ranise S (2010) Backward reachability of array-based systems by smt solving: termination and invariant synthesis. LMCS 6(4):1–48 · Zbl 1213.68379
[15] Ghilardi S, Ranise S (2010) MCMT: a model checker modulo theories. In: Proc of IJCAR’10. LNCS, vol 6803 · Zbl 1291.68257
[16] Hodges W (1993) Model theory. Cambridge University Press, Cambridge · Zbl 0789.03031
[17] Jayaraman K, Ganesh V, Tripunitara M, Rinard MC, Chapin S (2011) Automatic error finding in access-control policies. In: Proc of the ACM conference on computer and communications security (CCS), Chicago, USA
[18] Kuhn DR, Coyne EJ, Weil TR (2010) Adding attributes to role based access control. IEEE Comput 43(6):79–81 · doi:10.1109/MC.2010.155
[19] Lewis HR (1980) Complexity results for classes of quantificational formulas. J Comput Syst Sci 21(3):317–353 · Zbl 0471.03034 · doi:10.1016/0022-0000(80)90027-6
[20] Li N, Mao Z (2007) Administration in role based access control. In: Proc ACM symp on information, computer, and communication security (ASIACCS)
[21] Li N, Tripunitara MV (2006) Security analysis in role-based access control. ACM Trans Inf Syst Secur (TISSEC) 9(4):391–420 · Zbl 05453958 · doi:10.1145/1187441.1187442
[22] Navarro Pérez JA, Voronkov A (2007) Encodings of bounded LTL model checking in effectively propositional logic. In: CADE-21: proc of the 21st int conf on automated deduction. LNAI, vol 4603. Springer, Berlin, pp 346–361 · Zbl 1213.68386
[23] Navarro Pérez JA, Voronkov A (2008) Collection of papers dedicated to Harald Ganzinger’s memory, chapter planning with effectively propositional logic. Springer, Berlin
[24] Ramsey FP (1930) On a problem of formal logic. Proc Lond Math Soc s2-30(1):264–286 · JFM 55.0032.04 · doi:10.1112/plms/s2-30.1.264
[25] Rushby J (2006) Harnessing disruptive innovation in formal verification. In: Fourth international conference on software engineering and formal methods (SEFM), September. IEEE Comput Soc, Los Alamitos, pp 21–28
[26] Sandhu R, Coyne E, Feinstein H, Youmann C (1996) Role-based access control models. IEEE Comput 2(29):38–47 · Zbl 05087687 · doi:10.1109/2.485845
[27] SMT-LIB. http://www.smt-lib.org
[28] Schaad A, Moffett JD (2002) A lightweight approach to specification and analysis of role-based access control extensions. In: Proc. 7th SACMAT. ACM, New York, pp 13–22
[29] Schaad A, Moffet J, Jacob J (2001) The role-based access control system of a European bank: a case study and discussion. In: Proc of the 6th SACMAT. ACM, New York, pp 3–9
[30] SPASS. http://www.spass-prover.org
[31] Stoller S. http://www.cs.stonybrook.edu/\(\sim\)stoller/ccs2007
[32] Sutcliffe G (2009) The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J Autom Reason 43(4):337–362 · Zbl 1185.68636 · doi:10.1007/s10817-009-9143-8
[33] Stoller SD, Yang P, Gofman MI, Ramakrishnan CR (2007) Symbolic reachability analysis for parameterized administrative role based access control. In: Proc of SACMAT’09, pp 445–454
[34] Stoller SD, Yang P, Ramakrishnan CR, Gofman MI (2007) Efficient policy analysis for administrative role based access control. In: Proc of the 14th conf on computer and communications security (CCS). ACM, New York
[35] Sasturkar A, Yang P, Stoller SD, Ramakrishnan CR (2006) Policy analysis for administrative role based access control. In: Proc of the 19th computer security foundations (CSF) workshop, July. IEEE Comput Soc, Los Alamitos · Zbl 1234.68143
[36] Sasturkar A, Yang P, Stoller SD, Ramakrishnan CR (2011) Policy analysis for administrative role based access control. Theor Comput Sci 412(44):6208–6234 · Zbl 1234.68143 · doi:10.1016/j.tcs.2011.05.009
[37] Tinelli C, Zarba CG (2005) Combining non-stably infinite theories. J Autom Reason 34(3):209–238 · Zbl 1108.03014 · doi:10.1007/s10817-005-5204-9
[38] Z3. http://research.microsoft.com/en-us/um/redmond/projects/z3
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.