Analysis of access control policy updates through narrowing

ABSTRACT

Administration of access control policies is a difficult task, especially in large organizations. We consider the problem of detecting whether administrative actions can yield in policies where some security goals are compromised. In particular, we are interested in problems generated by modifications --- such as adding/deleting elements to/from the set of possible users or permissions --- of policies specified as term-rewrite systems. We propose to use rewriting techniques to compare the behaviors of the modified version and the original version of the policy. More precisely, we use narrowing to compute counter-examples to the equivalence of rewrite-based policies. We prove that our technique provides a sound and complete way to recursively enumerate the set of counter-examples, even when this set is not finite, or when a mistake of the administrator makes one or both systems non-terminating.

References

1. S. Antoy. Definitional Trees. In In Proc. of the 3rd International Conference on Algebraic and Logic Programming, pages 143--157. Springer LNCS, 1992.
2. S. Antoy, R. Echahed, and M. Hanus. A Needed Narrowing Strategy. In Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 268--279. ACM, 1994. 00415.
3. S. Antoy, B. Massey, M. Hanus, and F. Steiner. An implementation of narrowing strategies. In Proceedings of the 3rd ACM SIGPLAN international conference on Principles and practice of declarative programming, pages 207--217. ACM, 2001.
4. A. Armando and S. Ranise. Scalable automated symbolic analysis of administrative role-based access control policies by smt solving. J. Comput. Secur., 20(4):309--352, July 2012.
5. S. Barker. The next 700 access control models or a unifying meta-model? In SACMAT 2009, 14th ACM Symposium on Access Control Models and Technologies, Stresa, Italy, June 3-5, 2009, Proceedings, pages 187--196, 2009.
6. S. Barker and M. Fernández. Term rewriting for access control. In Data and Applications Security. Proceedings of DBSec'2006, Lecture Notes in Computer Science. Springer-Verlag, 2006.
7. G. Barthe, G. Dufay, M. Huisman, and S. M. de Sousa. Jakarta: a toolset to reason about the JavaCard platform. In Proceedings of e-SMART'01, number 2140 in Lecture Notes in Computer Science. Springer-Verlag, 2002.
8. C. Bertolissi and M. Fernández. A rewriting framework for the composition of access control policies. In Proceedings of the 10th ACM-SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'08), Valencia, 2008. ACM Press, 2008.
9. C. Bertolissi and M. Fernández. A metamodel of access control for distributed environments: Applications and properties. Inf. Comput., 238:187--207, 2014.
10. C. Bertolissi, M. Fernández, and S. Barker. Dynamic Event-based Access Control as Term Rewriting. In In Proc. DBSEC 2007, LNCS. Springer, 2007.
11. P. A. Bonatti and P. Samarati. Logics for authorization and security. In J. Chomicki, R. van der Meyden, and G. Saake, editors, Logics for Emerging Applications of Databases, pages 277--323. Springer, 2003.
12. B. Braßel, M. Hanus, B. Peemöller, and F. Reck. KiCS2: A new compiler from Curry to Haskell. In International Workshop on Functional and Constraint Logic Programming, pages 1--18. Springer, 2011.
13. N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pages 243--320. 1990. 00010.
14. D. J. Dougherty, C. Kirchner, H. Kirchner, and A. S. de Oliveira. Modular access control via strategic rewriting. In Proceedings of 12th European Symposium On Research In Computer Security, ESORICS, pages 578--593, 2007.
15. R. Echahed and F. Prost. Security policy in a declarative style. In Proc. 7th ACM-SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'05). ACM Press, 2005.
16. S. Escobar. Refining Weakly Outermost-Needed Rewriting and Narrowing. In Proc. of 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP'03, pages 113--123. ACM Press, 2003. 00021.
17. S. Escobar, C. Meadows, and J. Meseguer. A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties. Theor. Comput. Sci., 367:162--202, November 2006.
18. D. F. Ferraiolo, R. Sandhu, S. Gavrila, D. R. Kuhn, and R. Chandramouli. Proposed NIST Standard for Role-Based Access Control. 2001.
19. A. L. Ferrara, P. Madhusudan, and G. Parlato. Policy analysis for self-administrated role-based access control. In Tools and Algorithms for the Construction and Analysis of Systems, pages 432--447. Springer Berlin Heidelberg, 2013.
20. M. Hanus. Functional logic programming: From theory to Curry. Technical report, Citeseer, 2005.
21. M. A. Harrison, W. L. Ruzzo, and J. D. Ullman. Protection in operating systems. Commun. ACM, 19(8):461--471, 1976.
22. G. Huet and J.-J. Lévy. Computations in orthogonal rewriting systems, I and II. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 395--443 and 415--443. The MIT Press, Cambridge, MA, 1992.
23. J.-M. Hullot. Canonical forms and unification. In G. Goos, J. Hartmanis, W. Brauer, P. Brinch Hansen, D. Gries, C. Moler, G. Seegmüller, J. Stoer, N. Wirth, W. Bibel, and R. Kowalski, editors, 5th Conference on Automated Deduction Les Arcs, France, July 8-11, 1980, volume 87, pages 318--334. Springer Berlin Heidelberg, Berlin, Heidelberg, 1980.
24. R. Jagadeesan and V. Saraswat. Timed Constraint Programming: A Declarative Approach to Usage Control. In Proc. 7th ACM-SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'05). ACM Press, 2005.
25. S. Jha, N. Li, M. Tripunitara, Q. Wang, and W. Winsborough. Towards formal verification of role-based access control policies. IEEE Transactions on Dependable and Secure Computing, 5(4):242--255, 2008.
26. C. Kirchner, H. Kirchner, and A. S. de Oliveira. Analysis of Rewrite-Based Access Control Policies. Electronic Notes in Theoretical Computer Science, 234:55--75, Mar. 2009.
27. J. W. Klop. Term Rewriting Systems. In S. Abramsky, D. Gabbay, and T. Maibaurn, editors, Handbook of Logic in Computer Science, pages 1--116. Oxford University Press, 1992.
28. J. W. Klop and A. Middeldorp. Sequentiality in Orthogonal Term Rewriting Systems. Journal of Symbolic Computation, 12:161--195, 1991.
29. M. Koch, L. Mancini, and F. Parisi-Presicce. A graph based formalism for RBAC. In Proc. of SACMAT 2004, 9th ACM Symposium on Access Control Models and Technologies, New York, USA, 2004, pages 129--187, 2004.
30. N. Li and M. V. Tripunitara. Security analysis in role-based access control. ACM Transactions on Information and System Security (TISSEC), 9(4):391--420, 2006.
31. A. Lockman and N. Minsky. Unidirectional transport of rights and take- grant control. IEEE Transactions on Software Engineering, SE-8:597--604, November 1982.
32. W. Lux and H. Kuchen. An Efficient Abstract Machine for Curry. In K. Beiersdörfer, G. Engels, and W. Schäfer, editors, Informatik '99 --- Informatik überwindet Grenzen, 29. Jahrestagung der Gesellschaft für Informatik, Paderborn, 5-9. Oktober 1999, pages 390--399. Springer Verlag, 1999.
33. J. Meseguer and P. Thati. Symbolic Reachability Analysis Using Narrowing and Its Application to Verification of Cryptographic Protocols. Higher Order Symbol. Comput., 20(1-2):123--160, June 2007.
34. A. Middeldorp and E. Hamoen. Completeness Results for Basic Narrowing. Applicable Algebra in Engineering, Communication and Computing, 5(3-4):213--253, 1994. 00138.
35. R. S. Sandhu. The schematic protection model: Its definition and analysis for acyclic attenuating schemes. J. ACM, 35(2):404--432, 1988.
36. R. S. Sandhu. Lattice-based access control models. IEEE Computer, 26(11):9--19, Nov. 1993.
37. R. S. Sandhu and V. Bhamidipati. Role-based administration of user-role assignment: The ura97 model and its oracle implementation. Journal Of Computer Security, 7:317--342, 1999.
38. R. S. Sandhu, E. J. Coyne, H. L. Feinstein, and C. E. Youman. Role-based access control models. Computer, 29(2):38--47, 1996.
39. A. Santana de Oliveira. Réécriture et Modularité pour les Politiques de Sécurité. PhD thesis, Université Henri Poincaré, Nancy, France, 2008.
40. A. Sasturkar, P. Yang, S. D. Stoller, and C. Ramakrishnan. Policy analysis for administrative role based access control. In Computer Security Foundations Workshop, 2006. 19th IEEE, pages 13--pp. IEEE, 2006.
41. S. D. Stoller, P. Yang, C. R. Ramakrishnan, and M. I. Gofman. Efficient policy analysis for administrative role based access control. In Proceedings of the 14th ACM conference on Computer and communications security, pages 445--455. ACM, 2007.
42. L. Viganò. Automated security protocol analysis with the AVISPA tool. In Proc. of MFPS'05, volume 155 of ENTCS, pages 61--86. Elsevier, 2005.
43. L. Wang, D. Wijesekera, and S. Jajodia. A logic-based framework for attribute based access control. In Proceedings of the 2004 ACM Workshop on Formal Methods in Security Engineering, FMSE '04, pages 45--55. ACM, 2004.

Index Terms

• Security and privacy

  • Security services

    • Access control

  • Systems security

    • Operating systems security