Validation of Security-Design Models using Z

Muhammad Nafees Qamar (1, 2) , Yves Ledru (3) , Akram Idani (3)

1 LIG - Laboratoire d'Informatique de Grenoble
2 POP ART - Programming languages, Operating Systems, Parallelism, and Aspects for Real-Time
3 VASCO - Validation de Systèmes, Composants et Objets logiciels

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.

Domaines: Génie logiciel [cs.SE]

Muhammad Nafees Qamar, Yves Ledru, Akram Idani. Validation of Security-Design Models using Z. ICFEM 2011 - 13th International Conference on Formal Engineering Methods, Oct 2011, Durham, United Kingdom. pp.259-274, ⟨10.1007/978-3-642-24559-6_19⟩. ⟨hal-00860804⟩