Checking Interaction-Based Declassification Policies for Android Using Symbolic Execution
Mobile apps can access a wide variety of secure information, such as contacts and location. However, current mobile platforms include only coarse access control mechanisms to protect such data. In this paper, we introduce interaction-based declassificatio
- PDF / 749,851 Bytes
- 19 Pages / 439.37 x 666.142 pts Page_size
- 4 Downloads / 249 Views
University of Maryland, College Park, USA {micinski,jonfd,jsjeon,jfoster}@cs.umd.edu 2 Cornell University, Ithaca, USA [email protected]
Abstract. Mobile apps can access a wide variety of secure information, such as contacts and location. However, current mobile platforms include only coarse access control mechanisms to protect such data. In this paper, we introduce interaction-based declassification policies, in which the user’s interactions with the app constrain the release of sensitive information. Our policies are defined extensionally, so as to be independent of the app’s implementation, based on sequences of security-relevant events that occur in app runs. Policies use LTL formulae to precisely specify which secret inputs, read at which times, may be released. We formalize a semantic security condition, interaction-based noninterference, to define our policies precisely. Finally, we describe a prototype tool that uses symbolic execution of Dalvik bytecode to check interaction-based declassification policies for Android, and we show that it enforces policies correctly on a set of apps.
Keywords: Information flow
1
· Program analysis · Symbolic execution
Introduction
The Android platform includes a permission system that aims to prevent apps from abusing access to sensitive information, such as contacts and location. Unfortunately, once an app is installed, it has carte blanche to use any of its permissions in arbitrary ways at run time. For example, an app with location and Internet access could continuously broadcast the device’s location, even if such behavior is not expected by the user. To address this limitation, this paper presents a new framework for Android app security based on information flow control [8] and user interactions. The key idea behind our framework is that users naturally express their intentions about This research was supported in part by NSF grants CNS-1064997 and CNS-1421373, AFOSR grants FA9550-12-1-0334 and FA9550-14-1-0334, the partnership between UMIACS and the Laboratory for Telecommunication Sciences, and the National Security Agency. c Springer International Publishing Switzerland 2015 G. Pernul et al. (Eds.): ESORICS 2015, Part II, LNCS 9327, pp. 520–538, 2015. DOI: 10.1007/978-3-319-24177-7 26
Checking Interaction-Based Declassification Policies for Android
521
information release as they interact with an app. For example, clicking a button may permit an app to release a phone number over the Internet. Or, as another example, toggling a radio button from “coarse” to “fine” and back to “coarse” may temporarily permit an app to use fine-grained GPS location rather than a coarse-grained approximation. To model these kinds of scenarios, we introduce interaction-based declassification policies, which extensionally specify what information flows may occur after which sequences of events. Events are GUI interactions (e.g., clicking a button), inputs (e.g., reading the phone number), or outputs (e.g., sending over the Internet). A policy is a set of declassification conditi
Data Loading...
