Validation of a Security Policy by the Test of Its Formal B Specification -- A Case Study

Author

Ledru, Yves ; Idani, Akram ; Richier, Jean-Luc

Author_Institution

LIG, Univ. Grenoble Alpes, Grenoble, France

fYear

2015

fDate

18-18 May 2015

Firstpage

6

Lastpage

12

Abstract

This paper discusses the use of test and animation techniques to validate an access control policy, expressed in Secure UML. It reports on a case study of secure medical information system, where the Secure UML model expresses both functional and security models of the information system. It is translated into a specification in the B language. The case study takes advantage of animation tools associated to the B language to validate the functional model, to perform systematic test of permission rules and to investigate potential insiders attacks.

Keywords

Unified Modeling Language; authorisation; formal specification; medical information systems; program testing; UML security; access control policy; animation technique; formal B specification; functional model; insiders attacks; medical information system security; permission rules; security model; security policy; systematic test; test technique; Access control; Animation; Computational modeling; Medical diagnostic imaging; Medical services; Unified modeling language; Animation; B method; Formal specification; Test; Validation;

fLanguage

English

Publisher

ieee

Conference_Titel

Formal Methods in Software Engineering (FormaliSE), 2015 IEEE/ACM 3rd FME Workshop on

Conference_Location

Florence

Type

conf

DOI

10.1109/FormaliSE.2015.9

Filename

7166551