Abstract
We present a formal, tool-supported approach to the design and maintenance of access control policies expressed in the eXtensible Access Control Markup Language (XACML). Our aim is to help developers evaluate the consequences of policy decisions in complex situations where security requirements change and access decisions may depend on the external dynamic environment. The approach applies the model-oriented specification language from the Vienna Development Method (VDM++). An executable formal model of XACML access control is presented in VDM++. The use of the model to analyse and revise both policies and requirements on the environment is illustrated through an example. An approach to the practical problem of analysing access control in virtual organisations with dynamic membership and goals is proposed.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Andrews, D.J. (ed.): Information technology – Programming languages, their environments and system software interfaces – Vienna Development Method – Specification Language – Part 1: Base language. International Organization for Standardization, International Standard ISO/IEC 13817-1 (December 1996)
Becker, M.Y., Fournet, C., Gordon, A.D.: SecPAL: Design and semantics of a decentralized authorisation language. Technical Report MSR-TR-2006-120, Microsoft Research (September 2006)
Bryans, J.W., Fitzgerald, J.S., Jones, C.B., Mozolevsky, I.: Formal modelling of dynamic coalitions, with an application in chemical engineering. In: 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), IEEE Computer Society Press, Los Alamitos (2006) Also available as Technical Report CS-TR-981, Newcastle University, UK (to appear)
Bryans, J.W., Fitzgerald, J.S., Periorellis, P.: Model based analysis and validation of access control policies. Technical Report CS-TR-976, Newcastle University, School of Computing Science (July 2006)
Domingos, D., Rito-Silva, A., Veiga, P.: Authorization and access control in adaptive workflows. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 23–38. Springer, Heidelberg (2003)
Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Specifying and reasoning about dynamic access-control policies. In: Proceedings of the International Joint Conference on Automated Reasoning (August 2006)
Fisler, K., Krishnamurthi, S., Meyerovich, L.A., Tschantz, M.C.: Verification and change-impact analysis of access-control policies. In: ICSE 2005, pp. 196–205. ACM Press, New York (2005)
Fitzgerald, J.S., Larsen, P.G.: Modelling Systems: Practical Tools and Techniques in Software Development. Cambridge University Press, Cambridge (1998)
Fitzgerald, J.S., Larsen, P.G.: Triumphs and challenges for the industrial application of model-oriented formal methods. In: 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), IEEE Computer Society Press, Los Alamitos (2006) Also available as Technical Report CS-TR-999, Newcastle University, UK (to appear)
Fitzgerald, J.S., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs for Object-oriented Systems. Springer, Heidelberg (2004)
Hughes, G., Bultan, T.: Automated verification of access control policies. Technical Report 2004-22, University of California, Santa Barbara (2004)
Humenn, P.: The formal semantics of XACML, available at http://lists.oasis-open.org/archives/xacml/200310/pdf00000.pdf
Jones, C.B.: Systematic Software Development using VDM. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1990)
Jones, C.B., Hayes, I.J., Jackson, M.A.: Deriving specifications for systems that are connected to the physical world. In: Woodcock, J. (ed.) Essays in Honour of Dines Bjørner and Zhou Chaochen on the Occasion of their 70th Birthdays. LNCS, vol. 4700, pp. 364–390. Springer, Heidelberg (2007)
Méry, D., Merz, S.: Event systems and access control. In: Gollmann, D., Jürjens, J. (eds.) 6th International Workshop on Issues in the Theory of Security, Vienna, Austria, IFIP WG 1.7, Vienna University of Technology, pp. 40–54 (2006)
OASIS: eXtensible Access Control Markup Language (XACML) version 2.0. Technical report, OASIS (February 2005)
Overture Group: The VDM Portal (2007), http://www.vdmportal.org
Zhang, N., Ryan, M.D., Guelev, D.: Synthesising verified access control systems through model checking. Journal of Computer Security (in print, 2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bryans, J.W., Fitzgerald, J.S. (2007). Formal Engineering of XACML Access Control Policies in VDM++. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds) Formal Methods and Software Engineering. ICFEM 2007. Lecture Notes in Computer Science, vol 4789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76650-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-76650-6_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-76648-3
Online ISBN: 978-3-540-76650-6
eBook Packages: Computer ScienceComputer Science (R0)