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

51Citations
Citations of this article
64Readers
Mendeley users who have this article in their library.
Get full text

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. © 2010 IEEE.

Author supplied keywords

Cite

CITATION STYLE

APA

Shin, W., Kiyomoto, S., Fukushima, K., & Tanaka, T. (2010). A formal model to analyze the permission authorization and enforcement in the Android framework. In Proceedings - SocialCom 2010: 2nd IEEE International Conference on Social Computing, PASSAT 2010: 2nd IEEE International Conference on Privacy, Security, Risk and Trust (pp. 944–951). https://doi.org/10.1109/SocialCom.2010.140

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free