Document Open Access Logo

Towards a Certified Reference Monitor of the Android 10 Permission System

Authors Guido De Luca, Carlos Luna

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2020.3.pdf
  • Filesize: 0.76 MB
  • 18 pages

Document Identifiers

Author Details

Guido De Luca
  • Universidad Nacional de Rosario, Argentina
Carlos Luna
  • InCo, Facultad de Ingeniería, Universidad de la República, Montevideo, Uruguay

Cite AsGet BibTex

Guido De Luca and Carlos Luna. Towards a Certified Reference Monitor of the Android 10 Permission System. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.TYPES.2020.3

Abstract

Android is a platform for mobile devices that captures more than 85% of the total market share [International Data Corporation (IDC), 2020]. Currently, mobile devices allow people to develop multiple tasks in different areas. Regrettably, the benefits of using mobile devices are counteracted by increasing security risks. The important and critical role of these systems makes them a prime target for formal verification. In our previous work [Betarte et al., 2018], we exhibited a formal specification of an idealized formulation of the permission model of version 6 of Android. In this paper we present an enhanced version of the model in the proof assistant Coq, including the most relevant changes concerning the permission system introduced in versions Nougat, Oreo, Pie and 10. The properties that we had proved earlier for the security model have been either revalidated or refuted, and new ones have been formulated and proved. Additionally, we make observations on the security of the most recent versions of Android. Using the programming language of Coq we have developed a functional implementation of a reference validation mechanism and certified its correctness. The formal development is about 23k LOC of Coq, including proofs.

Subject Classification

ACM Subject Classification
  • Security and privacy → Systems security
  • Theory of computation → Proof theory
