Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Formal Methods in System Design
Published in: Formal Methods in System Design 1/2013

01-02-2013

Symbolic backward reachability with effectively propositional logic

Applications to security policy analysis

Author: Silvio Ranise

Published in: Formal Methods in System Design | Issue 1/2013

Log in

Activate our intelligent search to find suitable subject content or patents.

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.
previous article Efficiently solving quantified bit-vector formulas
next article SMT-based scenario verification for hybrid systems

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
Footnotes
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=A∧y=Em)∨(x=B∧y=M)∨(x=C∧y=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.
 
Literature
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
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)
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
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 CrossRef
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 MATHCrossRef
9.
10.
Enderton HB (1972) A mathematical introduction to logic. Academic Press, San Diego MATH
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)
12.
Fontaine P, Gribomont EP (2003) Decidability of invariant validation for parameterized systems. In: TACAS. LNCS, vol 2619. Springer, Berlin, pp 97–112
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 CrossRef
14.
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.
Ghilardi S, Ranise S (2010) MCMT: a model checker modulo theories. In: Proc of IJCAR’10. LNCS, vol 6803
16.
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 CrossRef
19.
Lewis HR (1980) Complexity results for classes of quantificational formulas. J Comput Syst Sci 21(3):317–353 MATHCrossRef
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 CrossRef
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 CrossRef
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.
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 CrossRef
26.
Sandhu R, Coyne E, Feinstein H, Youmann C (1996) Role-based access control models. IEEE Comput 2(29):38–47 CrossRef
27.
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.
31.
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 MATHCrossRef
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
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 MathSciNetMATHCrossRef
37.
38.
Metadata
Title
Symbolic backward reachability with effectively propositional logic
Applications to security policy analysis
Author
Silvio Ranise
Publication date
01-02-2013
Publisher
Springer US
Published in
Formal Methods in System Design / Issue 1/2013
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-012-0157-1

Other articles of this Issue 1/2013

Formal Methods in System Design 1/2013 Go to the issue

OriginalPaper

SMT proof checking using a logical framework

EditorialNotes

Preface to the special issue “SI: Satisfiability Modulo Theories”

OriginalPaper

SMT-based scenario verification for hybrid systems

OriginalPaper

Efficiently solving quantified bit-vector formulas

OriginalPaper

Being careful about theory combination

Premium Partner

    Image Credits