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.

Cache-based attacks are a class of side-channel attacks that are particularly effective in virtualized or cloud-based environments, where they have been used to recover secret keys from cryptographic implementations. One common approach to thwart cache-based attacks is to use constant-time implementations, i.e., which do not branch on secrets and do not perform memory accesses that depend on secrets. However, there is no rigorous proof that constant-time implementations are protected against concurrent cache-attacks in virtualization platforms with shared cache; moreover, many prominent implementations are not constant-time. An alternative approach is to rely on system-level mechanisms. One recent such mechanism is stealth memory, which provisions a small amount of private cache for programs to carry potentially leaking computations securely. Stealth memory induces a weak form of constant-time, called S-constant-time, which encompasses some widely used cryptographic implementations. However, there is no rigorous analysis of stealth memory and S-constant-time, and no tool support for checking if applications are S-constant-time.

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.

Virtualization platforms allow multiple operating systems to run on the same hardware. One of their central goal is to provide strong isolation between guest operating systems, unfortunately, they are often vulnerable to practical side-channel attacks. Cache attacks are a common class of side-channel attacks that use the cache as a side channel. We formalize an idealized model of virtualization that features the cache and the Translation Look aside Buffer (TLB), and that provides an abstract treatment of cache-based side-channels. We then use the model for reasoning about cache-based attacks and countermeasures, and for proving that isolation between guest operating systems can be enforced by flushing the cache upon context switch. In addition, we show that virtualized platforms are transparent, i.e. a guest operating system cannot distinguish whether it executes alone or together with other guest operating systems on the platform. The models and proofs have been machine-checked in the Coqproof assistant.