The Android Permissions System (APS) is a permission-based access control mechanism that controls the applications’ access to protected resources such as user contacts and GPS locations. The evolution of APS—as a critical component of Android—has made the user experience more convenient. However, the vulnerabilities and attacks targeting the APS indicate that its thorough security analysis is essential to ensure system security and to protect user information. Although previous works applied formal methods to verify the security of APS, its new capabilities, such as One-Time Permissions (OTPs), have not yet been studied. In this article, we present a model checking approach for security verification of APS that supports OTPs. We use Large Language Models in a Chain-of-Thought process to assist in extracting the behavior of APS from its documentation and source code to design a formal model and a set of security properties. Then we use the TLC model checker to verify the security properties against the model. We analyze the APS in both Android 6 and Android 11 and we succeed in discovering a previously known vulnerability in Android 6 as well as a new vulnerability in OTPs in Android 11 named Permanent Permission Access (PPA). We also implement an exploit code to show that PPA leads to permanent illegal access to sensitive resources. Our experiments show that the developed exploit app works on the latest versions of Android too (including Android 15). Besides, we propose the required fix to mitigate the vulnerability.

Abstract Android users install various apps, such as banking apps, on their smart devices dealing with user‐sensitive information. The Android framework, via Inter‐Component Communication (ICC) mechanism, ensures that app components (inside the same app or on different apps) can communicate. The literature works have shown that this mechanism can cause security issues, such as app security policy violations, especially in the case of Inter‐App Communication (IAC). Despite the plethora of research on detecting security issues in IAC, detection techniques face fundamental ICC challenges for improving the precision of static analysis. Challenges include providing comprehensive and scalable modeling of app specification, capturing all potential ICC paths, and enabling more effective IAC analysis. To overcome such challenges, in this paper, we propose a framework called VAnDroid2, as an extension of our previous work, to address the security issues in multiple components at both intra‐ and inter‐app analysis levels. VAnDroid2, based on Model‐Driven Reverse Engineering, has extended our previous work as per following: (1) providing a comprehensive Intermediate Representation (IR) of the app which supports extracting all the ICC information from the app, (2) extracting high‐level representations of the apps and their interactions by omitting the details that are not relevant to inter‐app security analysis, and (3) enabling more effective IAC security analysis. This framework is implemented as an Eclipse‐based tool. The results of evaluating VAnDroid2 w.r.t. correctness, scalability, and run‐time performance, and comparing with state‐of‐the‐art analysis tools well indicate that VAnDroid2 is a promising framework in the field of Android inter‐app security analysis.

Summary Software development is a collaborative activity that requires teams of software engineers to cooperate and work in parallel on versions of models. However, model management techniques such as model differencing, merging, and versioning have turned out to be difficult challenges, due to the complexity of operations and graph‐like nature of models. Therefore, a well‐developed support for model merging process, as well as conflict management, is highly desired. This paper presents a novel process for model merging, called the Epsilon‐based Three‐way Merging Process (E3MP) process. Model merging is a significant problem where there are different versions of a system model amongst modeler teams. E3MP includes three components implemented into the Epsilon framework. First, modelers can define domain‐specific rules that customize the merging process. Second, E3MP enables an automated method for syntactic and semantic conflict detection amongst different versions of the system model. Third, E3MP puts forward a pattern‐based approach for conflict resolution. We applied two generic benchmarks to assess conflict detection and resolution capabilities of our approach and carried out an initial scalability evaluation for the model merge with large models and large change sets. The results of our experiments revealed that the proposed process allows generating consistent and semantically correct merged models.

Summary Android is extensively used worldwide by mobile application developers. Android provides applications with a message passing system to communicate within and between them. Due to the risks associated with this system, it is vital to detect its unsafe operations and potential vulnerabilities. To achieve this goal, a new framework, called VAnDroid, based on Model Driven Reverse Engineering (MDRE), is presented that identifies security risks and vulnerabilities related to the Android application communication model. In the proposed framework, some security‐related information included in an Android app is automatically extracted and represented as a domain‐specific model. Then, it is used for analyzing security configurations and identifying vulnerabilities in the corresponding application. The proposed framework is implemented as an Eclipse‐based tool, which automatically identifies the Intent Spoofing and Unauthorized Intent Receipt as two attacks related to the Android application communication model. To evaluate the tool, it has been applied to several real‐world Android applications, including 20 apps from Google Play and 110 apps from the F‐Droid repository. VAnDroid is also compared with several existing analysis tools, and it is shown that it has a number of key advantages over those tools specifically regarding its high correctness, scalability, and usability in discovering vulnerabilities. The results well indicate the effectiveness and capacity of the VAnDroid as a promising approach in the field of Android security.

Summary Design patterns solve recurring design problems. One of the best practices, to solve a whole problem in a specific context, is to apply patterns in the form of a collection of related patterns, ie, a pattern language (PL). However, with the rapid growth of the number of patterns and their interrelationships in PLs and because manual verification of the applied PLs is a tedious and error‐prone task, when designing in PL‐based fashion, there is a need for tool support to verify the applied PLs. In our previous work, aimed at automating the development process of PL verification tools, a PL formalism was presented. This paper, based on the presented formalism, describes a framework called Pattern Language Verifier Generator (PLVGen) that automatically generates a pattern language verifier (PLV) for any given PL assuming its constituent patterns are represented in the Unified Modeling Language (UML). Using a modelware approach, two metamodels named pattern language specification language (PLSL) and pattern specification language (PSL) are developed to model the given PL and its patterns, respectively. By getting the models of a PL and its patterns, PLVGen automatically generates an epsilon validation language (EVL) module representing the expected PLV. By launching PLV, the applied PL on a UML model will be verified. To evaluate the applicability of PLVGen in practice, we automatically generated three PLVs. The statistics regarding the generated PLVs, as case studies, illustrate the scalability of PLVGen. Compared with similar tools, the generated PLVs are more portable, transparent, and free of ambiguities.

Many designers use the patterns of a pattern language in creating the design model. In designing with patterns, there are three aspects of the pattern language that must be taken into consideration: structural, syntactic, and semantic. That means, the patterns must be applied correctly, the relationship between patterns must be correct, and the design model must be semantically correct. The syntactic aspect is important for pattern languages due to the fact that the patterns in a pattern language are interconnected via several relationships. To achieve automatic design model checking, the three aspects of a pattern language must be precisely defined. We propose formalisms for representing the structural, syntactic, and semantic aspects of a pattern language. As our case study, we select a pattern language in the domain of enterprise application architecture, and show how the pattern language is described using the proposed formalism.