Abstract
The ever increasing expansion of mobile applications into nearly every aspect of modern life, from banking to healthcare systems, is making their security more important than ever. Modern smartphone operating systems (OS) rely substantially on the permission-based security model to enforce restrictions on the operations that each application can perform. In this paper, we perform an analysis of the permission protocol implemented in Android, a popular OS for smartphones. We propose a formal model of the Android permission protocol in Alloy, and describe a fully automatic analysis that identifies potential flaws in the protocol. A study of real-world Android applications corroborates our finding that the flaws in the Android permission protocol can have severe security implications, in some cases allowing the attacker to bypass the permission checks entirely.
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
Preview
Unable to display preview. Download preview PDF.
References
Felt, A.P., Chin, E., Hanna, S., Song, D., Wagner, D.: Android permissions demystified. In: 18th ACM Conference on Computer and Communications Security (CCS), pp. 627–638 (2011)
Davi, L., Dmitrienko, A., Sadeghi, A.-R., Winandy, M.: Privilege escalation attacks on android. In: Burmester, M., Tsudik, G., Magliveras, S., Ilić, I. (eds.) ISC 2010. LNCS, vol. 6531, pp. 346–360. Springer, Heidelberg (2011)
Pandita, R., Xiao, X., Yang, W., Enck, W., Xie, T.: Whyper: Towards automating risk assessment of mobile applications. In: Proceedings of the 22nd USENIX Conference on Security, SEC 2013, pp. 527–542. USENIX Association, Berkeley (2013)
Grace, M., Zhou, Y., Wang, Z., Jiang, X.: Systematic detection of capability leaks in stock android smartphones. In: Proceedings of the 19th Annual Symposium on Network and Distributed System Security (2012)
Schlegel, R., Zhang, K., Zhou, X., Intwala, M., Kapadia, A., Wang, X.: Soundcomber: A stealthy and context-aware sound trojan for smartphones. In: Proc. of 18th Annual Network and Distributed System Security Symposium, NDSS (2011)
Enck, W., Octeau, D., McDaniel, P., Chaudhuri, S.: A study of android application security. In: Proc. of USENIX (2011)
Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: Practice and experience. ACM Comput. Surv. 41(4), 19:1–19:36 (2009)
Bagheri, H., Sadeghi, A., Garcia, J., Malek, S.: Covert: Compositional analysis of android inter-app permission leakage. IEEE Transactions on Software Engineering (2015)
Jackson, D.: Software Abstractions: Logic, Language, and Analysis, 2nd edn. MIT Press (2012)
Google: Android system permissions, http://developer.android.com/guide/topics/security/permissions.html
Andoni, A., Daniliuc, D., Khurshid, S., Marinov, D.: Evaluating the small scope hypothesis, http://sdg.csail.mit.edu/pubs/2002/SSH.pdf
Felt, A.P., Wang, H.J., Moshchuk, A., Hanna, S., Chin, E.: Permission re-delegation: Attacks and defenses. In: 20th USENIX Security Symposium (2011)
Mark Murphy: Vulnerabilities with custom permissions (2014), http://commonsware.com/blog/2014/02/12/vulnerabilities-custom-permissions.html
Shin, W., Kiyomoto, S., Fukushima, K., Tanaka, T.: A formal model to analyze the permission authorization and enforcement in the android framework. In: IEEE International Conference on Privacy, Security, Risk and Trust, pp. 944–951 (2010)
Fragkaki, E., Bauer, L., Jia, L., Swasey, D.: Modeling and enhancing android’s permission system. In: 17th European Symposium on Research in Computer Security (ESORICS), pp. 1–18 (2012)
Chin, E., Felt, A.P., Greenwood, K., Wagner, D.: Analyzing inter-application communication in android. In: Proceedings of the 9th International Conference on Mobile Systems, Applications, and Services, MobiSys 2011. ACM, New York, pp. 239–252 (2011)
Octeau, D., McDaniel, P., Jha, S., Bartel, A., Bodden, E., Klein, J., Traon, Y.L.: Effective Inter-Component Communication Mapping in Android with Epicc: An Essential Step Towards Holistic Security Analysis. In: Proceedings of the 22nd USENIX Security Symposium, Washington, DC (August 2013)
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: Proc. of USENIX OSDI (2011)
Arzt, S., Rasthofer, S., Bodden, E., Bartel, A., Klein, J., Le Traon, Y., Octeau, D., McDaniel, P.: Flowdroid: Precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for android apps. In: Proceedings of the 35th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014 (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Bagheri, H., Kang, E., Malek, S., Jackson, D. (2015). Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification. In: Bjørner, N., de Boer, F. (eds) FM 2015: Formal Methods. FM 2015. Lecture Notes in Computer Science(), vol 9109. Springer, Cham. https://doi.org/10.1007/978-3-319-19249-9_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-19249-9_6
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19248-2
Online ISBN: 978-3-319-19249-9
eBook Packages: Computer ScienceComputer Science (R0)