Formal Analysis of Android’s Permission-Based Security Model

Published in Volume XXVI, Issue 1, 2016, pages 27-68, doi: 10.7561/SACS.2016.1.27

Authors: G. Betarte, J. Campo, C. Luna, A. Romano

Abstract

In this work we present a comprehensive formal specification of an idealized formulation of Android?s permission model. Permissions in Android are basically tags that developers declare in their applications, more precisely in the so-called application manifest, to gain access to sensitive resources. Several analyses have recently been carried out concerning the security of the Android system. Few of them, however, pay attention to the formal aspects of the permission enforcing framework. We provide a complete and uniform formulation of several security properties using the higher order logic of the Calculus of Inductive Constructions and sketch the proofs that have been developed and verified using the Coq proof assistant. We also analyze how the changes introduced in the latest version of Android, that allows to manage permissions at runtime, impact the presented model.

Full Text (PDF)

References

[1] James P. Anderson. Computer Security technology planning study. Technical report, Deputy for Command and Management System, USA, 1972. URL: http://csrc.nist.gov/publications/history/ande72. pdf.

[2] Android Developers. Android KitKat. Available at: https://developer.android.com/about/versions/kitkat.html. Last access: July 2016.

[3] Android Developers. Application Fundamentals. Available at: http://developer.android.com/guide/components/ fundamentals.html. Last access: July 2016.

[4] Android Developers. Application Manifest. Available at: http://developer. android.com/guide/topics/manifest/manifest-intro.html. Last access: July 2016.

[5] Android Developers. Context. Available at: http://developer.android.com/reference/android/content/Context.html. Last access: July 2016.

[6] Android Developers. . Available at: http://developer.android.com/guide/topics/manifest/manifest-element.html# uid. Last access: July 2016.

[7] Android Developers. Permissions. Available at: http://developer.android.com/guide/topics/security/permissions.html. Last access: July 2016.

[8] Android Developers. Requesting Permissions at Run Time. Available at: https://developer.android.com/intl/es/training/ permissions/requesting.html. Last access: July 2016.

[9] Android Developers. R.styleable. Available at: http://developer.android.com/reference/android/R.styleable.html. Last access: July 2016.

[10] Android Developers. Security Tips. Available at: http://developer.android.com/training/articles/security-tips.html. Last access: July 2016.

[11] Android Developers. Services. Available at: http://developer.android.com/guide/components/services.html. Last access: July 2016.

[12] Android Open Source Project. Android Security Overview. http://source.android.com/devices/tech/security/index.html. Last access: July 2016.

[13] June Andronick. Modélisation et Vérification Formelles de Systèmes Embarqués dans les Cartes à Microprocesseur – Plate-Forme Java Card et Système d’Exploitation. PhD thesis, Université Paris-Sud, 2006.

[14] Alessandro Armando, Gabriele Costa, and Alessio Merlo. Formal modeling and reasoning about the Android security framework. In Catuscia Palamidessi and Mark Dermot Ryan, editors, Trustworthy Global Computing – 7th International Symposium, TGC 2012, Newcastle upon Tyne, UK, September 7-8, 2012, Revised Selected Papers, volume 8191 of Lecture Notes in Computer Science, pages 64-81. Springer, 2012. doi:10.1007/978-3-642-41157-1_5.

[15] Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Jesús Mauricio Chimento, and Carlos Luna. Formally verified implementation of an idealized model of virtualization. In Ralph Matthes and Aleksy Schubert, editors, 19th International Conference on Types for Proofs and Programs, TYPES 2013, April 22-26, 2013, Toulouse, France, volume 26 of LIPIcs, pages 45-63. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 2013. doi:10.4230/LIPIcs.TYPES.2013.45.

[16] Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. Formal certification of code-based cryptographic proofs. SIGPLAN Not., 44(1):90-101, January 2009. doi:10.1145/1594834.1480894.

[17] Santiago Zanella Béguelin, Gustavo Betarte, and Carlos Luna. A formal specification of the MIDP 2.0 security model. In Theodosis Dimitrakos, Fabio Martinelli, Peter Y. A. Ryan, and Steve A. Schneider, editors, Formal Aspects in Security and Trust, Fourth International Workshop, FAST 2006, Hamilton, Ontario, Canada, August 26-27, 2006, Revised Selected Papers, volume 4691 of LNCS, pages 220-234. Springer, 2006. doi:10.1007/978-3-540-75227-1_15.

