Skip to main content
Erschienen in: Information Systems Frontiers 4/2021

14.11.2020

A Formal Specification of Access Control in Android with URI Permissions

verfasst von: Samir Talegaon, Ram Krishnan

Erschienen in: Information Systems Frontiers | Ausgabe 4/2021

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

A formal specification of access control yields a deeper understanding of any operating system, and facilitates performing security analysis of the OS. In this paper, we provide a comprehensive formal specification of access control in Android (ACiA). Prior work is limited in scope, furthermore, recent developments in Android concerning dynamic runtime permissions require rethinking of its formalization. Our formal specification includes three parts, the user-initiated operations (UIOs) and app-initiated operations (AIOs) - which are distinguished based on the initiating entity, and the URI permissions which are utilized in sharing temporary access to data. We also studied the evolution of URI permissions from API 10 (Gingerbread) to API 22 (Lollipop), and a brief discussion on this is included in the paper. Formalizing ACiA allowed us to discover many peculiar behaviors pertaining to ACiA. In addition to that, we discovered two significant issues with permissions in Android which were reported to Google.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

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!

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!

Literatur
Zurück zum Zitat Bagheri, H., Kang, E., Malek, S., & Jackson, D. (2015a). In Intl. Symp. on Formal Methods (pp. 73–89): Springer. Bagheri, H., Kang, E., Malek, S., & Jackson, D. (2015a). In Intl. Symp. on Formal Methods (pp. 73–89): Springer.
Zurück zum Zitat Bagheri, H., Sadeghi, A., Garcia, J., & Malek, S. (2015b). COVERT: Compositional analysis of android Inter-App permission leakage. IEEE Transactions on Software Engineering, 41(9), 866–886.CrossRef Bagheri, H., Sadeghi, A., Garcia, J., & Malek, S. (2015b). COVERT: Compositional analysis of android Inter-App permission leakage. IEEE Transactions on Software Engineering, 41(9), 866–886.CrossRef
Zurück zum Zitat Bagheri, H., Kang, E., Malek, S., & Jackson, D. (2018). A formal approach for detection of security flaws in the android permission system. Formal Aspects of Computing, 30(5), 525–544.CrossRef Bagheri, H., Kang, E., Malek, S., & Jackson, D. (2018). A formal approach for detection of security flaws in the android permission system. Formal Aspects of Computing, 30(5), 525–544.CrossRef
Zurück zum Zitat Betarte, G., Campo, J.D., Luna, C., & Romano, A. (2015). Verifying Android’s Permission Model, (pp. 485–504). Cham: Springer. Betarte, G., Campo, J.D., Luna, C., & Romano, A. (2015). Verifying Android’s Permission Model, (pp. 485–504). Cham: Springer.
Zurück zum Zitat Betarte, G., Campo, J., Luna, C., & Romano, A. (2016). Formal analysis of android’s Permission-Based security model 1. Scientific Annals of Computer Science, 26(1), 27–68.CrossRef Betarte, G., Campo, J., Luna, C., & Romano, A. (2016). Formal analysis of android’s Permission-Based security model 1. Scientific Annals of Computer Science, 26(1), 27–68.CrossRef
Zurück zum Zitat Betarte, G., Campo, J., Cristiá, M., Gorostiaga, F., Luna, C., & Sanz, C. (2017). Towards formal model-based analysis and testing of android’s security mechanisms. In 2017 XLIII Latin American Computer Conference (CLEI) (pp. 1–10): IEEE. Betarte, G., Campo, J., Cristiá, M., Gorostiaga, F., Luna, C., & Sanz, C. (2017). Towards formal model-based analysis and testing of android’s security mechanisms. In 2017 XLIII Latin American Computer Conference (CLEI) (pp. 1–10): IEEE.
Zurück zum Zitat Bugiel, S., Davi, L., Dmitrienko, A., Fischer, T., Sadeghi, A.R., & Shastry, B. (2012). Towards taming privilege-escalation attacks on android. In NDSS, Citeseer, (Vol. 17 p. 19). Bugiel, S., Davi, L., Dmitrienko, A., Fischer, T., Sadeghi, A.R., & Shastry, B. (2012). Towards taming privilege-escalation attacks on android. In NDSS, Citeseer, (Vol. 17 p. 19).
Zurück zum Zitat Chin, E., Felt, A.P., Greenwood, K., & Wagner, D. (2011). Analyzing inter-application communication in android. In Proc. of the 9th International Conference on Mobile Systems, Applications, and Services (pp. 239–252). Chin, E., Felt, A.P., Greenwood, K., & Wagner, D. (2011). Analyzing inter-application communication in android. In Proc. of the 9th International Conference on Mobile Systems, Applications, and Services (pp. 239–252).
Zurück zum Zitat Davi, L., Dmitrienko, A., Sadeghi, A.R., & Winandy, M. (2010). Privilege escalation attacks on android. In International conference on Information security (pp. 346–360): Springer. Davi, L., Dmitrienko, A., Sadeghi, A.R., & Winandy, M. (2010). Privilege escalation attacks on android. In International conference on Information security (pp. 346–360): Springer.
Zurück zum Zitat Enck, W., Ongtang, M., & McDaniel, P. (2009a). On lightweight mobile phone application certification. In Proc. of the 16th ACM Conference on Computer and Communications Security (pp. 235–245). Enck, W., Ongtang, M., & McDaniel, P. (2009a). On lightweight mobile phone application certification. In Proc. of the 16th ACM Conference on Computer and Communications Security (pp. 235–245).
Zurück zum Zitat Enck, W., Ongtang, M., & McDaniel, P. (2009b). Understanding android security. IEEE security & privacy, pp. 50–57. Enck, W., Ongtang, M., & McDaniel, P. (2009b). Understanding android security. IEEE security & privacy, pp. 50–57.
Zurück zum Zitat Enck, W., Octeau, D., McDaniel, P.D., & Chaudhuri, S. (2011). A study of android application security. In USENIX Security Symposium, (Vol. 2 p. 2). Enck, W., Octeau, D., McDaniel, P.D., & Chaudhuri, S. (2011). A study of android application security. In USENIX Security Symposium, (Vol. 2 p. 2).
Zurück zum Zitat Felt, A.P., Chin, E., Hanna, S., Song, D., & Wagner, D. (2011). Android permissions demystified. In Proc. of the 18th ACM conference on Computer and communications security (pp. 627–638). Felt, A.P., Chin, E., Hanna, S., Song, D., & Wagner, D. (2011). Android permissions demystified. In Proc. of the 18th ACM conference on Computer and communications security (pp. 627–638).
Zurück zum Zitat Fragkaki, E., Bauer, L., Jia, L., & Swasey, D. (2012). Modeling and Enhancing Android’s Permission System, (pp. 1–18). Berlin: Springer.CrossRef Fragkaki, E., Bauer, L., Jia, L., & Swasey, D. (2012). Modeling and Enhancing Android’s Permission System, (pp. 1–18). Berlin: Springer.CrossRef
Zurück zum Zitat Geerts, F., Goethals, B., & Mielikäinen, T. (2004). Tiling databases. In International conference on discovery science (pp. 278–289): Springer. Geerts, F., Goethals, B., & Mielikäinen, T. (2004). Tiling databases. In International conference on discovery science (pp. 278–289): Springer.
Zurück zum Zitat Grace, M.C., Zhou, Y., Wang, Z., & Jiang, X. (2012). Systematic detection of capability leaks in stock android smartphones. In NDSS, (Vol. 14 p. 19). Grace, M.C., Zhou, Y., Wang, Z., & Jiang, X. (2012). Systematic detection of capability leaks in stock android smartphones. In NDSS, (Vol. 14 p. 19).
Zurück zum Zitat Guo, Q. (2010). A formal approach to the role mining problem. PhD thesis, Rutgers University-Graduate School-Newark. Guo, Q. (2010). A formal approach to the role mining problem. PhD thesis, Rutgers University-Graduate School-Newark.
Zurück zum Zitat Ongtang, M., McLaughlin, S., Enck, W., & McDaniel, P. (2012). Semantically rich application-centric security in android. Security and Communication Networks, 5(6), 658–673.CrossRef Ongtang, M., McLaughlin, S., Enck, W., & McDaniel, P. (2012). Semantically rich application-centric security in android. Security and Communication Networks, 5(6), 658–673.CrossRef
Zurück zum Zitat Shabtai, A., Fledel, Y., Kanonov, U., Elovici, Y., Dolev, S., & Glezer, C. (2010). Google android: a comprehensive security assessment. IEEE Security & Privacy, 8(2), 35–44.CrossRef Shabtai, A., Fledel, Y., Kanonov, U., Elovici, Y., Dolev, S., & Glezer, C. (2010). Google android: a comprehensive security assessment. IEEE Security & Privacy, 8(2), 35–44.CrossRef
Zurück zum Zitat Shin, W., Kiyomoto, S., Fukushima, K., & Tanaka, T. (2010). A formal model to analyze the permission authorization and enforcement in the Android framework. In Proc. - socialcom 2010: 2nd IEEE international conference on social computing, PASSAT 2010: 2nd IEEE International Conference on Privacy, Security, Risk and Trust (pp. 944–951). Shin, W., Kiyomoto, S., Fukushima, K., & Tanaka, T. (2010). A formal model to analyze the permission authorization and enforcement in the Android framework. In Proc. - socialcom 2010: 2nd IEEE international conference on social computing, PASSAT 2010: 2nd IEEE International Conference on Privacy, Security, Risk and Trust (pp. 944–951).
Zurück zum Zitat Talegaon, S., & Krishnan, R. (2019). A formal specification of access control in android. In International Conference on Secure Knowledge Management in Artificial Intelligence Era (pp. 101–125): Springer. Talegaon, S., & Krishnan, R. (2019). A formal specification of access control in android. In International Conference on Secure Knowledge Management in Artificial Intelligence Era (pp. 101–125): Springer.
Zurück zum Zitat Taylor, V.F., & Martinovic, I. (2016). Quantifying permission-creep in the google play store. arXiv:160601708. Taylor, V.F., & Martinovic, I. (2016). Quantifying permission-creep in the google play store. arXiv:160601708.
Zurück zum Zitat Tuncay, G.S., Demetriou, S., Ganju, K., & Gunter, C.A. (2018). Resolving the predicament of android custom permissions. In Proc. 2018 Network and Distributed System Security Symposium. Reston: Internet Society. Tuncay, G.S., Demetriou, S., Ganju, K., & Gunter, C.A. (2018). Resolving the predicament of android custom permissions. In Proc. 2018 Network and Distributed System Security Symposium. Reston: Internet Society.
Zurück zum Zitat Vaidya, J., Atluri, V., & Warner, J. (2006). Roleminer: mining roles using subset enumeration. In Proceedings of the 13th ACM conference on Computer and communications security (pp. 144–153). Vaidya, J., Atluri, V., & Warner, J. (2006). Roleminer: mining roles using subset enumeration. In Proceedings of the 13th ACM conference on Computer and communications security (pp. 144–153).
Zurück zum Zitat Vaidya, J., Atluri, V., & Guo, Q. (2007). The role mining problem: finding a minimal descriptive set of roles. In Proceedings of the 12th ACM symposium on Access control models and technologies (pp. 175–184). Vaidya, J., Atluri, V., & Guo, Q. (2007). The role mining problem: finding a minimal descriptive set of roles. In Proceedings of the 12th ACM symposium on Access control models and technologies (pp. 175–184).
Zurück zum Zitat Vaidya, J., Atluri, V., & Guo, Q. (2010). The role mining problem: a formal perspective. ACM Transactions on Information and System Security (TISSEC), 13(3), 1–31.CrossRef Vaidya, J., Atluri, V., & Guo, Q. (2010). The role mining problem: a formal perspective. ACM Transactions on Information and System Security (TISSEC), 13(3), 1–31.CrossRef
Zurück zum Zitat Wei, X., Gomez, L., Neamtiu, I., & Faloutsos, M. (2012). Permission evolution in the android ecosystem. In Proc. of the 28th Annual Computer Security Applications Conference (pp. 31–40). Wei, X., Gomez, L., Neamtiu, I., & Faloutsos, M. (2012). Permission evolution in the android ecosystem. In Proc. of the 28th Annual Computer Security Applications Conference (pp. 31–40).
Metadaten
Titel
A Formal Specification of Access Control in Android with URI Permissions
verfasst von
Samir Talegaon
Ram Krishnan
Publikationsdatum
14.11.2020
Verlag
Springer US
Erschienen in
Information Systems Frontiers / Ausgabe 4/2021
Print ISSN: 1387-3326
Elektronische ISSN: 1572-9419
DOI
https://doi.org/10.1007/s10796-020-10066-9

Weitere Artikel der Ausgabe 4/2021

Information Systems Frontiers 4/2021 Zur Ausgabe

Premium Partner