Konstantine Arkoudas
Skip Abstract Section
Skip Supplemental Material SectionAbstract
We introduce a new methodology for formulating, analyzing, and applying access-control policies. Policies are expressed as formal theories in the SMT (satisfiability-modulo-theories) subset of typed first-order logic, and represented in a programmable logical framework, with each theory extending a core ontology of access control. We reduce both request evaluation and policy analysis to SMT solving, and provide experimental results demonstrating the practicality of these reductions. We also introduce a class of canonical requests and prove that such requests can be evaluated in linear time. In many application domains, access requests are either naturally canonical or can easily be put into canonical form. The resulting policy framework is more expressive than XACML and languages in the Datalog family, without compromising efficiency. Using the computational logic facilities of the framework, a wide range of sophisticated policy analyses (including consistency, coverage, observational equivalence, and change impact) receive succinct formulations whose correctness can be straightforwardly verified. The use of SMT solving allows us to efficiently analyze policies with complicated numeric (integer and real) constraints, a weak point of previous policy analysis systems. Further, by leveraging the programmability of the underlying logical framework, our system provides exceptionally flexible ways of resolving conflicts and composing policies. Specifically, we show that our system subsumes FIA (Fine-grained Integration Algebra), an algebra recently developed for the purpose of integrating complex policies.
Supplemental Material
Available for Download
pdf
a17-arkoudas_appendix.pdf (21.2 KB)
The proof is given in an electronic appendix, available online in the ACM Digital Library.
- Abadi, M., Burrows, M., Lampson, B. W., and Plotkin, G. D. 1993. A calculus for access control in distributed systems. ACM Trans. Program. Lang. Syst. 15, 4, 706--734. Google Scholar
Digital Library
- Agrawal, D., Giles, J., Lee, K., and Lobo, J. 2005. Policy ratification. In Proceedings of the 6th IEEE International Conference on Policies for Distributed Systems and Networks (POLICY’05). 223--232. Google ScholarDigital Library
- Alberti, F., Armando, A., and Ranise, S. 2011. Efficient symbolic automated analysis of administrative attribute-based rbac-policies. In Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security (ASIACCS’11). ACM Press, New York, 165--175. Google ScholarDigital Library
- Anderson, R. J. 2008. Security Engineering 2nd Ed. Wiley.Google Scholar
- Antoniou, G., Baldoni, M., Bonatti, P. A., Nejdl, W., and Olmedilla, D. 2007. Rule-based policy specification. In Secure Data Management in Decentralized Systems, T. Yu and S. Jajodia Eds., Advances in Information Security Series, vol. 33, Springer, 169--216.Google Scholar
- Arkoudas, K. 2004. Athena. http://proofcentral.org/athena/.Google Scholar
- Arkoudas, K., Chadha, R., and Chiang, J. C. 2011a. An application of formal methods to cognitive radios. In Proceedings of the Design and Implementation of Formal Tools and Systems, a Workshop of Formal Methods in Computer Aided Design (DIFTS/FMCAD’11). 3--13.Google Scholar
- Arkoudas, K., Chadha, R., and Chiang, J. C. 2011b. An efficient policy engine for dynamic spectrum access. In Proceedings of the 4th International Conference on Cognitive Radios (CogArt’11).Google Scholar
- Bahrak, B., Deshpande, A. A., Whitaker, M., and Park, J. M. 2010. BRESAP: A policy reasoner for processing spectrum access policies represented by binary decision diagrams. In Proceedings of the IEEE Symposium on New Frontiers in Dynamic Spectrum. 1--12.Google Scholar
- Bandara, A. K., Lupu, E. C., and Russo, A. 2003. Using event calculus to formalise policy specification and analysis. In Proceedings of the 4th IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY’03). IEEE Computer Society, 26--39. Google ScholarDigital Library
- Becker, M., Fournet, C., and Gordon, A. 2007. Design and semantics of a decentralized authorization language. In Proceedings of the 20th IEEE Computer Security Foundations Symposium. IEEE Computer Society, 3--15. Google ScholarDigital Library
- Becker, M. Y. and Sewell, P. 2004. Cassandra: Distributed access control policies with tunable expressiveness. In Proceedings of the 5th IEEE International Workshop on Policies for Distributed Systems and Networks. 159--168. Google ScholarDigital Library
- Bertino, E., Catania, B., Ferrari, E., and Perlasca, P. 2003. A logical framework for reasoning about access control models. ACM Trans. Inf. Syst. Secur. 6, 71--127. Google ScholarDigital Library
- Bonatti, P., di Vimercati, S. D. C., and Samarati, P. 2002. An algebra for composing access control policies. ACM Trans. Inf. Syst. Secur. 5, 1--35. Google ScholarDigital Library
- Bonatti, P. A., Olmedilla, D., and Peer, J. 2006. Advanced policy queries. In Proceedings of the 17th European Conference on Artificial Intelligence. IOS Press, 200--204. Google ScholarDigital Library
- Bruns, G. and Huth, M. 2011. Access control via belnap logic: Intuitive, expressive, and analyzable policy composition. ACM Trans. Inf. Syst. Secur. 14, 1, 9:1--9:27. Google ScholarDigital Library
- Bryans, J. 2005. Reasoning about xacml policies using csp. In Proceedings of the Workshop on Secure Web Services (SWS’05). ACM Press, New York, 28--35. Google ScholarDigital Library
- Chadha, R. and Kant, L. 2007. Policy-Driven Mobile Ad Hoc Network Management. Wiley/IEEE Press. Google ScholarDigital Library
- Courcelle, B. 1983. Fundamental properties of infinite trees. Theor. Comput. Sci. 25, 95--169.Google ScholarCross Ref
- Crampton, J. and Morisset, C. 2012. PTaCL: A language for attribute-based access control in open systems. In Principles of Security and Trust, Lecture Notes in Computer Science, vol. 7215, Springer, 390--409. Google ScholarDigital Library
- de Moura, L., Dutertre, B., and Shankar, N. 2007. A tutorial on satisfiability modulo theories. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV’07). Lecture Notes in Computer Science, vol. 4590, Springer, 20--36. Google ScholarDigital Library
- Detreville, J. 2002. Binder, a logic-based security language. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 105--113. Google ScholarDigital Library
- Fisler, K., Krishnamurthi, S., Meyerovich, L. A., and Tschantz, M. C. 2005. Verification and change-impact analysis of access-control policies. In Proceedings of the 27th International Conference on Software Engineering (ICSE’05). ACM Press, New York, 196--205. Google ScholarDigital Library
- Fredkin, E. 1960. Trie memory. Comm. ACM 3, 490--499. Google ScholarDigital Library
- Haarslev, V. and Möller, R. 2001. RACER system description. In Proceedings of the 1st International Joint Conference on Automated Reasoning (IJCAR’01). Springer, 701--706. Google ScholarDigital Library
- Halpern, J. Y. and Weissman, V. 2008. Using first-order logic to reason about policies. ACM Trans. Inf. Syst. Secur. 11, 1--41. Google ScholarDigital Library
- Harrison, M. A., Ruzzo, W. L., and Ullman, J. D. 1976. Protection in operating systems. Comm. ACM 19, 461--471. Google ScholarDigital Library
- Hoare, C. A. R. 1978. Communicating sequential processes. Comm. ACM 21, 666--677. Google ScholarDigital Library
- Hosmer, H. H. 1993. The multipolicy paradigm for trusted systems. In Proceedings on the Workshop on New Security Paradigms (NSPW’92-93). ACM Press, New York, 19--32. Google ScholarDigital Library
- Hughes, G. and Bultan, T. 2008. Automated verification of xacml policies using a sat solver. Int. J. Softw. Tools Technol. Transfer 10, 6, 503--520. Google ScholarDigital Library
- Huonder, F. 2010. Conflict detection and resolution of xacml policies. Masters thesis, University of Applied Sciences Rapperswil.Google Scholar
- Hutton, G. 1999. A tutorial on the universality and expressiveness of fold. J. Funct. Program. 9, 355--372. Google ScholarDigital Library
- Jackson, D. 2002. Alloy: A lightweight object modelling notation. Softw. Engin. Methodol. 11, 2, 256--290. Google ScholarDigital Library
- Jajodia, S., Samarati, P., Sapino, M. L., and Subrahmanian, V. S. 2001. Flexible support for multiple access control policies. ACM Trans. Database Syst. 26, 214--260. Google ScholarDigital Library
- Kagal, L., Berners-Lee, T., Connolly, D., and Weitzner, D. 2006. Using semantic web technologies for policy management on the web. In Proceedings of the 21st National Conference on Artificial Intelligence. Vol. 2, AAAI Press, 1337--1344. Google ScholarDigital Library
- Kagal, L., Finin, T., and Joshi, A. 2003. A policy language for a pervasive computing environment. In Proceedings of the 4th IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY’03). IEEE Computer Society, 63--74. Google ScholarDigital Library
- Kemper, A., Moerkotte, G., and Steinbrunn, M. 1992. Optimizing boolean expressions in object-bases. In Proceedings of the 18th International Conference on Very Large Data Bases (VLDB’92). Morgan Kaufmann Publishers, San Fransisco, CA, 79--90. Google ScholarDigital Library
- Kolovski, V. 2008. Logic-based framework for web access control policies. Ph.D. thesis, Computer Science Department, University of Maryland. Google ScholarDigital Library
- Kolovski, V. and Hendler, J. 2008. XACML policy analysis using description logics. www.mindswap.org/~kolovskiKolovskiXACMLAnalysisJCSSubmission.pdf.Google Scholar
- Kolovski, V., Hendler, J., and Parsia, B. 2007. Analyzing web access control policies. In Proceedings of the 16th International Conference on World Wide Web (WWW’07). ACM Press, New York, 677--686. Google ScholarDigital Library
- Krishnamurthi, S. 2003. The continue server (or, how i administered padl 2002 and 2003). In Proceedings of the 5th International Symposium on Practical Aspects of Declarative Languages (PADL’03). V. Dahl and P. Wadler Eds., Lecture Notes in Computer Science, vol. 2562, Springer, 2--16. Google ScholarDigital Library
- Krukow, K., Nielsen, M., and Sassone, V. 2008. A logical framework for history-based access control and reputation systems. J. Comput. Secur. 16, 63--101. Google ScholarDigital Library
- Lampson, B., Abadi, M., Burrows, M., and Wobber, E. 1991. Authentication in distributed systems: Theory and practice. SIGOPS Oper. Syst. Rev. 25, 165--182. Google ScholarDigital Library
- Li, N., Mitchell, J. C., and Winsborough, W. H. 2002. Design of a role-based trust management framework. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 114--130. Google ScholarDigital Library
- Mankai, M. and Logrippo, L. 2005. Access control policies: Modeling and validation. In Proceedings of the 5th NOTERE Conference. 85--91.Google Scholar
- Massacci, F. 1997. Reasoning about security: A logic and a decision method for role-based access control. In Proceedings of the 1st International Joint Conference on Qualitative and Quantitative Practical Reasoning (ECSQARU-FAPR’97). 421--435. Google ScholarDigital Library
- Moura, L. D. and Bjørner, N. 2011. Satisfiability modulo theories: Introduction and applications. Comm. ACM 54, 9, 69--77. Google ScholarDigital Library
- Perry, J., Arkoudas, K., Chiang, J., and Chadha, R. 2013. Modular natural language interfaces to logic-based policy frameworks. Comput. Standards Interfaces 35, 5, 417--427.Google ScholarCross Ref
- Rao, P., Lin, D., Bertino, E., Li, N., and 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 Press, New York, 63--72. Google ScholarDigital Library
- Rissanen, E. 2007. Extensible access control markup language (xacml) version 3.0 (core specication and schemas). www.oasis-open.org/committees/download.php/23950/xacml-3.0-core-wd-02.zip.Google Scholar
- Rushby, J. 2006. Harnessing disruptive innovation in formal verification. In Proceedings of the 4th International Conference on Software Engineering and Formal Methods (SEFM’06). D. V. Hung and P. Pandya Eds., IEEE Computer Society, 21--28. Google ScholarDigital Library
- Sandhu, R., Bhamidipati, V., and Munawer, Q. 1999. The arbac97 model for role-based administration of roles. ACM Trans. Inf. Syst. Secur. 2, 105--135. Google ScholarDigital Library
- Schaad, A. and Moffett, J. D. 2002. A lightweight approach to specification and analysis of role-based access control extensions. In Proceedings of the 7th ACM Symposium on Access Control Models and Technologies (SACMAT’02). ACM Press, New York, 13--22. Google ScholarDigital Library
- Toahchoodee, M. and Ray, I. 2005. Validation of policy integration using alloy. In Proceedings of the 2nd International Conference on Distributed Computing and Internet Technology (ICDCIT’05). G. Chakraborty Ed., Lecture Notes in Computer Science, vol. 3816, Springer, 420--431. Google ScholarDigital Library
- Trevor, J. 2001. SD3: A trust management system with certified evaluation. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 106--115. Google ScholarDigital Library
- Uszok, A., Bradshaw, J. M., Johnson, M., Jeffers, R., Tate, A., Dalton, J., and Aitken, S. 2004. KAoS policy management for semantic web services. IEEE Intell. Syst. 19, 32--41. Google ScholarDigital Library
- Westerinen, A., Schnizlein, J., Strassner, J., Scherling, M., Quinn, B., Herzog, S., Huynh, A., Carlson, M., Perry, J., and Waldbusser, S. 2001. Terminology for policy-based management. RFC 3198 (Informational). Google ScholarDigital Library
- Wijesekera, D. and Jajodia, S. 2003. A propositional policy algebra for access control. ACM Trans. Inf. Syst. Secur. 6, 286--325. Google ScholarDigital Library
- Woo, T. Y. C. and Lam, S. S. 1992. Authorization in distributed systems: A formal approach. In Proceedings of the IEEE Symposium on Security and Privacy (SP’92). IEEE Computer Society. Google ScholarDigital Library
- Woo, T. Y. C. and Lam, S. S. 1993. Authorizations in distributed systems: A new approach. J. Comput. Secur. 2, 2--3, 107--136.Google ScholarCross Ref
- Zhang, N., Ryan, M., and Guelev, D. 2005. Evaluating access control policies through model checking. In Proceedings of the 8th International Conference on Information Security (ISC’05). J. Zhou, J. Lopez, R. Deng, and F. Bao Eds., Lecture Notes in Computer Science, vol. 3650, Springer, 446--460. Google ScholarDigital Library
- Zhao, C., Heilili, N., Liu, S., and Lin, Z. 2005. Representation and reasoning on rbac: A description logic approach. In Proceedings of the 2nd International Colloquium on Theoretical Aspects of Computing (ICTAC’05). D. V. Hung and M. Wirsing Eds., Lecture Notes in Computer Science, vol. 3722, Springer, 381--393. Google ScholarDigital Library
Index Terms
- Sophisticated Access Control via SMT and Logical Frameworks
Recommendations
Access-Control Policies via Belnap Logic: Effective and Efficient Composition and Analysis
CSF '08: Proceedings of the 2008 21st IEEE Computer Security Foundations SymposiumIt is difficult to develop and manage large, multi-author access control policies without a means to compose larger policies from smaller ones. Ideally, an access-control policy language will have a small set of simple policy combinators that allow for ...
Automated Policy Analysis
POLICY '12: Proceedings of the 2012 IEEE International Symposium on Policies for Distributed Systems and NetworksStatic analysis of access-control policies is becoming increasingly important. Such analysis can reveal errors and vulnerabilities in the policies, as well as logical inconsistencies, unintended effects, and discrepancies between different policies or ...
Analyzing web access control policies
WWW '07: Proceedings of the 16th international conference on World Wide WebXACML has emerged as a popular access control language on the Web, but because of its rich expressiveness, it has proved difficult to analyze in an automated fashion. In this paper, we present a formalization of XACML using description logics (DL), ...
Comments