Keywords
  • Android
  • Permission model
  • Formal idealized model
  • Reference monitor
  • Formal proofs
  • Certified implementation
  • Coq

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. J. 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. Application Fundamentals. Available at: http://developer.android.com/guide/components/fundamentals.html. Last access: Feb. 2021
  3. Android Developers. Permissions. Available at: http://developer.android.com/guide/topics/security/permissions.html. Last access: Feb. 2021
  4. Android Developers. Protection levels. Available at: https://developer.android.com/guide/topics/permissions/overview#normal-dangerous. Last access: Feb. 2021
  5. H. Bagheri, A. Sadeghi, J. Garcia, and S. Malek. Covert: Compositional analysis of android inter-app permission leakage. IEEE Transactions on Software Engineering, 41(9):866-886, September 2015. URL: https://doi.org/10.1109/TSE.2015.2419611.
  6. 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, November 2017. URL: https://doi.org/10.1007/s00165-017-0445-z.
  7. A. Balaa and Y. Bertot. Fix-point equations for well-founded recursion in type theory. In M. Aagaard and J. Harrison, editors, TPHOLs, volume 1869 of LNCS, pages 1-16. Springer, 2000. URL: https://doi.org/10.1007/3-540-44659-1_1.
  8. G. Barthe, J. Forest, D. Pichardie, and V. Rusu. Defining and reasoning about recursive functions: A practical tool for the coq proof assistant. In M. Hagiya and P. Wadler, editors, FLOPS, volume 3945 of LNCS, pages 114-129. Springer, 2006. URL: https://doi.org/10.1007/11737414_9.
  9. Stefan Berghofer, Lukas Bulwahn, and Florian Haftmann. Turning inductive into equational specifications. In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, TPHOLs, volume 5674 of LNCS, pages 131-146. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_11.
  10. Gustavo Betarte, Juan Campo, Felipe Gorostiaga, and Carlos Luna. A Certified Reference Validation Mechanism for the Permission Model of Android: 27th International Symposium, LOPSTR 2017, Namur, Belgium, October 10-12, 2017, Revised Selected Papers. Springer, July 2018. URL: https://doi.org/10.1007/978-3-319-94460-9_16.
  11. P. Chester, C. Jones, M. Wiem Mkaouer, and D. E. Krutz. M-perm: A lightweight detector for android permission gaps. In 2017 IEEE/ACM 4th International Conference on Mobile Software Engineering and Systems (MOBILESoft), pages 217-218, May 2017. URL: https://doi.org/10.1109/MOBILESoft.2017.23.
  12. E. De Angelis, F. Fioravanti, A. Pettorossi, and M. Proietti. Program verification via iterated specialization. Sci. Comput. Program., 95:149-175, 2014. URL: https://doi.org/10.1016/j.scico.2014.05.017.
  13. Michael Gordon, Kim deokhwan, Jeff Perkins, Limei Gilham, Nguyen Nguyen, and Martin Rinard. Information-flow analysis of android applications in droidsafe. In NDSS Symposium 2015, January 2015. URL: https://doi.org/10.14722/ndss.2015.23089.
  14. International Data Corporation (IDC). Smartphone market share. Technical report, International Data Corporation (IDC), 2020. Google Scholar
  15. Daniel Jackson. Software Abstractions: Logic, Language, and Analysis. The MIT Press, 2012. Google Scholar
  16. Wilayat Khan, Habib Ullah, Aakash Ahmad, Khalid Sultan, Abdullah Alzahrani, Sultan Khan, Mohammad Alhumaid, and Sultan Abdulaziz. Crashsafe: a formal model for proving crash-safety of android applications. Human-centric Computing and Information Sciences, 8, December 2018. URL: https://doi.org/10.1186/s13673-018-0144-7.
  17. P. Letouzey. Programmation fonctionnelle certifiée - L'extraction de programmes dans l'assistant Coq. PhD thesis, Université Paris-Sud, July 2004. Google Scholar
  18. Pierre Letouzey. A New Extraction for Coq. In Proceedings of TYPES'02, volume 2646 of LNCS, 2003. Google Scholar
  19. Guido De Luca and Carlos Luna. Formal verification of the security model of Android 10: Coq code. Available at: https://github.com/g-deluca/android-coq-model. Last access: Feb. 2021
  20. Guido De Luca and Carlos Luna. Towards a certified reference monitor of the android 10 permission system. CoRR, abs/2011.00720, 2020. URL: http://arxiv.org/abs/2011.00720.
  21. Carlos Luna, Gustavo Betarte, Juan Diego Campo, Camila Sanz, Maximiliano Cristiá, and Felipe Gorostiaga. A formal approach for the verification of the permission-based security model of android. CLEI Electron. J., 21(2), 2018. URL: https://doi.org/10.19153/cleiej.21.2.3.
  22. René Mayrhofer, Jeffrey Vander Stoep, Chad Brubaker, and Nick Kralevich. The android platform security model. CoRR, abs/1904.05572, 2019. URL: http://arxiv.org/abs/1904.05572.
  23. Damien Octeau, Daniel Luchaup, Matthew Dering, Somesh Jha, and Patrick McDaniel. Composite constant propagation: Application to android inter-component communication analysis. In Proceedings of the 37th International Conference on Software Engineering - Volume 1, ICSE '15, pages 77-88, Piscataway, NJ, USA, 2015. IEEE Press. URL: http://dl.acm.org/citation.cfm?id=2818754.2818767.
  24. Open Handset Alliance. Android project. Available at: https://source.android.com/. Last access: Feb. 2021
  25. W. Shin, S. Kiyomoto, K. Fukushima, and T. Tanaka. A formal model to analyze the permission authorization and enforcement in the android framework. In SocialCom'10, pages 944-951, Washington, DC, USA, 2010. IEEE Computer Society. URL: https://doi.org/10.1109/SocialCom.2010.140.
  26. W. Shin, S. Kiyomoto, K. Fukushima, and T. Tanaka. A frst step towards automated permission-enforcement analysis of the android framework. In SAM 2010, pages 323-329. CSREA Press, 2010. Google Scholar
  27. The Coq Team. The Coq Proof Assistant Reference Manual - Version V8.12.0, 2020. URL: http://coq.inria.fr.
  28. P.-N. Tollitte, D. Delahaye, and C. Dubois. Producing certified functional code from inductive specifications. In Chris Hawblitzel and Dale Miller, editors, CPP, volume 7679 of LNCS, pages 76-91. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-35308-6_9.
  29. Fengguo Wei, Sankardas Roy, Xinming Ou, and Robby. Amandroid: A precise and general inter-component data flow analysis framework for security vetting of android apps. ACM Transactions on Privacy and Security, 21:1-32, April 2018. URL: https://doi.org/10.1145/3183575.
  30. S. Wu and J. Liu. Overprivileged permission detection for android applications. In ICC 2019 - 2019 IEEE International Conference on Communications (ICC), pages 1-6, May 2019. URL: https://doi.org/10.1109/ICC.2019.8761572.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact