Android embodies security mechanisms at both OS and application level. In this platform application security is built primarily upon a system of permissions which specify restrictions on the operations a particular process can perform. The critical role of these security mechanisms makes them a prime target for (formal) verification. We present an idealized model of a reference monitor of the novel mechanisms of Android 6 (and further), where it is possible to grant permissions at run time. Using the programming language of the proof-assistant Coq we have developed a functional implementation of the reference validation mechanism and certified its correctness with respect to the specified reference monitor. Several properties concerning the permission model of Android 6 and its security mechanisms have been formally formulated and proved. Applying the program extraction mechanism provided by Coq we have also derived a certified Haskell prototype of the reference validation mechanism.
Several analyses have been carried out concerning the security of the Android system @cite_15 @cite_8 @cite_0 @cite_6 @cite_10 . Few works, however, pay attention to the formal aspects of the permission enforcing framework. In particular, Shin @cite_19 @cite_22 build a formal framework that represents the Android permission system, which is developed in Coq , as we do. However, that work does not consider several aspects of the platform covered in our model, namely, the different types of components, the interaction between a running instance and the system, the R W operation on a content provider, the semantics of the permission delegation mechanism and novel aspects of the security model, such as the management of runtime permissions.
@cite_22 @cite_8 @cite_6 @cite_0 @cite_19 @cite_15 @cite_10
2156368183 1986330503 2150587160 2105412867
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. Permission-based security models provide controlled access to various system resources. The expressiveness of the permission set plays an important role in providing the right level of granularity in access control. In this work, we present a methodology for the empirical analysis of permission-based security models which makes novel use of the Self-Organizing Map (SOM) algorithm of Kohonen (2001). While the proposed methodology may be applicable to a wide range of architectures, we analyze 1,100 Android applications as a case study. Our methodology is of independent interest for visualization of permission-based systems beyond our present Android-specific empirical analysis. We offer some discussion identifying potential points of improvement for the Android permission model attempting to increase expressiveness where needed without increasing the total number of permissions or overall complexity. Several works have recently shown that Android’s security architecture cannot prevent many undesired behaviors that compromise the integrity of applications and the privacy of their data. This paper makes two main contributions to the body of research on Android security: first, it develops a formal framework for analyzing Android-style security mechanisms; and, second, it describes the design and implementation of Sorbet, an enforcement system that enables developers to use permissions to specify secrecy and integrity policies. Our formal framework is composed of an abstract model with several specific instantiations. The model enables us to formally define some desired security properties, which we can prove hold on Sorbet but not on Android. We implement Sorbet on top of Android 2.3.7, test it on a Nexus S phone, and demonstrate its usefulness through a case study. Android is the first mass-produced consumer-market open source mobile platform that allows developers to easily create applications and users to readily install them. However, giving users the ability to install third-party applications poses serious security concerns. While the existing security mechanism in Android allows a mobile phone user to see which resources an application requires, she has no choice but to allow access to all the requested permissions if she wishes to use the applications. There is no way of granting some permissions and denying others. Moreover, there is no way of restricting the usage of resources based on runtime constraints such as the location of the device or the number of times a resource has been previously used. In this paper, we present Apex -- a policy enforcement framework for Android that allows a user to selectively grant permissions to applications as well as impose constraints on the usage of resources. We also describe an extended package installer that allows the user to set these constraints through an easy-to-use interface. Our enforcement framework is implemented through a minimal change to the existing Android code base and is backward compatible with the current security mechanism.