Modeling and Analyzing the Android Permission Framework using High Level Petri Nets

Android permission framework is a part of Android OS to enforce secure cross application communication. However the android permission framework is very complex, and its descriptions are scattered in dozens of webpages. It is very difficult to understand the relationships among multiple permission levels and their potential vulnerabilities. This paper presents a formal model of the Android permission framework using high level Petri nets. The model precisely defines the complex relationships among different levels of permissions. The model is constructed incrementally and thus is easily adaptable to future changes. The model building process is supported by our tool environment PIPE+, which further provides several analysis techniques. Simulation results for several scenarios that obey and violate the permission requirements are discussed.