A Formal Lens on Android Permissions System: Modeling, Verification, and Exploitation Using LLMs and Model Checking

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 paper, 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 One-Time Permissions 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.