[18] D. E. Bell and L. J. LaPadula. Secure computer systems: Mathematical foundations. Technical Report MTR-2547, Vol. 1, MITRE Corp., Bedford, MA, 1973.

[19] Yves Bertot, Pierre Castéran, Gérard (informaticien) Huet, and Chris- tine Paulin-Mohring. Interactive theorem proving and program development : Coq-Art : the calculus of inductive constructions. Texts in theoretical computer science. Springer, Berlin, New York, 2004. Données complémentaires http://coq.inria.fr. URL: http://opac.inria.fr/record=b1101046.

[20] G. Betarte, E. Giménez, C. Loiseaux, and B. Chetali. FORMAVIE: Formal Modeling and Verification of the Java Card 2.1.1 Security Architecture. In Proceedings of eSmart-02, 2002.

[21] Gustavo Betarte, Juan Diego Campo, Carlos Daniel Luna, and Agustín Romano. Verifying Android’s permission model. In Martin Leucker, Camilo Rueda, and Frank D. Valencia, editors, Theoretical Aspects of Computing – ICTAC 2015 – 12th International Colloquium Cali, Colombia, October 29-31, 2015, Proceedings, volume 9399 of Lecture Notes in Computer Science, pages 485-504. Springer, 2015. doi:10. 1007/978-3-319-25150-9_28.

[22] Michele Bugliesi, Stefano Calzavara, and Alvise Spanò. Lintent: Towards security type-checking of Android applications. In Proceedings of Formal Techniques for Distributed Systems – Joint IFIP WG 6.1 International Conference, FMOODS/FORTE 2013, pages 289-304, Berlin, Heidelberg, 2013. Springer. doi:10.1007/978-3-642-38592-6_20.

[23] Avik Chaudhuri. Language-based security on Android. In Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, PLAS ’09, pages 1-7, New York, NY, USA, 2009. ACM. doi:10.1145/1554339.1554341.

[24] Boutheina Chetali and Quang-Huy Nguyen. About the world-first smart card certificate with EAL7 formal assurances. Slides 9th ICCC, Jeju, Korea, September 2008. Available at: http://www.commoncriteriaportal.org/iccc/9iccc/pdf/B2404.pdf.

[25] Erika Chin, Adrienne Porter Felt, Kate Greenwood, and David Wagner. Analyzing inter-application communication in Android. In Proceedings of the 9th International Conference on Mobile Systems, Applications, and Services, MobiSys ’11, pages 239-252, New York, NY, USA, 2011. ACM. doi:10.1145/1999995.2000018.

[26] Mauro Conti, Vu Thien Nga Nguyen, and Bruno Crispo. CRePE: context-related policy enforcement for Android. In Proceedings of the 13th international conference on Information security, ISC’10, pages 331-345, Berlin, Heidelberg, 2011. Springer-Verlag. doi:10.1007/ 978-3-642-18178-8_29.

[27] Thierry Coquand and Gerard Huet. The calculus of constructions. Inf. Comput., 76(2-3):95-120, February 1988. doi:10.1016/0890-5401(88) 90005-3.

[28] Lucas Davi, Alexandra Dmitrienko, Ahmad-Reza Sadeghi, and Marcel Winandy. Privilege escalation attacks on Android. In Proceedings of the 13th international conference on Information security, ISC’10, pages 346-360, Berlin, Heidelberg, 2011. Springer-Verlag. doi:10.1007/ 978-3-642-18178-8_30.

[29] Parvez Faruki, Ammar Bharmal, Vijay Laxmi, Vijay Ganmoor, Manoj Singh Gaur, Mauro Conti, and Muttukrishnan Rajarajan. Android security: A survey of issues, malware penetration, and defenses. IEEE Communications Surveys and Tutorials, 17(2):998-1022, 2015. doi:10.1109/COMST.2014.2386139.

[30] Adrienne Porter Felt, Erika Chin, Steve Hanna, Dawn Song, and David Wagner. Android permissions demystified. In Proceedings of the 18th ACM conference on Computer and communications security, CCS ’11, pages 627-638, New York, NY, USA, 2011. ACM. doi:10.1145/2046707.2046779.

[31] Adrienne Porter Felt, Helen J. Wang, Alexander Moshchuk, Steve Hanna, and Erika Chin. Permission re-delegation: Attacks and defenses. In USENIX Security Symposium. USENIX Association, 2011. URL: http://static.usenix.org/events/sec11/tech/full_papers/Felt.pdf.

