Skip to main content
Erschienen in: Formal Methods in System Design 1/2013

01.02.2013

Symbolic backward reachability with effectively propositional logic

Applications to security policy analysis

verfasst von: Silvio Ranise

Erschienen in: Formal Methods in System Design | Ausgabe 1/2013

Einloggen

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

search-config
loading …

Abstract

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.

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!

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!

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!

Fußnoten
1
Since BSR formulae do not allow the use of function symbols, their Herbrand universe is finite and, therefore, a satisfiable formula always admits a finite model.
 
2
Here and in the rest of the example, we omit the “type” of variables. For example, the formula above should be written as ∀x,y.(U(x)∧R(x))⇒(ua(x,y)⇔((x=Ay=Em)∨(x=By=M)∨(x=Cy=HR))), where U is the unary predicate recognizing users and R is that for roles. In other words, quantifiers should always be relativized to the appropriate unary predicates U and R.
 
3
More precisely, let \(\theta_{n_{f}}\) be the ∃+-BSR formula labelling n f and tr be a transition formula. Compute \(\mathit {Pre}(\mathit{tr},\theta_{n_{f}})\) along the lines of the proof of Proposition 1 and then transform the resulting existential BSR formula into a finite disjunction of ∃+-BSR formulae by standard logical manipulations. Repeat this process for each transition formula tr. At the end of this process, you obtain a set of ∃+-BSR formulae whose disjunction is logically equivalent to the pre-image of \(\theta_{n_{f}}\) with respect to the disjunction of all the transitions that are used to label the children of n f .
 
4
This states that it is possible to design an algorithm for solving the user-role reachability problem with a high complexity in terms of the number of roles occurring in the goal (recall the definitions from Sect. 5) and a polynomial complexity in terms of the overall input size when the number of roles in the goal is fixed.
 
