A Formal Specification of Access Control in Android

  • Samir TalegaonEmail author
  • Ram Krishnan
Conference paper
Part of the Communications in Computer and Information Science book series (CCIS, volume 1186)


A formal specification of any access control system enables deeper understanding of that system and facilitates performing security analysis. In this paper, we provide a comprehensive formal specification of the Android mobile operating system’s access control system, a widely used mobile OS. Prior work is limited in scope, in addition recent developments in Android concerning dynamic runtime permissions require rethinking of its formalization. Our formal specification includes two parts, the User-Initiated Operations (UIOs) and Application-Initiated Operations (AIOs), which are segregated based on the entity that initiates those operation. Formalizing ACiA allowed us to discover many peculiar behaviors in Android’s access control system. In addition to that, we discovered two significant issues with permissions in Android which were reported to Google.


Android Permissions Access control Formal model 



This work is partially supported by DoD ARO Grant W911NF-15-1-0518, NSF CREST Grant HRD-1736209 and NSF CAREER Grant CNS-1553696.


  1. 1.
    Android permission protection level “normal” are never re-granted! (2019). Accessed 21 Mar 2019
  2. 2.
    Android Permissions|Android Open Source Project (2019). Accessed 17 June 2019
  3. 3.
    Issue about Android’s permission to permission-group mapping (2019). Accessed 21 Mar 2019
  4. 4.
    Request App Permissions|Android Developers (2019). Accessed 12 Mar 2019
  5. 5.
    Bagheri, H., Kang, E., Malek, S., Jackson, D.: Detection of design flaws in the android permission protocol through bounded verification. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 73–89. Springer, Cham (2015). Scholar
  6. 6.
    Bagheri, H., Kang, E., Malek, S., Jackson, D.: A formal approach for detection of security flaws in the android permission system. Formal Aspects Computi. 30(5), 525–544 (2018)CrossRefGoogle Scholar
  7. 7.
    Bagheri, H., Sadeghi, A., Garcia, J., Malek, S.: COVERT: compositional analysis of android inter-app permission leakage. IEEE Trans. Softw. Eng. 41(9), 866–886 (2015)CrossRefGoogle Scholar
  8. 8.
    Betarte, G., Campo, J., Cristiá, M., Gorostiaga, F., Luna, C., Sanz, C.: Towards formal model-based analysis and testing of android’s security mechanisms. In: 2017 XLIII Latin American Computer Conference (CLEI), pp. 1–10. IEEE (2017)Google Scholar
  9. 9.
    Betarte, G., Campo, J., Luna, C., Romano, A.: Formal analysis of android’s permission-based security model 1. Sci. Ann. Comput. Sci. 26(1), 27–68 (2016)MathSciNetzbMATHGoogle Scholar
  10. 10.
    Betarte, G., Campo, J.D., Luna, C., Romano, A.: Verifying android’s permission model. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 485–504. Springer, Cham (2015). Scholar
  11. 11.
    Enck, W., Ongtang, M., McDaniel, P.: Understanding android security. IEEE Secur. Priv. 7(1), 50–57 (2009)CrossRefGoogle Scholar
  12. 12.
    Fragkaki, E., Bauer, L., Jia, L., Swasey, D.: Modeling and enhancing android’s permission system. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol. 7459, pp. 1–18. Springer, Heidelberg (2012). Scholar
  13. 13.
    Shin, W., Kiyomoto, S., Fukushima, K., Tanaka, T.: A formal model to analyze the permission authorization and enforcement in the android framework. In: Proceedings - SocialCom 2010: 2nd IEEE International Conference on Social Computing, PASSAT 2010: 2nd IEEE International Conference on Privacy, Security, Risk and Trust, pp. 944–951 (2010)Google Scholar
  14. 14.
    Tuncay, G.S., Demetriou, S., Ganju, K., Gunter, C.A.: Resolving the predicament of android custom permissions. In: Proceedings of the 2018 Network and Distributed System Security Symposium. Internet Society, Reston (2018)Google Scholar

Copyright information

© Springer Nature Singapore Pte Ltd. 2020

Authors and Affiliations

  1. 1.University of Texas at San AntonioSan AntonioUSA

Personalised recommendations