A Formal Model to Analyze the Permission Authorization and Enforcement in the Android Framework

TLDR

This paper proposes a formal model of the Android permission scheme. The authors describe a state‑based model of Android permission entities and relationships, and use a theorem prover to verify security against specified requirements. The model enables logical confirmation of security, serves as a reference for other platforms, reveals a vulnerability in Android, and represents the first formalization of its permission scheme.

Abstract

This paper proposes a formal model of the Android permission scheme. We describe the scheme specifying entities and relationships, and provide a state-based model which includes the behavior specification of permission authorization and the interactions between application components. We also show how we can logically confirm the security of the specified system. Utilizing a theorem prover, we can verify security with given security requirements based on mechanically checked proofs. The proposed model can be used as a reference model when the scheme is implemented in a different embedded platform, or when we extend the current scheme with additional constraints or elements. We demonstrate the use of the verifiable specification through finding a security vulnerability in the Android system. To our knowledge, this is the first formalization of the permission scheme enforced by the Android framework.