Checking interaction-based declassification policies for android using symbolic execution

Kristopher Micinski, Jonathan Fetter-Degges, Jinseong Jeon, Jeffrey S. Foster, Michael R. Clarkson

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationComputer Security – ESORICS 2015 - 20th European Symposium on Research in Computer Security, Proceedings
EditorsGünther Pernul, Peter Y.A. Ryan, Edgar Weippl
PublisherSpringer Verlag
Pages520-538
Number of pages19
ISBN (Print)9783319241760
DOIs
StatePublished - Jan 1 2015
Externally publishedYes
Event20th European Symposium on Research in Computer Security, ESORICS 2015 - Vienna, Austria
Duration: Sep 21 2015Sep 25 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9327
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference20th European Symposium on Research in Computer Security, ESORICS 2015
CountryAustria
CityVienna
Period9/21/159/25/15

Keywords

  • Information flow
  • Program analysis
  • Symbolic execution

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Checking interaction-based declassification policies for android using symbolic execution'. Together they form a unique fingerprint.

  • Cite this

    Micinski, K., Fetter-Degges, J., Jeon, J., Foster, J. S., & Clarkson, M. R. (2015). Checking interaction-based declassification policies for android using symbolic execution. In G. Pernul, P. Y. A. Ryan, & E. Weippl (Eds.), Computer Security – ESORICS 2015 - 20th European Symposium on Research in Computer Security, Proceedings (pp. 520-538). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9327). Springer Verlag. https://doi.org/10.1007/978-3-319-24177-7_26