Abstract
This paper is aimed at formally specifying and validating security-design models of an information system. It combines graphical languages and formal methods, integrating specification languages such as UML and an extension, SecureUML, with the Z language. The modeled system addresses both functional and security requirements of a given application. The formal functional specification is built automatically from the UML diagram, using our RoZ tool. The secure part of the model instanciates a generic security-kernel written in Z, free from applications specificity, which models the concepts of RBAC (Role-Based Access Control). The final modeling step creates a link between the functional model and the instanciated security kernel. Validation is performed by animating the model, using the Jaza tool. Our approach is demonstrated on a case-study from the health care sector where confidentiality and integrity appear as core challenges to protect medical records.
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
Abdallah, A.E., Khayat, E.J.: Formal Z Specifications of Several Flat Role-Based Access Control Models. In: Proceedings of the 30th Annual IEEE/NASA Software Engineering Workshop (SEW 2006), pp. 282–292. IEEE Computer Society, Los Alamitos (2006)
Amálio, N., Polack, F.: Comparison of Formalisation Approaches of UML Class Constructs in Z and Object-Z. In: Bert, D., Bowen, J., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 339–358. Springer, Heidelberg (2003)
Basin, D., Doser, J., Lodderstedt, T.: Model Driven Security: From UML Models to Access Control Infrastructures. ACM TOSEM 15(1), 39–91 (2006)
Basin, D.A., Clavel, M., Doser, J., Egea, M.: Automated Analysis of Security Design Models. Information and Software Technology, Special issue on Model Based Development for Secure Information Systems 51(5) (2009)
Boswell, A.: Specification and Validation of a Security Policy Model. IEEE Transactions on Software Engineering 21(2), 63–68 (1995)
Dupuy, S., Ledru, Y., Chabre-Peccoud, M.: An Overview of RoZ: A Tool for Integrating UML and Z Specifications. In: Wangler, B., Bergman, L.D. (eds.) CAiSE 2000. LNCS, vol. 1789, pp. 417–430. Springer, Heidelberg (2000)
Ferraiolo, D.F., Sandhu, R.S., Gavrila, S.I., Kuhn, D.R., Chandramouli, R.: Proposed NIST standard for Role-based Access Control. ACM Transactions on Information and System Security, 224–274 (2001)
Hall, A.: Specifying and Interpreting Class Hierarchies in Z. In: Proceedings of the Z User Workshop, pp. 120–138. Springer/BCS (1994)
Jürjens, J.: Secure Systems Development with UML. Springer, Heidelberg (2004)
Ledru, Y.: Using Jaza to Animate RoZ Specifications of UML Class Diagrams. In: Proceedings of the 30th Annual IEEE/NASA Software Engineering Workshop (SEW-30 2006), pp. 253–262. IEEE Computer Society, Los Alamitos (2006)
Ledru, Y., Qamar, N., Idani, A., Richier, J.L., Labiadh, M.A.: Validation of security policies by the animation of Z specifications. In: 16th ACM Symposium on Access Control Models and Technologies, SACMAT 2011, pp. 155–164. ACM, New York (2011)
Morimoto, S., Shigematsu, S., Goto, Y., Cheng, J.: Formal verification of security specifications with common criteria. In: Proceedings of the 22nd Annual ACM Symposium on Applied Computing (SAC 2007), pp. 1506–1512. ACM, New York (2007)
Power, D., Slaymaker, M., Simpson, A.: On Formalizing and Normalizing Role-Based Access Control Systems. The Computer Journal 52(3), 305–325 (2009)
Sohr, K., Drouineaud, M., Ahn, G.: Formal Specification of Role-based Security Policies for Clinical Information Systems. In: Proc. of the 20th Annual ACM Symposium on Applied Computing, pp. 332–339. ACM, New York (2005)
Sohr, K., Drouineaud, M., Ahn, G.J., Gogolla, M.: Analyzing and managing role-based access control policies. IEEE Trans. Knowl. Data Eng. 20(7), 924–939 (2008)
Spivey, J.M.: The Z Notation: A reference manual, 2nd edn. Prentice Hall, Englewood Cliffs (1992)
Toahchoodee, M., Ray, I., Anastasakis, K., Georg, G., Bordbar, B.: Ensuring spatio-temporal access control for real-world applications. In: SACMAT 2009, 14th ACM Symp. on Access Control Models and Technologies. ACM, New York (2009)
Utting, M.: JAZA: Just Another Z Animator (2005), http://www.cs.waikato.ac.nz/~marku/jaza/
Wordsworth, J.: Software Development with Z: a practical approach to formal methods. Addison-Wesley, Reading (1992)
Yuan, C., He, Y., He, J., Zhou, Z.: A Verifiable Formal Specification for RBAC Model with Constraints of Separation of Duty. In: Lipmaa, H., Yung, M., Lin, D. (eds.) Inscrypt 2006. LNCS, vol. 4318, pp. 196–210. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Qamar, N., Ledru, Y., Idani, A. (2011). Validation of Security-Design Models Using Z. In: Qin, S., Qiu, Z. (eds) Formal Methods and Software Engineering. ICFEM 2011. Lecture Notes in Computer Science, vol 6991. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24559-6_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-24559-6_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24558-9
Online ISBN: 978-3-642-24559-6
eBook Packages: Computer ScienceComputer Science (R0)