[32] Elli Fragkaki, Lujo Bauer, Limin Jia, and David Swasey. Modeling and enhancing Android’s permission system. In Sara Foresti, Moti Yung, and Fabio Martinelli, editors, Proceedings of the 17th European Symposium on Research in Computer Security, ESORICS 2012, volume 7459 of Lecture Notes in Computer Science, pages 1-18. Springer, 2012. doi:10.1007/978-3-642-33167-1_1.

[33] Gartner. Gartner says worldwide smartphone sales grew 9.7 percent in fourth quarter of 2015. Technical report, Gartner, Inc., 2016. Available at: http://www.gartner.com/newsroom/id/3215217. Last access: July 2016.

[34] GSI. Formal verification of the security model of Android: Coq code. Available at: http://www.fing.edu.uy/inco/grupos/gsi/documentos/proyectos/modelo.tar.gz. Last access: July 2016.

[35] Xavier Leroy. Formal verification of a realistic compiler. Commun. ACM, 52:107-115, July 2009. doi:10.1145/1538788.1538814.

[36] P. Letouzey. Programmation fonctionnelle certifiée – L’extraction de programmes dans l’assistant Coq. PhD thesis, Université Paris-Sud, July 2004.

[37] Pierre Letouzey. A New Extraction for Coq. In Herman Geuvers and Freek Wiedijk, editors, Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, volume 2646 of LNCS. Springer-Verlag, 2003. doi: 10.1007/3-540-39185-1_12.

[38] Mohammad Nauman, Sohail Khan, and Xinwen Zhang. Apex: extending Android permission model and enforcement with user-defined runtime constraints. In Proceedings of the 5th ACM Symposium on Information, Computer and Communications Security, ASIACCS ’10, pages 328-332, New York, NY, USA, 2010. ACM. doi:10.1145/1755688.1755732.

[39] Open Handset Alliance. Android project. Available at: //source. android.com/. Last access: July 2016.

[40] C. Paulin-Mohring. Inductive definitions in the system Coq – rules and properties. In M. Bezem and J. F. Groote, editors, 1st Int. Conf. on Typed Lambda Calculi and Applications, volume 664 of LNCS, pages 328-345. Springer-Verlag, 1993. doi:10.1007/BFb0037116.

[41] Mariantonietta La Polla, Fabio Martinelli, and Daniele Sgandurra. A survey on security for mobile devices. IEEE Communications Surveys and Tutorials, 15(1):446-471, 2013. doi:10.1109/SURV.2012.013012.00028.

[42] Bahman Rashidi and Carol Fung. A survey of android security threats and defenses. Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA), 6(3):3-35, September 2015. URL: http://isyou.info/jowua/papers/jowua-v6n3-1.pdf.

[43] D. Sbîrlea, M. G. Burke, S. Guarnieri, M. Pistoia, and V. Sarkar. Automatic detection of inter-application permission leaks in Android applications. IBM J. Res. Dev., 57(6):2:10-2:10, November 2013. doi: 10.1147/JRD.2013.2284403.

[44] Wook Shin, Shinsaku Kiyomoto, Kazuhide Fukushima, and Toshiaki Tanaka. A formal model to analyze the permission authorization and enforcement in the Android framework. In Proceedings of the 2010 IEEE Second International Conference on Social Computing, pages 944-951, Washington, DC, USA, 2010. IEEE Computer Society. doi: 10.1109/SocialCom.2010.140.

[45] Jeff Six. Application Security for the Android Platform. O’Reilly Media, 2011.

[46] Guillermo Suarez-Tangil, Juan E. Tapiador, Pedro Peris-Lopez, and Arturo Ribagorda. Evolution, detection and analysis of malware for smart devices. IEEE Communications Surveys and Tutorials, 16(2):961- 987, 2014. doi:10.1109/SURV.2013.101613.00077.

[47] Sufatrio, Darell J. J. Tan, Tong-Wei Chua, and Vrizlynn L. L. Thing. Securing Android: A survey, taxonomy, and challenges. ACM Comput. Surv., 47(4):58:1-58:45, May 2015. doi:10.1145/2733306.

[48] The Coq Development Team. The Coq Proof Assistant Reference Manual Version V8.5, 2016. URL: http://coq.inria.fr.

Bibtex

@article{sacscuza:betarte2016faoapsm,
  title={Formal Analysis of Android's Permission-Based Security Model},
  author={G. Betarte and J. Campo and C. Luna and A. Romano},
  journal={Scientific Annals of Computer Science},
  volume={26},
  number={1},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2016},
  pages={27--68},
  doi={10.7561/SACS.2016.1.27},
  publisher={``A.I. Cuza'' University Press}
}