Show simple item record

Checking Interaction-Based Declassification Policies for Android Using Symbolic Execution

dc.contributor.authorMicinski, Kristopher
dc.contributor.authorFetter-Degges, Jonathan
dc.contributor.authorJeon, Jinseong
dc.contributor.authorFoster, Jeffrey S.
dc.contributor.authorClarkson, Michael R.
dc.description.abstractMobile 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.en_US
dc.relation.ispartofseriesUM Computer Science Department;CS-TR-5044
dc.titleChecking Interaction-Based Declassification Policies for Android Using Symbolic Executionen_US

Files in this item


This item appears in the following Collection(s)

Show simple item record