Document Type : Research Article
Authors
1 Faculty of Computer Engineering, Department of Software Engineering, University of Isfahan, Isfahan, Iran.
2 MDSE Research Group, Department of Software Engineering, University of Isfahan, Isfahan, Iran.
Abstract
Android is a widely used operating system that employs a permission-based access control model. The Android Permissions System (APS) is responsible for mediating application resource requests. APS is a critical component of the Android security mechanism; hence, a failure in the design of APS can potentially lead to vulnerabilities that grant unauthorized access to resources by malicious applications. In this paper, we present a formal approach for modeling and verifying the security properties of APS. We demonstrate the usability of the proposed approach by showcasing the detection of a well-known
vulnerability found in Android’s custom permissions.
Keywords
[1] Ren´e Mayrhofer, Jeffrey Vander Stoep, Chad Brubaker, and Nick Kralevich. The Android Platform Security Model. ACM Transactions on Privacy and Security, 24(3):35, 2021.
[2] Parnika Bhat and Kamlesh Dutta. A Survey on Various Threats and Current State of Security in Android Platform. ACM Computing Surveys, 52(1):35, 2019. Publisher: ACM New York, NY, USA.
[3] G¨uliz Seray Tuncay, Soteris Demetriou, Karan Ganju, and Carl A. Gunter. Resolving the Predicament of Android Custom Permissions. In Proceedings of the Network and Distributed System Security Symposium, NDSS ’18, page 15, San Diego, CA, USA, 2018. The Internet Society. Publisher: Internet Society.
[4] Hamid Bagheri, Eunsuk Kang, Sam Malek, and Daniel Jackson. A Formal Approach for Detection of Security Flaws in the Android Permission System. Formal Aspects of Computing, 30(5):525–544, 2018. Publisher: Springer.
[5] Rui Li, Wenrui Diao, Zhou Li, Shishuai Yang, Shuang Li, and Shanqing Guo. Android Custom Permissions Demystified: A Comprehensive Security Evaluation. IEEE Transactions on Software Engineering, Early Access:20, 2021. Publisher: IEEE.
[6] Samir Talegaon and Ram Krishnan. A Formal Specification of Access Control in Android with URI Permissions. Information Systems Frontiers, page 18, 2020. Publisher: Springer.
[7] Wook Shin, Shinsaku Kiyomoto, Kazuhide Fukushima, and Toshiaki Tanaka. Towards Formal Analysis of the Permission-Based Security Model for Android. In Proceedings of the International Conference on Wireless and Mobile Communications, ICWMC ’09, pages 87–92, Cannes/La Bocca, France, 2009. IEEE.
[8] Hamid Bagheri, Alireza Sadeghi, Joshua Garcia, and Sam Malek. COVERT: Compositional Analysis of Android Inter-App Permission Leakage. IEEE Transactions on Software Engineering, 41(9):866–886, 2015. Conference Name: IEEE Transactions on Software Engineering.
[9] Gustavo Betarte, Juan Campo, Carlos Luna, and Agust´ın Romano. Formal Analysis of Android’s Permission-Based Security Model. Scientific Annals of Computer Science, 26(1):27–68, 2016.
[10] Iman M. Almomani and Aala Al Khayer. A Comprehensive Analysis of the Android Permissions System. IEEE Access, 8:216671–216688, 2020. Publisher: IEEE.
[11] Bradley Schmerl, Jeff Gennari, Alireza Sadeghi, Hamid Bagheri, Sam Malek, Javier C´amara, and David Garlan. Architecture Modeling and Analysis of Security in Android Systems. In Bedir Tekinerdogan, Uwe Zdun, and Ali Babar, editors, Proceedings of the European Conference on Software Architecture, ECSA ’16, pages 274–290, Copenhagen, Denmark, 2016. Springer.
[12] Alireza Sadeghi, Reyhaneh Jabbarvand, Negar Ghorbani, Hamid Bagheri, and Sam Malek. A Temporal Permission Analysis and Enforcement Framework for Android. In Proceedings of the International Conference on Software Engineering, ICSE ’18, pages 846–857, Gothenburg, Sweden, 2018. ACM.
[13] Samir Talegaon and Ram Krishnan. Role-Based Access Control Models for Android. In Proceedings of the International Conference on Trust, Privacy and Security in Intelligent Systems and Applications, TPS-ISA ’2020, pages 179–188, Atlanta, GA, USA, 2020. IEEE.
[14] Samir Talegaon and Ram Krishnan. A Formal Specification of Access Control in Android. In Sanjay K. Sahay, Nihita Goel, Vishwas Patil, and Murtuza Jadliwala, editors, Proceedings of the International Conference on Secure Knowledge Management in Artificial Intelligence Era, volume 1186 of SKM ’19, pages 101–125, Goa, India, 2020. Springer.
[15] Roger S. Pressman and Bruce Maxim. Software Engineering: A Practitioner’s Approach. McGraw Hill, New York, NY, 8th edition edition, 2014.
[16] G. Blake Meike and Lawrence Schiefer. Inside the Android OS: Building, Customizing, Managing and Operating Android System Services. Addison-Wesley Professional, Hoboken, 1st edition edition, 2021.
[17] Efthimios Alepis and Constantinos Patsakis. Unravelling Security Issues of Runtime Permissions in Android. Journal of Hardware and Systems Security, 3(1):45–63, 2019.
[18] Gustavo Betarte, Juan Campo, Carlos Luna, Camila Sanz, Felipe Gorostiaga, and Maximiliano Cristi´a. A Formal Approach for the Verification of the Permission-Based Security Model of Android. CLEI Electronic Journal, 21(2):21, 2018.
[19] Hamid Bagheri, Eunsuk Kang, Sam Malek, and Daniel Jackson. Detection of Design Flaws in the Android Permission Protocol through Bounded Verification. In Proceedings of the International Symposium on Formal Methods, FM ’15, pages
73–89, Oslo, Norway, 2015. Springer.
[20] Gustavo Betarte, Juan Campo, Felipe Gorostiaga, and Carlos Luna. A Certified Reference Validation Mechanism for the Permission Model of Android. In Fabio Fioravanti and John P. Gallagher, editors, Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR ’17, pages 271–288, Namur, Belgium, 2018. Springer.
[21] Gustavo Betarte, Juan Campo, Maximiliano Cristi´a, Felipe Gorostiaga, Carlos Luna, and Camila Sanz. Towards Formal Model-Based Analysis and Testing of Android’s Security Mechanisms. In Proceedings of the Latin American Computer Conference, CLEI ’17, pages 1–10, Cordoba, Argentina, 2017. IEEE.
[22] Xudong He. Modeling and Analyzing the Android Permission Framework Using High-Level Petri Nets. In Proceedings of the International Conference on Software Quality, Reliability and Security, QRS ’17, pages 232–239, Prague, Czech
Republic, 2017. IEEE.
[23] Alireza Sadeghi. Efficient Permission-Aware Analysis of Android Applications. Doctoral Dissertation, University of California, Irvine, Irvine, CA, USA, 2017.
[24] Alessandro Armando, Gabriele Costa, and Alessio Merlo. Formal Modeling and Reasoning about the Android Security Framework. In Catuscia Palamidessi and Mark D. Ryan, editors, Proceedings of the International Symposium on Trustworthy Global Computing, TGC ’12, pages 64–81, Newcastle upon Tyne, UK, 2013. Springer.
[25] Elli Fragkaki, Lujo Bauer, Limin Jia, and David
Swasey. Modeling and Enhancing Android’s Permission System. In Proceedings of the European Symposium on Research in Computer Security, ESORICS ’12, page 18, Pisa, Italy, 2012. Springer.
[2] Parnika Bhat and Kamlesh Dutta. A Survey on Various Threats and Current State of Security in Android Platform. ACM Computing Surveys, 52(1):35, 2019. Publisher: ACM New York, NY, USA.
[3] G¨uliz Seray Tuncay, Soteris Demetriou, Karan Ganju, and Carl A. Gunter. Resolving the Predicament of Android Custom Permissions. In Proceedings of the Network and Distributed System Security Symposium, NDSS ’18, page 15, San Diego, CA, USA, 2018. The Internet Society. Publisher: Internet Society.
[4] Hamid Bagheri, Eunsuk Kang, Sam Malek, and Daniel Jackson. A Formal Approach for Detection of Security Flaws in the Android Permission System. Formal Aspects of Computing, 30(5):525–544, 2018. Publisher: Springer.
[5] Rui Li, Wenrui Diao, Zhou Li, Shishuai Yang, Shuang Li, and Shanqing Guo. Android Custom Permissions Demystified: A Comprehensive Security Evaluation. IEEE Transactions on Software Engineering, Early Access:20, 2021. Publisher: IEEE.
[6] Samir Talegaon and Ram Krishnan. A Formal Specification of Access Control in Android with URI Permissions. Information Systems Frontiers, page 18, 2020. Publisher: Springer.
[7] Wook Shin, Shinsaku Kiyomoto, Kazuhide Fukushima, and Toshiaki Tanaka. Towards Formal Analysis of the Permission-Based Security Model for Android. In Proceedings of the International Conference on Wireless and Mobile Communications, ICWMC ’09, pages 87–92, Cannes/La Bocca, France, 2009. IEEE.
[8] Hamid Bagheri, Alireza Sadeghi, Joshua Garcia, and Sam Malek. COVERT: Compositional Analysis of Android Inter-App Permission Leakage. IEEE Transactions on Software Engineering, 41(9):866–886, 2015. Conference Name: IEEE Transactions on Software Engineering.
[9] Gustavo Betarte, Juan Campo, Carlos Luna, and Agust´ın Romano. Formal Analysis of Android’s Permission-Based Security Model. Scientific Annals of Computer Science, 26(1):27–68, 2016.
[10] Iman M. Almomani and Aala Al Khayer. A Comprehensive Analysis of the Android Permissions System. IEEE Access, 8:216671–216688, 2020. Publisher: IEEE.
[11] Bradley Schmerl, Jeff Gennari, Alireza Sadeghi, Hamid Bagheri, Sam Malek, Javier C´amara, and David Garlan. Architecture Modeling and Analysis of Security in Android Systems. In Bedir Tekinerdogan, Uwe Zdun, and Ali Babar, editors, Proceedings of the European Conference on Software Architecture, ECSA ’16, pages 274–290, Copenhagen, Denmark, 2016. Springer.
[12] Alireza Sadeghi, Reyhaneh Jabbarvand, Negar Ghorbani, Hamid Bagheri, and Sam Malek. A Temporal Permission Analysis and Enforcement Framework for Android. In Proceedings of the International Conference on Software Engineering, ICSE ’18, pages 846–857, Gothenburg, Sweden, 2018. ACM.
[13] Samir Talegaon and Ram Krishnan. Role-Based Access Control Models for Android. In Proceedings of the International Conference on Trust, Privacy and Security in Intelligent Systems and Applications, TPS-ISA ’2020, pages 179–188, Atlanta, GA, USA, 2020. IEEE.
[14] Samir Talegaon and Ram Krishnan. A Formal Specification of Access Control in Android. In Sanjay K. Sahay, Nihita Goel, Vishwas Patil, and Murtuza Jadliwala, editors, Proceedings of the International Conference on Secure Knowledge Management in Artificial Intelligence Era, volume 1186 of SKM ’19, pages 101–125, Goa, India, 2020. Springer.
[15] Roger S. Pressman and Bruce Maxim. Software Engineering: A Practitioner’s Approach. McGraw Hill, New York, NY, 8th edition edition, 2014.
[16] G. Blake Meike and Lawrence Schiefer. Inside the Android OS: Building, Customizing, Managing and Operating Android System Services. Addison-Wesley Professional, Hoboken, 1st edition edition, 2021.
[17] Efthimios Alepis and Constantinos Patsakis. Unravelling Security Issues of Runtime Permissions in Android. Journal of Hardware and Systems Security, 3(1):45–63, 2019.
[18] Gustavo Betarte, Juan Campo, Carlos Luna, Camila Sanz, Felipe Gorostiaga, and Maximiliano Cristi´a. A Formal Approach for the Verification of the Permission-Based Security Model of Android. CLEI Electronic Journal, 21(2):21, 2018.
[19] Hamid Bagheri, Eunsuk Kang, Sam Malek, and Daniel Jackson. Detection of Design Flaws in the Android Permission Protocol through Bounded Verification. In Proceedings of the International Symposium on Formal Methods, FM ’15, pages
73–89, Oslo, Norway, 2015. Springer.
[20] Gustavo Betarte, Juan Campo, Felipe Gorostiaga, and Carlos Luna. A Certified Reference Validation Mechanism for the Permission Model of Android. In Fabio Fioravanti and John P. Gallagher, editors, Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR ’17, pages 271–288, Namur, Belgium, 2018. Springer.
[21] Gustavo Betarte, Juan Campo, Maximiliano Cristi´a, Felipe Gorostiaga, Carlos Luna, and Camila Sanz. Towards Formal Model-Based Analysis and Testing of Android’s Security Mechanisms. In Proceedings of the Latin American Computer Conference, CLEI ’17, pages 1–10, Cordoba, Argentina, 2017. IEEE.
[22] Xudong He. Modeling and Analyzing the Android Permission Framework Using High-Level Petri Nets. In Proceedings of the International Conference on Software Quality, Reliability and Security, QRS ’17, pages 232–239, Prague, Czech
Republic, 2017. IEEE.
[23] Alireza Sadeghi. Efficient Permission-Aware Analysis of Android Applications. Doctoral Dissertation, University of California, Irvine, Irvine, CA, USA, 2017.
[24] Alessandro Armando, Gabriele Costa, and Alessio Merlo. Formal Modeling and Reasoning about the Android Security Framework. In Catuscia Palamidessi and Mark D. Ryan, editors, Proceedings of the International Symposium on Trustworthy Global Computing, TGC ’12, pages 64–81, Newcastle upon Tyne, UK, 2013. Springer.
[25] Elli Fragkaki, Lujo Bauer, Limin Jia, and David
Swasey. Modeling and Enhancing Android’s Permission System. In Proceedings of the European Symposium on Research in Computer Security, ESORICS ’12, page 18, Pisa, Italy, 2012. Springer.
)