by Gabriele Costa, Alessio Merlo and Luca Verderame
We present a security-enabled application marketplace that provides formal security guarantees to the existing mobile software distribution paradigm. Our proposal allows users and organizations to apply fine-grained security policies on top of the existing market-based software deployment with no need for invasive customization of devices and without compromising the system scalability and usability.
Most modern mobile Operating Systems (OSs)rely on application marketplaces, also called app stores, to allow users to download and install software packages that extend their devices with new functionalities. The success of this software distribution paradigm is confirmed by the gargantuan number of mobile applications released and installed every day.
Despite the enormous advantages in terms of customizability, access to many third party software packages raises several security issues. One major issue is how to provide fine grained, strong security guarantees without compromising usability and scalability. Most mobile OSs don’t apply security-relevant settings automatically, critical choices about security aspects have to be made by the user. For instance, Android requires that users accept the application contract, or “manifest”, at installation time. Also, the marketplace collects positive and negative feedback that serves as a reputation system that customers can consider before installing new software.
Nevertheless, these mechanisms do not offer proper protection to users. Indeed, manifest descriptions are extremely coarse grained, eg, “this app will use the filesystem”, and even expert users struggle to find a relationship between a manifest and their security needs. Recent studies have demonstrated that users generally disregard security-relevant warnings upon installation of applications, thus ignoring potential security risks.
Furthermore, once a user has installed an application, it can run freely and independently of the context, ie the device configuration, under which it is used. For instance, current mobile OSs have no mechanism to prevent a user from playing games or executing applications that may spread sensitive information during business hours. Consequently, organizations that could benefit from their employees having a smartphone, eg, because the company could avoid purchasing multiple specific devices, may be reluctant to use them.
To cope with these issues, we recently proposed (see [1,2]) a novel approach that provides formal security guarantees to the users of mobile devices. Furthermore, the system is built on top of the existing mobile applications distribution paradigm, which makes the whole system scalable and reusable.
In practice, a mobile application marketplace works as follows: Owners of mobile devices register to a marketplace by means of access credentials. The marketplace stores device information and configuration, eg, hardware profile, OS version and installed applications. When the user decides to install a new application, the marketplace checks the compatibility with the device configuration and requests the user to provide the application with the requested access rights. If the user disagrees, the installation is cancelled, otherwise the marketplace sends the software package and the device installs it.
We propose the use of a security enabled marketplace that acts as a security proxy, providing a formal security guarantee. A secure marketplace exploits a security policies management system and verifies whether a certain application can be installed on a device without affecting the security configuration. Application packages are analyzed to extract security contracts that, in turn, extend and enrich the manifest. Contracts are safe representations of the application’s behaviour, and denote all the possible sequences of system access operations that the software can perform (including possible synchronizations with other installed applications).
The secure marketplace then applies a model checking procedure to verify whether the device configuration composed with the application contract is still policy-compliant. If it is, the application is labeled as safe. Otherwise, the application can be modified by instrumenting its code with security checks, guaranteeing that it respects the policy. In both cases, the secure marketplace generates a safety proof that the user can verify, through automatic proof checking, before installation.
After installation confirmation, the secure marketplace updates the policy management system with the new security state of the device.
Our proposed system could work with most of the common usage contexts for mobile devices. Indeed, it applies equally to both private customers, ie, users wanting to apply security controls to their own devices, and companies, ie, organizations in which employees and affiliated persons must respect precise security restrictions.
We are currently developing a real implementation of our secure marketplace that customers can use to mediate the access to standard marketplaces, eg, Google play.
We plan to release a secure marketplace implementation for Android OS in mid-2013. Moreover, we are currently investigating potential extensions of our proposal; including the adoption of security monitoring to allow the user to install applications that statically violate the policy. In this way, application executions are guaranteed to respect the security policy.
References:
[1] A. Armando, G. Costa, A. Merlo: “Formal Modeling and Reasoning about the Android Security Framework”, in proc. of TGC 2012, Newcastle upon Tyne, UK, 2012
http://www.ai-lab.it/merlo/publications/ AndroidModel.pdf
[2] A. Armando, G. Costa, A. Merlo, L. Verderame: “Bring Your Own Device, Securely”, in proc. of SAC 2013, Coimbra, Portugal, 2013
http://www.ai-lab.it/merlo/publications/ BYODroid-extended.pdf
Please contact:
Gabriele Costa
University of Genova, Italy
Tel: +39 0103536545
E-mail:
Alessio Merlo
E-Campus University, Italy
Tel: +39 0103532344
E-mail:
