Kristopher Micinski
Current Organizations / Institutes
The organizations/institutes from the scholar's latest article
Research Subjects
Research Interests
Kristopher Micinski has a total of 7 co-authors. Here are the top co-authors by number of shared publications:
Jonathan Fetter-Degges
University of Maryland
2 shared publicationsJeffrey S. Foster
University of Maryland
1 shared publication- Jeffrey S. Foster
University of Maryland
1 shared publication Jinseong Jeon
University of Maryland
1 shared publication- Jinseong Jeon
University of Maryland College Park
1 shared publication Michael R. Clarkson
Cornell University
1 shared publication
Latest Publications
- 18 November 2015
- Published by Springer Nature
- p. 520-538
Checking Interaction-Based Declassification Policies for Android Using Symbolic Execution
- 18 November 2015
- Published by Springer Nature
- p. 520-538
Checking Interaction-Based Declassification Policies for Android Using Symbolic Execution
- Open Access
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 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 to check interaction-based declassification policies for Android, and we show that it enforces policies correctly on a set of apps.
Open AccessChecking 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 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 to check interaction-based declassification policies for Android, and we show that it enforces policies correctly on a set of apps.