Towards a transformation approach from SecureUML to Alloy

In critical information systems, Role-Based Access Control (RBAC) has been frequently used. The specification of access control policies is an essential step in securing information systems. This article presents a transformative approach for addressing design challenges within these specifications using Model-Driven Architecture (MDA). A method is introduced for specifying and verifying model-based access control (RBAC) rules by combining SecureUML and Alloy, referred to as SecureUML2Alloy. This approach leverages transformation techniques based on metamodels to express the SecureUML source model in the Alloy target model. The SecureUML2Alloy framework allows for the generation of an initial Alloy code that can be extended with facts, functions, and predicates depending on the case. The transformative framework offers a reliable, automated mechanism for verifying security specifications in critical systems, promoting both theoretical and practical advancements in model transformation and formal verification. This method provides a pathway for future automation tools in secure system design and analysis, contributing to the reliability and security of software systems across multiple fields.