This paper introduces the subject of secrecy models development by transformation, with formal validation. In an enterprise, constructing a secrecy model is a participatory exercise involving policy makers and implementers. Policy makers iteratively provide business governance requirements, while policy implementers formulate rules of access in computer-executable terms. The process is error prone and may lead to undesirable situations thus threatening the security of the enterprise. At each iteration, a security officer (SO) needs to guarantee business continuity by ensuring property preservation; as well, he needs to check for potential threats due to policy changes. This paper proposes a method that is meant to address both aspects: the formal analysis of transformation results and the formal proof that transformations are property preserving. UML is used for expressing and transforming models [1], and the Alloy analyzer is used to perform integrity checks [3]. Governance requirements dictate a security policy, that regulates access to information. This policy is implemented by means of secrecy models. Hence, the SO defines the mandatory secrecy rules as a part of enterprise governance model in order to implement security policy. For instance, a secrecy rule may state: higher-ranking officers have read rights to information at lower ranks. Automation helps reduce design errors of combined and complex secrecy models [2]. However, current industry practices do not include precise methods for constructing and validating enterprise governance models. Our research proposes a formal transformation method to construct secrecy models by way of applying transformations to a base UML model (BM). For example, starting from the BM, with only three primitives: Subject/Verb/Object, we can generate RBAC0 in addition to SecureUML [2] model. By way of examples and by means of formal analysis we intend to show that, using our method, a SO is able to build different types of secrecy models and validate them for consistency, in addition to detecting scenarios resulting from unpreserved properties.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{HassanSAL10,
author = {Wa{\"{e}}l Hassan and
Nadera Slimani and
Kamel Adi and
Luigi Logrippo},
editor = {Marc Frappier and
Uwe Gl{\"{a}}sser and
Sarfraz Khurshid and
R{\'{e}}gine Laleau and
Steve Reeves},
title = {Secrecy {UML} Method for Model Transformations},
booktitle = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
{ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5977},
pages = {400},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-11811-1\_35},
doi = {10.1007/978-3-642-11811-1\_35},
timestamp = {Sat, 31 May 2025 23:08:41 +0200},
biburl = {https://dblp.org/rec/conf/asm/HassanSAL10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}