[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Verification and enforcement of access control policies

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Access control mechanisms protect critical resources of systems from unauthorized access. In a policy-based management approach, administrators define user privileges as rules that determine the conditions and the extent of users’ access rights. As rules become more complex, analytical skills are required to identify conflicts and interactions within the rules that comprise a system policy—especially when rules are stateful and depend on event histories. Without adequate tool support such an analysis is error-prone and expensive. In consequence, many policy specifications are inconsistent or conflicting that render the system insecure. The security of the system, however, does not only depend on the correct specification of the security policy, but in a large part also on the correct interpretation of those rules by the system’s enforcement mechanism.

In this paper, we show how policy rules can be formalized in Fusion Logic, a temporal logic for the specification of behavior of systems. A symbolic decision procedure for Fusion Logic based on Binary Decision Diagrams (BDDs) is provided and we introduce a novel technique for the construction of enforcement mechanisms of access control policy rules that uses a BDD encoded enforcement automaton based on input traces which reflect state changes in the system. We provide examples of verification of policy rules, such as absence of conflicts, and dynamic separation of duty and of the enforcement of policies using our prototype implementation (FLCheck) for which we detail the underlying theory.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4

Similar content being viewed by others

Notes

  1. For readability we use \(\operatorname {Aut}^{d}\) in the context of Policy, and \(\operatorname {Aut}\) in the context of the Enforcement Mechanism.

  2. http://www.tech.dmu.ac.uk/~cau/software/flcheck-1.0.tar.gz.

References

  1. Abadi M, Fournet C (2003) Access control based on execution history. In: 10th annual network and distributed system symposium (NDSS’03). The Internet Society, Reston, pp 1–15

    Google Scholar 

  2. Antimirov VM (1996) Partial derivatives of regular expressions and finite automaton constructions. Theor Comput Sci 155(2):291–319. doi:10.1016/0304-3975(95)00182-4

    Article  MathSciNet  MATH  Google Scholar 

  3. Bahrak B, Deshpande A, Whitaker M, Park JM (2010) Bresap: a policy reasoner for processing spectrum access policies represented by binary decision diagrams. In: 2010 IEEE symposium on new frontiers in dynamic spectrum, pp 1–12. doi:10.1109/DYSPAN.2010.5457867

    Chapter  Google Scholar 

  4. Bandara AK, Lupu EC, Sloman M (2007) Policy-based management. In: Burgess M, Bergstra J (eds) Handbook of network and system administration. Elsevier, Amsterdam

    Google Scholar 

  5. Bertino E, Bonatti PA, Ferrari E (2001) TRBAC: a temporal role-based access control model. ACM Trans Inf Syst Secur 4(3):191–233. doi:10.1145/501978.501979

    Article  Google Scholar 

  6. Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput 35(8):677–691. doi:10.1109/TC.1986.1676819

    Article  MATH  Google Scholar 

  7. Bryant RE (1992) Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3):293–318. doi:10.1145/136035.136043

    Article  Google Scholar 

  8. Brzozowski JA (1964) Derivatives of regular expressions. J ACM 11:481–494. doi:10.1145/321239.321249

    Article  MathSciNet  MATH  Google Scholar 

  9. Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142–170. doi:10.1016/0890-5401(92)90017-A

    Article  MathSciNet  MATH  Google Scholar 

  10. Chaochen Z, Hoare CAR, Ravn AP (1991) A calculus of durations. Inf Process Lett 40(5):269–276. doi:10.1016/0020-0190(91)90122-X

    Article  MathSciNet  MATH  Google Scholar 

  11. Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma E, Larsen KG (eds) CAV. Lecture notes in computer science, vol 2404. Springer, Berlin, pp 359–364

    Google Scholar 

  12. Cimatti A, Roveri M, Tonetta S (2008) Symbolic compilation of PSL. IEEE Trans Comput-Aided Des Integr Circuits Syst 27(10):1737–1750. doi:10.1109/TCAD.2008.2003303

    Article  Google Scholar 

  13. Clarke EM Jr, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge

    Google Scholar 

  14. Coudert O, Berthet C, Madre JC (1989) Verification of sequential machines using boolean functional vectors. In: Claesen L (ed) Proceedings of the IFIP international workshop on applied formal methods for correct VLSI design, Leuven, Belgium, pp 111–128

    Google Scholar 

  15. Coudert O, Berthet C, Madre JC (1989) Verification of synchronous sequential machines based on symbolic execution. In: Sifakis J (ed) Automatic verification methods for finite state systems, international workshop, Grenoble, France. LNCS, vol 407. Springer, Berlin, pp 365–373

    Chapter  Google Scholar 

  16. Coudert O, Berthet C, Madre JC (1990) A unified framework for the formal verification of sequential circuits. In: Proceedings of the IEEE international conference on computer aided design, pp 126–129

    Google Scholar 

  17. Damianou N, Dulay N, Lupu E, Sloman M (2001) The Ponder specification language. In: Workshop on policies for distributed systems and networks (Policy2001)

    Google Scholar 

  18. Duan Z, Tian C, Zhang L (2008) A decision procedure for propositional projection temporal logic with infinite models. Acta Inform 45:43–78. doi:10.1007/s00236-007-0062-z

    Article  MathSciNet  MATH  Google Scholar 

  19. Elgaard J, Klarlund N, Møller A (1998) MONA 1.x: new techniques for WS1S and WS2S. In: Proceedings of the 10th international conference on computer-aided verification, CAV ’98. LNCS, vol 1427. Springer, Berlin, pp 516–520

    Chapter  Google Scholar 

  20. Fisher M, Dixon C, Peim M (2001) Clausal temporal resolution. ACM Trans Comput Log 2(1):12–56. doi:10.1145/371282.371311

    Article  MathSciNet  Google Scholar 

  21. Gomez R, Bowman H (2004) PITL2MONA: implementing a decision procedure for propositional interval temporal logic. J Appl Non-Class Log 14(1–2):105–148. Issue on Interval temporal logics and duration calculi. V Goranko and A Montanari guest eds

    Article  MATH  Google Scholar 

  22. Harel D (1987) Statecharts: a visual formalism for complex systems. Sci Comput Program 8(3):231–274. doi:10.1016/0167-6423(87)90035-9

    Article  MathSciNet  MATH  Google Scholar 

  23. Harel D, Kozen D, Tiuryn J (2000) Dynamic logic. MIT Press, Cambridge

    MATH  Google Scholar 

  24. Holzmann GJ (1997) The model checker SPIN. IEEE Trans Softw Eng 23(5):279–295

    Article  MathSciNet  Google Scholar 

  25. Hu H, Ahn GJ, Kulkarni K (2011) Anomaly discovery and resolution in web access control policies. In: Proceedings of the 16th ACM symposium on access control models and technologies. SACMAT ’11. ACM, New York, pp 165–174. doi:10.1145/1998441.1998472

    Chapter  Google Scholar 

  26. IBM Cooperation (2003) Enterprise privacy authorisation language (EPAL) version 1.2. Submitted to the W3C. http://www.w3.org/Submission4/2003/SUBM-EPAL-20031110/

  27. IEEE (2005) IEEE standard for property specification language (PSL), std 1850-2005. Tech rep, IEEE. doi:10.1109/IEEESTD.2005.97780

  28. ISO/IEC (2006) ISO/IEC 10181-3:1996 information technology—open systems interconnection—security frameworks for open systems: access control framework. http://www.iso.org/iso/en/CatalogueDetailPage.CatalogueDetail?CSNUMBER=18199

  29. Jajodia S, Samarati P, Sapino ML, Subrahmanian VS (2001) Flexible support for multiple access control policies. ACM Trans Database Syst 26(2):214–260. doi:10.1145/383891.383894

    Article  MATH  Google Scholar 

  30. Janicke H, Cau A, Siewe F, Zedan H, Jones K (2006) A compositional event & time-based policy model. In: Proceedings of POLICY2006, London, Ontario, Canada. IEEE Computer Society, London, pp 173–182

    Google Scholar 

  31. Janicke H, Cau A, Siewe F, Zedan H (2007) Deriving enforcement mechanisms from policies. In: Proceedings of the 8th IEEE international workshop on policies for distributed systems (POLICY2007), pp 161–170

    Chapter  Google Scholar 

  32. Janicke H, Cau A, Siewe F, Zedan H (2012) Dynamic access control policies: specification and verification. Comput J. doi:10.1093/comjnl/bxs102

    Google Scholar 

  33. Joshi J, Bertino E, Ghafoor A (2005) An analysis of expressiveness and design issues for the generalized temporal role-based access control model. IEEE Trans Dependable Secure Comput 2(2):157–175. doi:10.1109/TDSC.2005.18

    Article  Google Scholar 

  34. Joshi J, Bertino E, Latif U, Ghafoor A (2005) A generalized temporal role-based access control model. IEEE Trans Knowl Data Eng 17(1):4–23. doi:10.1109/TKDE.2005.1

    Article  Google Scholar 

  35. Klarlund N, Møller A (2001) MONA version 1.4 user manual. Notes series NS-01-1, BRICS, Department of Computer Science, Aarhus University. Available from http://www.brics.dk/mona/. Revision of BRICS NS-98-3

  36. Kolovski V (2008) Logic-based framework for web access control policies. PhD thesis, Computer Science Department of University of Maryland, College Park

  37. Kono S (1995) A combination of clausal and non-clausal temporal logic programs. In: Fisher M, Owens R (eds) Executable modal and temporal logics. Lecture notes in artificial intelligence, Cambery, France, vol 897. Springer, Berlin, pp 40–57

    Chapter  Google Scholar 

  38. Kozen D (1992) Private commuication

  39. Kropf T (1999) Introduction to formal hardware verification: methods and tools for designing correct circuits and systems, 1st edn. Springer, New York

    Book  Google Scholar 

  40. Lamport L (1994) The temporal logic of actions. ACM Trans Program Lang Syst 16(3):872–923. doi:10.1145/177492.177726

    Article  Google Scholar 

  41. Lampson BW (1974) Protection. Oper Syst Rev 8(1):18–24. doi:10.1145/775265.775268

    Article  Google Scholar 

  42. Leucker M, Sánchez C (2010) Regular linear-time temporal logic. In: Markey N, Wijsen J (eds) TIME. IEEE Computer Society, Los Alamitos, pp 3–5. doi:10.1109/TIME.2010.29

    Google Scholar 

  43. Lupu EC, Sloman M (1999) Conflicts in policy-based distributed systems management. IEEE Trans Softw Eng 25(6):852–869. doi:10.1109/32.824414

    Article  Google Scholar 

  44. Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: specification. Springer, New York

    Book  Google Scholar 

  45. Masood A, Ghafoor A, Mathur AP (2010) Conformance testing of temporal role-based access control systems. IEEE Trans Dependable Secure Comput 7(2):144–158. doi:10.1109/TDSC.2008.41

    Article  Google Scholar 

  46. McMillan KL (1993) Symbolic model checking. Kluwer Academic, Norwell

    Book  MATH  Google Scholar 

  47. Moszkowski B (1983) Reasoning about digital circuits. PhD thesis, Department of Computer Science, Stanford University, technical report STAN-CS-83-970

  48. Moszkowski B (1985) A temporal logic for multilevel reasoning about hardware. IEEE Trans Comput 18(2):10–19

    Google Scholar 

  49. Moszkowski B (2004) A hierarchical completeness proof for propositional interval temporal logic with finite time. J Appl Non-Class Log 14(1–2):55–104. Special issue on Interval temporal logics and duration calculi

    Article  MATH  Google Scholar 

  50. Moszkowski B (2005) A hierarchical analysis of propositional temporal logic based on intervals. In: Artemov S, Barringer H, d’Avila Garcez AS, Lamb LC, Woods J (eds) We will show them: essays in honour of Dov Gabbay, vol 2. King’s College, London, pp 371–440

    Google Scholar 

  51. Moszkowski B (2011) Compositional reasoning using intervals and time reversal. In: International syposium on temporal representation and reasoning, pp 107–114. doi:10.1109/TIME.2011.25

    Google Scholar 

  52. OASIS (2005) eXtensible access control markup language (XACML) version 2.0. http://www.oasis-open.org/committees/tc_home.php?wg_abbrev=xacml#XACML20

  53. Pandya PK (2001) Specifying and deciding quantified discrete-time duration calculus formulae using DCVALID. In: Pattersson P, Yovine S (eds) Proceedings of workshop on real-time tools (RT-TOOL’2001). Affiliated with CONCUR 2001, Uppsala University, Sweden, technical report 2001-14, full version available as technical report TCS-00-PKP-1, Tata Institute of Fundamental Research, 2000

    Google Scholar 

  54. Park J, Sandhu RS (2004) The UCON ABC usage control model. ACM Trans Inf Syst Secur 7(1):128–174. doi:10.1145/984334.984339

    Article  Google Scholar 

  55. Park J, Zhang X, Sandhu RS (2004) Attribute mutability in usage control. In: Farkas C, Samarati P (eds) Proceedings of IFIP TC11/WG 11.3 eighteenth annual conference on data and applications security, Sitges, Catalonia, Spain. Kluwer, Dordrecht, pp 15–29

    Google Scholar 

  56. Prior AN (1967) Past, present and future. Oxford University Press, Oxford

    Book  MATH  Google Scholar 

  57. Rao P, Lin D, Bertino E, Li N, Lobo J (2009) An algebra for fine-grained integration of xacml policies. In: Proceedings of the 14th ACM symposium on access control models and technologies, SACMAT ’09. ACM, New York, pp 63–72. doi:10.1145/1542207.1542218

    Chapter  Google Scholar 

  58. Sandhu R, Park J (2003) The UCON ABC usage control model. In: Proceeding of the second international workshop on mathematical method, models and architectures for computer networks security

    Google Scholar 

  59. Schaad A, Lotz V, Sohr K (2006) A model-checking approach to analysing organisational controls in a loan origination process. In: Ferraiolo DF, Ray I (eds) SACMAT. ACM, New York, pp 139–149. doi:10.1145/1133058.1133079

    Google Scholar 

  60. Schneider FB (2000) Enforceable security policies. ACM Trans Inf Syst Secur 3(1):30–50. doi:10.1145/353323.353382

    Article  Google Scholar 

  61. Siewe F, Cau A, Zedan H (2003) A compositional framework for access control policies enforcement. In: Proceedings of the ACM workshop on formal methods in security engineering: from specifications to code

    Google Scholar 

  62. Sloman M (1994) Policy driven management for distributed systems. J Netw Syst Manag 2:333–360

    Article  Google Scholar 

  63. Somenzi F (1998) CUDD: Colorado University decision diagram package. University of Colorado at Boulder. http://vlsi.colorado.edu/~fabio/CUDD/

  64. Woo TYC, Lam SS (1993) Authorization in distributed systems: a new approach. J Comput Secur 2(2(3):107–136

    Google Scholar 

  65. Zhang X, Park J, Parisi-Presicce F, Sandhu R (2004) A logical specification for usage control. In: SACMAT ’04: proceedings of the ninth ACM symposium on access control models and technologies. ACM, New York, pp 1–10. doi:10.1145/990036.990038

    Chapter  Google Scholar 

  66. Zhang X, Parisi-Presicce F, Sandhu RS, Park J (2005) Formal model and policy specification of usage control. ACM Trans Inf Syst Secur 8(4):351–387. doi:10.1145/1108906.1108908

    Article  Google Scholar 

  67. Zhang X, Sandhu RS, Parisi-Presicce F (2006) Safety analysis of usage control authorization models. In: Lin FC, Lee DT, Lin BS, Shieh S, Jajodia S (eds) ASIACCS. ACM, New York, pp 243–254. doi:10.1145/1128817.1128853

    Chapter  Google Scholar 

  68. Zhang X, Seifert JP, Sandhu RS (2008) Security enforcement model for distributed usage control. In: Singhal M, Serugendo GDM, Tsai JJP, Lee W, Römer K, Tseng YC, Hsiao HCW (eds) SUTC. IEEE Computer Society, Los Alamitos, pp 10–18. doi:10.1109/SUTC.2008.79

    Google Scholar 

Download references

Acknowledgements

The authors would like to thank the anonymous reviewers for their comments that were very helpful for shaping the manuscript.

Author information

Authors and Affiliations

  1. Software Technology Research Laboratory, De Montfort University, LE1 9BH, Leicester, UK

    Antonio Cau, Helge Janicke & Ben Moszkowski

Authors
  1. Antonio Cau
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Helge Janicke
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ben Moszkowski
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Antonio Cau.

Appendix: Proofs

Appendix: Proofs

Lemma 3 Let R be a right fusion logic formula and dep(R) be the dependent variables introduced by and (k=0,1). Then the formula below is valid:

Proof

The proof is done via structural induction on R and by employing the reduction rules in Table 2. We also make use of some existing Fusion Logic theorems.

  • Case R=W: is equal to, using the reduction rule and dep(W)=∅, □ r true which is equal to true.

  • Case R=¬X: is equal to, using the reduction rule , . Because dep(¬X)=dep(X), this is equal to . Using the induction hypothesis, this holds.

  • Case R=X 1∨X 2: is equal to, using the reduction rule , is equal to, as dep(X 1∨X 2)=dep(X 1)∪dep(X 2) and dep(X 1)∩dep(X 2)=∅, . Using the induction hypothesis twice, this holds.

  • Case R=〈test(W)〉X: is equal to, using the reduction rule , . This is equal to, as dep(〈test(W)〉X)=dep(X), . Using the induction hypothesis, this holds.

  • Case R=〈step(T)〉X: We first consider k=0. is equal to, using the reduction rule , . This is equal to, as dep(〈test(W)〉X)={r 〈step(T)〉X }∪dep(X), . This is equal to, using the induction hypothesis, . Substitute for r 〈step(T)〉X the value will give which holds.

    We now consider the case k=1. is equal to, using the reduction rule , . This is equal to, as dep(〈test(W)〉X)=dep(X), . Using the induction hypothesis, this holds.

  • Case R=〈E 1∨E 2〉X: is equal to, using the reduction rule and dep(〈E 1∨E 2〉X)=dep(〈E 1〉X)∪dep(〈E 2〉X) and using the reduction rule , . Using the induction hypothesis in a similar way as the case R=X 1∨X 2, we get the desired result.

  • Case R=〈E 1;E 2〉X: is equal to, using the reduction rule , let X 1=〈E 2〉X and dep(〈E 1;E 2〉X)=dep(〈E 1〉X 1), . Using the induction hypothesis, this holds.

  • Case R=〈E ∗〉X: is equal to, using the reduction rule and let X 1 denote \(X \mathrel {\scriptstyle \vee }\langle c(E) \rangle {r_{\scriptsize \langle E^{*}\rangle {X}}}\), . Using induction hypothesis and \(dep(\langle E ^{*}\rangle {X} ) = \{ r_{\scriptsize \langle E ^{*}\rangle {X}} \} \cup dep(X)\), we get . Substitute for \(r_{\scriptsize \langle E ^{*}\rangle {X}}\) the value , will give the desired result.

 □

Lemma 4 Let R be a right fusion logic formula. Then the next implication is valid:

Proof

The proof is done via structural induction on R and by employing the reduction rules in Table 2. We also make use of some existing Fusion Logic theorems.

  • Case R=W: is equal to, using the reduction rules and , □ r true⊃W≡W and this holds.

  • Case R=¬X: is equal to, using the reduction rule and , which is equivalent to . Use the induction hypothesis to get the desired result.

  • Case R=X 1∨X 2: is equal to, using the reduction rules and , . Using the induction hypothesis and , and the theorem , will give the desired result.

  • Case R=〈test(W)〉X: is equal to, using the reduction rules and , . Using the induction hypothesis and the theorem 〈test(W)〉X≡(W∧X), gives the desired result.

  • Case R=〈step(T)〉X: We first consider k=0. is equal to, using the reduction rules and , . We know that is equivalent to . Using the induction hypothesis we get . Using the theorem , gives us the desired result.

    We now consider the case k=1. is equal to, using the reduction rules and , . Using the induction hypothesis and the theorem , gives us the desired result.

  • Case R=〈E 1∨E 2〉X: is equal to, using the reduction rules , , and , . Using the induction hypothesis and plus the theorem and 〈E 1∨E 2〉X≡〈E 1〉X∨〈E 2〉X, gives us the desired result.

  • Case R=〈E 1;E 2〉X: is equal to, using the reduction rules and , . Using the induction hypothesis and and the theorem 〈E 1;E 2〉X≡〈E 1〉〈E 2〉X, gives us the desired result.

  • Case R=〈E ∗〉X: is equal to, using the reduction rules and and let X 1 denote \(X\,{\mathrel {\scriptstyle \vee }}\, \langle c(E) \rangle {r_{\scriptsize \langle E^{*}\rangle {X}}}\), . Using the induction hypothesis and the theorem and 〈E ∗〉X≡X∨〈c(E)〉〈E ∗〉X, gives us the desired result.

 □

Rights and permissions

Reprints and permissions

About this article

Cite this article

Cau, A., Janicke, H. & Moszkowski, B. Verification and enforcement of access control policies. Form Methods Syst Des 43, 450–492 (2013). https://doi.org/10.1007/s10703-013-0187-3

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-013-0187-3

Keywords

Search

Navigation