A formal model to analyze the permission authorization and enforcement in the Android framework

  • Shin W
  • Kiyomoto S
  • Fukushima K
 et al. 
  • 64


    Mendeley users who have this article in their library.
  • 40


    Citations of this article.


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.

Author-supplied keywords

  • Android
  • Formal model
  • Permission

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Wook Shin

  • Shinsaku Kiyomoto

  • Kazuhide Fukushima

  • Toshiaki Tanaka

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free