Towards a certified reference monitor of the Android 10 permission system
Guido De Luca, Carlos Luna

TL;DR
This paper formalizes and verifies a reference model of Android's permission system across multiple versions using Coq, ensuring correctness and analyzing security properties of recent Android releases.
Contribution
It provides an enhanced formal specification and certified implementation of Android's permission system in Coq, covering versions from Nougat to Android 10.
Findings
Revalidated or refuted previous security properties
Formulated and proved new security properties
Developed a certified reference validation mechanism
Abstract
Android is a platform for mobile devices that captures more than 85% of the total market-share. 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 (LNCS 10855, https://doi.org/10.1007/978-3-319-94460-9_16), we exhibited a formal specification of an idealized formulation of the permission model of version \texttt{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 on versions Nougat, Oreo, Pie and 10. The properties that we had proved earlier for the security model has been either revalidated or refuted, and new…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