Literatur
1.
Zurück zum Zitat 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 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
2.
Zurück zum Zitat 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) 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)
3.
Zurück zum Zitat Abdulla PA, Cerans K, Jonsson B, Tsay Y-K (1996) General decidability theorems for infinite-state systems. In: Proc of LICS, pp 313–321 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.
Zurück zum Zitat Armando A, Ranise S (2010) Automated symbolic analysis of ARBAC policies. In: 6th int workshop on security and trust management (STM) Armando A, Ranise S (2010) Automated symbolic analysis of ARBAC policies. In: 6th int workshop on security and trust management (STM)
5.
Zurück zum Zitat Crampton J (2002) Authorization and antichains. PhD thesis, Birkbeck, University of London, London, England Crampton J (2002) Authorization and antichains. PhD thesis, Birkbeck, University of London, London, England
6.
Zurück zum Zitat 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 CrossRef 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 CrossRef
7.
Zurück zum Zitat 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 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.
Zurück zum Zitat Dickson LE (1913) Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Am J Math 35(4):413–422 MATHCrossRef Dickson LE (1913) Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Am J Math 35(4):413–422 MATHCrossRef
9.
Zurück zum Zitat de Moura L (2011) Personal communication de Moura L (2011) Personal communication
10.
Zurück zum Zitat Enderton HB (1972) A mathematical introduction to logic. Academic Press, San Diego MATH Enderton HB (1972) A mathematical introduction to logic. Academic Press, San Diego MATH
11.
Zurück zum Zitat 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) 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)
12.
Zurück zum Zitat Fontaine P, Gribomont EP (2003) Decidability of invariant validation for parameterized systems. In: TACAS. LNCS, vol 2619. Springer, Berlin, pp 97–112 Fontaine P, Gribomont EP (2003) Decidability of invariant validation for parameterized systems. In: TACAS. LNCS, vol 2619. Springer, Berlin, pp 97–112
13.
Zurück zum Zitat 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 CrossRef 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 CrossRef
14.
Zurück zum Zitat Ghilardi S, Ranise S (2010) Backward reachability of array-based systems by smt solving: termination and invariant synthesis. LMCS 6(4):1–48 MathSciNet Ghilardi S, Ranise S (2010) Backward reachability of array-based systems by smt solving: termination and invariant synthesis. LMCS 6(4):1–48 MathSciNet
15.
Zurück zum Zitat Ghilardi S, Ranise S (2010) MCMT: a model checker modulo theories. In: Proc of IJCAR’10. LNCS, vol 6803 Ghilardi S, Ranise S (2010) MCMT: a model checker modulo theories. In: Proc of IJCAR’10. LNCS, vol 6803
17.
Zurück zum Zitat 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 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.
Zurück zum Zitat Kuhn DR, Coyne EJ, Weil TR (2010) Adding attributes to role based access control. IEEE Comput 43(6):79–81 CrossRef Kuhn DR, Coyne EJ, Weil TR (2010) Adding attributes to role based access control. IEEE Comput 43(6):79–81 CrossRef
19.
Zurück zum Zitat Lewis HR (1980) Complexity results for classes of quantificational formulas. J Comput Syst Sci 21(3):317–353 MATHCrossRef Lewis HR (1980) Complexity results for classes of quantificational formulas. J Comput Syst Sci 21(3):317–353 MATHCrossRef
20.
Zurück zum Zitat Li N, Mao Z (2007) Administration in role based access control. In: Proc ACM symp on information, computer, and communication security (ASIACCS) Li N, Mao Z (2007) Administration in role based access control. In: Proc ACM symp on information, computer, and communication security (ASIACCS)
21.
Zurück zum Zitat Li N, Tripunitara MV (2006) Security analysis in role-based access control. ACM Trans Inf Syst Secur (TISSEC) 9(4):391–420 CrossRef Li N, Tripunitara MV (2006) Security analysis in role-based access control. ACM Trans Inf Syst Secur (TISSEC) 9(4):391–420 CrossRef
22.
Zurück zum Zitat 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 CrossRef 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 CrossRef
23.
Zurück zum Zitat Navarro Pérez JA, Voronkov A (2008) Collection of papers dedicated to Harald Ganzinger’s memory, chapter planning with effectively propositional logic. Springer, Berlin Navarro Pérez JA, Voronkov A (2008) Collection of papers dedicated to Harald Ganzinger’s memory, chapter planning with effectively propositional logic. Springer, Berlin
25.
Zurück zum Zitat 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 CrossRef 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 CrossRef
26.
Zurück zum Zitat Sandhu R, Coyne E, Feinstein H, Youmann C (1996) Role-based access control models. IEEE Comput 2(29):38–47 CrossRef Sandhu R, Coyne E, Feinstein H, Youmann C (1996) Role-based access control models. IEEE Comput 2(29):38–47 CrossRef
28.
Zurück zum Zitat 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 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.
Zurück zum Zitat 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 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
32.
Zurück zum Zitat 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 MATHCrossRef 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 MATHCrossRef
33.
Zurück zum Zitat 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 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.
Zurück zum Zitat 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 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.
Zurück zum Zitat 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 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
36.
Zurück zum Zitat Sasturkar A, Yang P, Stoller SD, Ramakrishnan CR (2011) Policy analysis for administrative role based access control. Theor Comput Sci 412(44):6208–6234 MathSciNetMATHCrossRef Sasturkar A, Yang P, Stoller SD, Ramakrishnan CR (2011) Policy analysis for administrative role based access control. Theor Comput Sci 412(44):6208–6234 MathSciNetMATHCrossRef
Metadaten
Titel
Symbolic backward reachability with effectively propositional logic
Applications to security policy analysis
verfasst von
Silvio Ranise
Publikationsdatum
01.02.2013
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 1/2013
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-012-0157-1

Weitere Artikel der Ausgabe 1/2013

Formal Methods in System Design 1/2013 Zur Ausgabe