Abstract
Managing access control policies in modern computer systems can be challenging and error-prone. Combining multiple disparate access policies can introduce unintended consequences. In this paper, we present a formal model for specifying access to resources, a model that encompasses the semantics of the xacml access control language. From this model we define several ordering relations on access control policies that can be used to automatically verify properties of the policies. We present a tool for automatically verifying these properties by translating these ordering relations to Boolean satisfiability problems and then applying a sat solver. Our experimental results demonstrate that automated verification of xacml policies is feasible using this approach.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abad-Peiro, J.L., Debar, H., Schweinberger, T., Trommler, P.: PLAS—Policy language for authorizations. Technical Report RZ 3126, IBM Research Division (1999)
Abadi M., Burrows M., Lampson B., Plotkin G.: A calculus for access control in distributed systems. ACM Trans. Programm. Lang. Syst. 15(4), 706–734 (1993)
Bertino E., Bettini C., Ferrari E., Samarati P.: An access control model supporting periodicity constraints and temporal reasoning. ACM Trans. Database Syst. 23(3), 231–285 (1998)
Bonatti, P., Damiani, E., De Capitani di Vimercati, S., Samarati, P.: An access control model for data archives. In: Proceedings of the 16th International Conference on Information Security: Trusted Information, pp. 261–276. Kluwer International Federation For Information Processing Series Paris, France (2001)
Bonatti P., De Capitani di Vimercati S., Samarati P.: An algebra for composing access control policies. ACM Trans. Inf. Syst. Secur. 5(1), 1–35 (2002)
Brace, K.S., Rudellv, R.L., Bryant, R.E.: Efficient implementation of a bdd package. In: Proceedings of the 27th ACM/IEEE Design Automation Conference, pp. 40–45 (1990)
Damiani, E., De Capitani di Vimercati, S., Fernández-Medina, E., Samarati, P.: Access control of SVG documents. In: Proceedings of DBSec 2002, pp. 219–230 (2002)
Damiani E., De Capitani di Vimercati S., Paraboschi S., Samarati P.: Design and implementation of an access control processor for XML documents. Comput. Netw. 33(1–6), 59–75 (2000)
Damiani E., De Capitani di Vimercati S., Paraboschi S., Samarati P.: A fine-grained access control system for XML documents. ACM Trans. Inf. Syst. Secur. 5(2), 169–202 (2002)
Damiani E., Samarati S.P., De Capitani di Vimercati S., Paraboschi S.: Controlling access to XML documents. IEEE Internet Comput. 5(6), 18–28 (2001)
De Capitani di Vimercati, S., Samarati, P.: Access control in federated systems. In: Proceedings of the 1996 Workshop on New Security Paradigms, pp. 87–99. ACM Press, Lake Arrowhead (1996)
Fisler, K., Krishnamurthi, S., Meyerovich, L.A., Tschantz, M.C.: Verification and change-impact analysis of access-control policies. In: Proceedings of the 27th International Conference on Software Engineering, pp. 196–205, St. Louis, Missouri (2005)
Heckman, M., Levitt, K.N.: Applying the composition principle to verify a hierarchy of security servers. In: HICSS (3), pp. 338–347 (1998)
Hughes, G., Bultan, T.: Automated verification of access control policies. Technical Report 2004-22. Department of Computer Science, University of California, Santa Barbara (2004)
Hughes, G., Bultan, T.: Automated verification of XACML policies using a SAT solver. In: Proceedings of the Workshop on Web Quality, Verification and Validation (WQVV ’07) (2007)
Jackson, D.: Automating first-order relational logic. In: Proceedings of ACM SIGSOFT Conf. Foundations of Software Engineering (2000)
Jackson, D.: Software Abstractions: Logic, Language and Analysis. MIT Press, Cambridge (2006). http://softwareabstractions.org/
Jackson D., Damon C.A.: Elements of style: analyzing a software design feature with a counterexample detector. IEEE. Trans. Softw. Eng. 22(7), 484–495 (1996)
Jackson, D., Schechter, I., Shlyakhter, I.: Alcoa: the Alloy constraint analyzer. In: Proceedings of International Conference on Software Engineering. IEEE, Limerick (2000)
Jajodia S., Samarati P., Sapino M.L., Subrahmanian V.S.: Flexible support for multiple access control policies. ACM Trans. Database Syst. 26(2), 214–260 (2001)
Jajodia, S., Samarati, P., Subrahmanian, V.S.: A logical language for expressing authorizations. In: Proceedings of the 1997 IEEE Symposium on Security and Privacy, pp. 31–42. IEEE Press, Oakland (1997)
Jajodia, S., Samarati, P., Subrahmanian, V.S., Bertino, E.: A unified framework for enforcing multiple access control policies. In: SIGMOD’97, pp. 474–485. Tucson, AZ (1997)
Krishnamurthi, S.: The Continue server. In: Symposium on the Practical Aspects of Declarative Languages (2003)
Marinov, D., Andoni, A., Danilinc, D., Khurshid, S., Rinard, M.: An evaluation of exhaustive testing for data structures. Technical Report MIT-LCS-TR-921, MIT CSAIL (2003)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: 39th Design Automation Conference (DAC 2001), Las Vegas (2001)
Naumovich, G.: A conservative algorithm for computing the flow of permissions in Java programs. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA ’02), pp. 33–43 (2002)
Plaisted D.A., Greenbaum S.: A structure-preserving clause form translation. J. Symb. Comput. 2, 293–304 (1986)
Samarati, P., De Capitani di Vimercati, S.: Foundations of Security Analysis and Design. Chap. 3, pp. 137–196. Springer, Heidelberg (2001)
Sandhu R., Samarati P.: Authentication, access control, and audit. ACM Comput. Surv. 28(1), 241–243 (1996)
Sandhu R.S.: Lattice-based access control models. IEEE Comput. 26(11), 9–19 (1993)
Sandhu R.S., Coyne E.J., Feinstein H.L., Youman C.E.: Role-based access control models. IEEE Comput. 29(2), 38–47 (1996)
Sandhu R.S., Samarati P.: Access control: principles and practice. IEEE Commun. Mag. 32(9), 40–48 (1994)
Schaad, A., Moffet, J.: A lightweight approach to specification and analysis of role-based access control extensions. In: 7th ACM Symposium on Access Control Models and Technologies (SACMAT 2002) (2002)
eXtensible Access Control Markup Language (XACML) Version 1.0. OASIS Standard (2003). http://www.oasis-open.org/committees/tc_home.php?wg_abbrev=xacml
Extensible markup language (XML) 1.0, 2nd edn. W3C (2000). http://www.w3.org/TR/REC-xml
XML Schema part 2: Datatypes. W3C Recommendation (2001). http://www.w3.org/TR/xmlschema-2/
Zao, J., Wee, H., Chu, J., Jackson, D.: RBAC schema verification using lightweight formal model and constraint analysis. In: Proceedings of the Eighth ACM Symposium on Access Control Models and Technologies (2003)
Author information
Authors and Affiliations
Corresponding author
Additional information
This work is supported by NSF grants CCF-0614002 and CCF-0716095.
Rights and permissions
About this article
Cite this article
Hughes, G., Bultan, T. Automated verification of access control policies using a SAT solver. Int J Softw Tools Technol Transfer 10, 503–520 (2008). https://doi.org/10.1007/s10009-008-0087-9
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-008-0087-9