In 2018, as part of an undergraduate thesis project, a semi-formal access control model called PCA-RBAC (Purpose and Consent /Aware RBAC) was proposed. This model extends the Role-Based Access Control (RBAC) paradigm by incorporating notions of purpose and consent. PCA-RBAC was developed based on requirements drawn from Uruguay's Personal Data Protection Law No. 18.331, enacted in 2008. The model allows individuals to grant different types of consent depending on the kind of data involved, ensuring that such consents are respected when personal information is accessed. In the present work, the PCA-RBAC model is specified in a fully formal manner, representing, to the best of our knowledge, the first formalization of a system of this kind. A detailed analysis of some essential security properties of the model is performed; in particular, the system ensures that access to sensitive information is denied unless the necessary requirements regarding purpose and consent are met. Specifying the system as a state machine is key to rigorously analyzing its properties.

Attribute-based access control (ABAC) and relationship-based access control (ReBAC) are innovative access control methods that extend traditional models, including role-based access control (RBAC). This paper examines these models to suggest their application as a means of verifying the consent of a personal data subject. The objective is to apply these models in accordance with the General Data Protection Regulation (GDPR), which requires data owners to consent to the processing of their data for defined purposes, and ensure users utilize this data solely for those purposes. To validate this, we explore a benchmark proposed by NIST related to access control in a hospital setting, modifying it to assess data subject consent. From this case study, we deployed both access control approaches and subsequently compared their performance.

Security on mobile devices is fundamental, as they are managing confidential information in particular. Two of the most popular operating systems for mobile devices are Android and iOS. This work presents and analyzes some key characteristics of its security models, considering in particular its permission systems. Additionally, this paper presents a hybrid mobile application, a framework, for permission analysis that can run on both Android and iOS. The framework, which can be extended, places special emphasis on the relationship between the user's privacy and the permission system.

Mimblewimble is a privacy-oriented cryptocurrency technology that provides security and scalability properties that distinguish it from other protocols. Mimblewimble’s cryptographic approach is based on Elliptic Curve Cryptography which allows verifying a transaction without revealing any information about the transactional amount or the parties involved. Mimblewimble combines Confidential transactions, CoinJoin, and cut-through to achieve a higher level of privacy, security, and scalability. In our previous work ([2], [26], [25]), we have presented and discussed these security properties and presented a model-driven verification approach in order to guarantee the correctness of the protocol implementations. In particular, we have proposed an idealized model that is essential to the described verification process. In that formal setting, we say that a transaction is valid if it is balanced, all output range proofs are valid and the kernel signature is valid for the excess. However, no formal and precise definition was given to the signature requirement. In this paper, we put forward an extension of our model to enable signatures. We specify a signature scheme that allows us to develop several properties and lemmas we have defined on our initial idealized model. The definition of a valid transaction is extended accordingly.

This article presents an implementation, based on model-driven development, that supports mutation testing techniques for the evaluation of test cases. The mutation of the code is carried out through a process of model transformations that starts with a transformation of a JAVA program to a representation of it in XMI, which satisfies the requirements of the JAVA metamodel. Later, mutation rules are applied to the model by means of a transformation, model by model, to generate a mutated version of the original program. Finally, JAVA code mutated again through a transformation, model to text, defined with MOF2Text. This last version is the one used to experiment with the different test cases. The main contribution of this work is the proposal of a mutation mechanism of JAVA programs that makes use of existing standards and tools in the context of model-driven development.

This article reports on our experiences in applying formal methods to verify the security mechanisms of Android. We have developed a comprehensive formal specification of Android's permission model, which has been used to state and prove properties that establish expected behavior of the procedures that enforce the defined access control policy. We are also interested in providing guarantees concerning actual implementations of the mechanisms. Therefore we are following a verification approach that combines the use of idealized models on which fundamental properties are formally verified with testing of actual implementations using lightweight model-based techniques. We describe the formalized model, present security properties that have been verified using the Coq proof assistant and discuss a testing technique that relies on the use of certified algorithms.

The development of complex dynamic systems requires studies and analysis prior to implementation in order to detect unwanted behaviors. UML is a language widely used for modeling these systems through state machines. These models do not have appropriate execution and simulation tools to analyze the real behavior of systems. Discrete Event System Specification (DEVS) formalism allows to cover these deficiencies. Today, there are robust tools that run and collect information from DEVS models. This paper proposes an ad hoc implementation of graphical modeling of dynamic systems using a simplification of UML state machines. The paper also presents the development in Java of a transformation process for obtaining DEVS models and code generation for PowerDEVS, through a plugin for the Eclipse platform. Thus, this work is an essential step in the process of building a system that automates the process of analysis, design and implementation of UML state machines using DEVS.

The development of complex dynamic systems require studies and analysis prior to deployment with the goal of detecting unwanted behavior. UML is a language widely used for modeling these systems through state machines, among other mechanisms. Currently, these models do not have appropriate execution and simulation tools to analyze the real behavior of systems. Modeling and simulation for design and prototyping of systems are widely used techniques. In particular, the Discrete Event system Specification (DEVS) formalism separates the modeling and simulation; there are several tools available on the market that run and collect information from DEVS models. This paper proposes a model transformation mechanism of UML state machines to DEVS models in the context MDD, through the declarative QVT Relations language, in order to perform simulations using tools, such as PowerDEVS.

The software development methodologies and modeling techniques simplify the complexity of the software construction. The management of a software project wants to get a quality product, planning, organizing, supervising and controlling the evolution of this project throughout its life cycle. This work stems from a Research and Innovation Project for Improvement of Undergraduate Education that involves four courses of the last year of the course grade Computer Analyst, including the Final Project. This paper intends to address, investigate and identify the causes which make having the methodological tools and training, more teachers with years of experience in delivering these courses and personal monitoring of each group of students who made the Final Project, many cases fail to complete the project within the established planning.