Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
(Two scenarios) Scenario A: Multiple applications from the same developer define the same permission into distinct permission-levels and/or permission-groups; this is a valid condition, but, only the first application’s definition of the permission counts whereas the rest are ignored.
Scenario B: Multiple applications from different developers define the same permission into distinct permission-levels and/or permission-groups; this condition is invalid, since only one developer is allowed to define a new permission at any given time. However, once that application gets uninstalled, other applications from different developers are able to define the same permission!
References
Android permission protection level “normal” are never re-granted! (2019). https://issuetracker.google.com/issues/129029397. Accessed 21 Mar 2019
Android Permissions|Android Open Source Project (2019). https://source.android.com/devices/tech/config. Accessed 17 June 2019
Issue about Android’s permission to permission-group mapping (2019). https://issuetracker.google.com/issues/128888710. Accessed 21 Mar 2019
Request App Permissions|Android Developers (2019). https://developer.android.com/training/permissions/requesting/. Accessed 12 Mar 2019
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). https://doi.org/10.1007/978-3-319-19249-9_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)
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)
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)
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)
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). https://doi.org/10.1007/978-3-319-25150-9_28
Enck, W., Ongtang, M., McDaniel, P.: Understanding android security. IEEE Secur. Priv. 7(1), 50–57 (2009)
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). https://doi.org/10.1007/978-3-642-33167-1_1
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)
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)
Acknowledgements
This work is partially supported by DoD ARO Grant W911NF-15-1-0518, NSF CREST Grant HRD-1736209 and NSF CAREER Grant CNS-1553696.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Talegaon, S., Krishnan, R. (2020). A Formal Specification of Access Control in Android. In: Sahay, S., Goel, N., Patil, V., Jadliwala, M. (eds) Secure Knowledge Management In Artificial Intelligence Era. SKM 2019. Communications in Computer and Information Science, vol 1186. Springer, Singapore. https://doi.org/10.1007/978-981-15-3817-9_7
Download citation
DOI: https://doi.org/10.1007/978-981-15-3817-9_7
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-15-3816-2
Online ISBN: 978-981-15-3817-9
eBook Packages: Computer ScienceComputer Science (R0)