Top

Published in:

2015 | OriginalPaper | Chapter

Checking Interaction-Based Declassification Policies for Android Using Symbolic Execution

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

Published in: Computer Security -- ESORICS 2015

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Factorization of Behavioral Integrity

next chapter Enhancing Java Runtime Environment for Smart Cards Against Runtime Attacks

Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82–90 (2013). http://doi.acm.org/10.1145/2408776.2408795 CrossRef

Chen, K.Z., Johnson, N.M., D’Silva, V., Dai, S., MacNamara, K., Magrino, T., Wu, E.X., Rinard, M., Song, D.X.: Contextual policy enforcement in Android applications with permission event graphs. In: NDSS, The Internet Society (2013). http://dblp.uni-trier.de/db/conf/ndss/ndss2013.html#ChenJDDMMWRS13

Chong, S., Myers, A.C.: Security policies for downgrading. In: Proceedings of the 11th ACM Conference on Computer and Communications Security, pp. 189–209, October 2004

Chong, S., Vikram, K., Myers, A.C.: SIF: enforcing confidentiality and integrity in web applications. In: Proceedings of 16th USENIX Security Symposium on USENIX Security Symposium, SS 2007, pp. 1:1–1:16. USENIX Association, Berkeley (2007)

Clark, D., Hunt, S.: Non-interference for deterministic interactive programs. In: Degano, P., Guttman, J., Martinelli, F. (eds.) FAST 2008. LNCS, vol. 5491, pp. 50–66. Springer, Heidelberg (2009). http://dx.doi.org/10.1007/978-3-642-01465-9_4 CrossRef

Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014 (ETAPS 2014). LNCS, vol. 8414, pp. 265–284. Springer, Heidelberg (2014). http://dx.doi.org/10.1007/978-3-642-54792-8_15 CrossRef

Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010). http://dl.acm.org/citation.cfm?id=1891823.1891830 CrossRef

Denning, D.E.R.: Secure Information Flow in Computer Systems. Ph.D. thesis, West Lafayette, IN, USA (1975), aAI7600514

Enck, W., Gilbert, P., Chun, B.G., Cox, L.P., Jung, J., McDaniel, P., Sheth, A.N.: Taintdroid: An information-flow tracking system for realtime privacy monitoring on smartphones. In: Proceedings of the 9th USENIX Conference on Operating Systems Design and Implementation, OSDI 2010, pp. 1–6. USENIX Association, Berkeley (2010). http://dl.acm.org/citation.cfm?id=1924943.1924971

10.

Google: Managing the Activity Lifecycle (2015). http://developer.android.com/training/basics/activity-lifecycle/index.html

11.

Jeon, J., Micinski, K.K., Foster, J.S.: SymDroid: Symbolic Execution for Dalvik Bytecode. Technical report CS-TR-5022, Department of Computer Science, University of Maryland, College Park, July 2012

12.

Jia, L., Aljuraidan, J., Fragkaki, E., Bauer, L., Stroucken, M., Fukushima, K., Kiyomoto, S., Miyake, Y.: Run-time enforcement of information-flow properties on android. In: Crampton, J., Jajodia, S., Mayes, K. (eds.) ESORICS 2013. LNCS, vol. 8134, pp. 775–792. Springer, Heidelberg (2013). http://dx.doi.org/10.1007/978-3-642-40203-6_43 CrossRef

13.

Krohn, M., Yip, A., Brodsky, M., Cliffer, N., Kaashoek, M.F., Kohler, E., Morris, R.: Information flow control for standard OS abstractions. In: Proceedings of Twenty-first ACM SIGOPS Symposium on Operating Systems Principles, SOSP 2007, pp. 321–334. ACM, New York (2007)

14.

Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Logics of Programs. Lecture Notes in Computer Science, vol. 193, pp. 196–218. Springer, Berlin (1985). http://dx.doi.org/10.1007/3-540-15648-8_16 CrossRef

15.

Ma, K.-K., Yit Phang, K., Foster, J.S., Hicks, M.: Directed symbolic execution. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 95–111. Springer, Heidelberg (2011). http://dl.acm.org/citation.cfm?id=2041552.2041563 CrossRef

16.

Micinski, K., Fetter-Degges, J., Jeon, J., Foster, J.S., Clarkson, M.R.: Checking interaction-based declassification policies for android using symbolic execution. Technical report CS-TR-5044, Department of Computer Science, University of Maryland, College Park, July 2015

17.

de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). http://dx.doi.org/10.1007/978-3-540-78800-3_24 CrossRef

18.

Myers, A.C.: Jflow: Practical mostly-static information flow control. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1999, pp. 228–241. ACM, New York (1999). http://doi.acm.org/10.1145/292540.292561

19.

O’Neill, K.R., Clarkson, M.R., Chong, S.: Information-flow security for interactive programs. In: Proceedings of the 19th IEEE Workshop on Computer Security Foundations, CSFW 2006, pp. 190–201. IEEE Computer Society, Washington (2006). http://dx.doi.org/10.1109/CSFW.2006.16

20.

Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS 1977, pp. 46–57. IEEE Computer Society, Washington (1977). http://dx.doi.org/10.1109/SFCS.1977.32

21.

Rafnsson, W., Hedin, D., Sabelfeld, A.: Securing interactive programs. In: Proceedings of the 2012 IEEE 25th Computer Security Foundations Symposium, CSF 2012, pp. 293–307. IEEE Computer Society, Washington (2012). http://dx.doi.org/10.1109/CSF.2012.15

22.

Roesner, F., Kohno, T., Moshchuk, A., Parno, B., Wang, H.J., Cowan, C.: User-driven access control: rethinking permission granting in modern operating systems. In: Proceedings of the 2012 IEEE Symposium on Security and Privacy, SP 2012, pp. 224–238. IEEE Computer Society, Washington (2012). http://dx.doi.org/10.1109/SP.2012.24

23.

Sabelfeld, A., Sands, D.: Declassification: dimensions and principles. J. Comput. Secur. 17(5), 517–548 (2009)CrossRef

24.

Vaughan, J.A., Chong, S.: Inference of expressive declassification policies. In: Proceedings of the 2011 IEEE Symposium on Security and Privacy SP 2011, pp. 180–195. IEEE Computer Society, Washington (2011). http://dx.doi.org/10.1109/SP.2011.20

25.

Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2–3), 167–187 (1996). http://dl.acm.org/citation.cfm?id=353629.353648 CrossRef

26.

Yang, Z., Yang, M., Zhang, Y., Gu, G., Ning, P., Wang, X.S.: Appintent: analyzing sensitive data transmission in Android for privacy leakage detection. In: Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, CCS 2013, pp. 1043–1054. ACM, New York (2013). http://doi.acm.org/10.1145/2508859.2516676

27.

Yee, K.P.: Aligning security and usability. IEEE Secur. Priv. 2(5), 48–55 (2004)CrossRef

28.

Zdancewic, S., Myers, A.: Observational determinism for concurrent program security. In: Proceedings of 16th IEEE Computer Security Foundations Workshop 2003, pp. 29–43 (2003)

Title: Checking Interaction-Based Declassification Policies for Android Using Symbolic Execution
Authors: Kristopher Micinski
Jonathan Fetter-Degges
Jinseong Jeon
Jeffrey S. Foster
Michael R. Clarkson
Publisher: Springer International Publishing
Book: Computer Security -- ESORICS 2015
Print ISBN: 978-3-319-24176-0

Electronic ISBN: 978-3-319-24177-7

Copyright Year: 2015
DOI: https://doi.org/10.1007/978-3-319-24177-7_26

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner