Checking interaction-based declassification policies for android using symbolic execution

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

doi:10.1007/978-3-319-24177-7_26

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/Entry/Poem › Conference contribution

10 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 language	English (US)
Title of host publication	Computer Security – ESORICS 2015 - 20th European Symposium on Research in Computer Security, Proceedings
Editors	Günther Pernul, Peter Y.A. Ryan, Edgar Weippl
Publisher	Springer Verlag
Pages	520-538
Number of pages	19
ISBN (Print)	9783319241760
DOIs	https://doi.org/10.1007/978-3-319-24177-7_26
State	Published - 2015
Externally published	Yes
Event	20th European Symposium on Research in Computer Security, ESORICS 2015 - Vienna, Austria Duration: Sep 21 2015 → Sep 25 2015

Publication series

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

Conference

Conference	20th European Symposium on Research in Computer Security, ESORICS 2015
Country/Territory	Austria
City	Vienna
Period	9/21/15 → 9/25/15

Keywords

Information flow
Program analysis
Symbolic execution

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-319-24177-7_26

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

Checking interaction-based declassification policies for android using symbolic execution. / Micinski, Kristopher; Fetter-Degges, Jonathan; Jeon, Jinseong et al.
Computer Security – ESORICS 2015 - 20th European Symposium on Research in Computer Security, Proceedings. ed. / Günther Pernul; Peter Y.A. Ryan; Edgar Weippl. Springer Verlag, 2015. p. 520-538 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9327).

Research output: Chapter in Book/Entry/Poem › Conference contribution

Micinski, K, Fetter-Degges, J, Jeon, J, Foster, JS & Clarkson, MR 2015, Checking interaction-based declassification policies for android using symbolic execution. in G Pernul, PYA Ryan & E Weippl (eds), Computer Security – ESORICS 2015 - 20th European Symposium on Research in Computer Security, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9327, Springer Verlag, pp. 520-538, 20th European Symposium on Research in Computer Security, ESORICS 2015, Vienna, Austria, 9/21/15. https://doi.org/10.1007/978-3-319-24177-7_26

Micinski K, Fetter-Degges J, Jeon J, Foster JS, Clarkson MR. Checking interaction-based declassification policies for android using symbolic execution. In Pernul G, Ryan PYA, Weippl E, editors, Computer Security – ESORICS 2015 - 20th European Symposium on Research in Computer Security, Proceedings. Springer Verlag. 2015. p. 520-538. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-24177-7_26

Micinski, Kristopher ; Fetter-Degges, Jonathan ; Jeon, Jinseong et al. / Checking interaction-based declassification policies for android using symbolic execution. Computer Security – ESORICS 2015 - 20th European Symposium on Research in Computer Security, Proceedings. editor / Günther Pernul ; Peter Y.A. Ryan ; Edgar Weippl. Springer Verlag, 2015. pp. 520-538 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{6f134961f5864705886e380be7dd57a2,

title = "Checking interaction-based declassification policies for android using symbolic execution",

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{\textquoteright}s interactions with the app constrain the release of sensitive information. Our policies are defined extensionally, so as to be independent of the app{\textquoteright}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, Program analysis, Symbolic execution",

author = "Kristopher Micinski and Jonathan Fetter-Degges and Jinseong Jeon and Foster, {Jeffrey S.} and Clarkson, {Michael R.}",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2015.; 20th European Symposium on Research in Computer Security, ESORICS 2015 ; Conference date: 21-09-2015 Through 25-09-2015",

year = "2015",

doi = "10.1007/978-3-319-24177-7_26",

language = "English (US)",

isbn = "9783319241760",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "520--538",

editor = "G{\"u}nther Pernul and Ryan, {Peter Y.A.} and Edgar Weippl",

booktitle = "Computer Security – ESORICS 2015 - 20th European Symposium on Research in Computer Security, Proceedings",

}

TY - GEN

T1 - Checking interaction-based declassification policies for android using symbolic execution

AU - Micinski, Kristopher

AU - Fetter-Degges, Jonathan

AU - Jeon, Jinseong

AU - Foster, Jeffrey S.

AU - Clarkson, Michael R.

N1 - Publisher Copyright: © Springer International Publishing Switzerland 2015.

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

KW - Information flow

KW - Program analysis

KW - Symbolic execution

UR - http://www.scopus.com/inward/record.url?scp=84951756575&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84951756575&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-24177-7_26

DO - 10.1007/978-3-319-24177-7_26

M3 - Conference contribution

AN - SCOPUS:84951756575

SN - 9783319241760

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 520

EP - 538

BT - Computer Security – ESORICS 2015 - 20th European Symposium on Research in Computer Security, Proceedings

A2 - Pernul, Günther

A2 - Ryan, Peter Y.A.

A2 - Weippl, Edgar

PB - Springer Verlag

T2 - 20th European Symposium on Research in Computer Security, ESORICS 2015

Y2 - 21 September 2015 through 25 September 2015

ER -

Checking interaction-based declassification policies for android using symbolic execution

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this