DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2020.3

Towards a Certified Reference Monitor of the Android 10 Permission System

Authors: Guido De Luca and Carlos Luna

Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{deluca_et_al:LIPIcs.TYPES.2020.3,
  author =	{De Luca, Guido and Luna, Carlos},
  title =	{{Towards a Certified Reference Monitor of the Android 10 Permission System}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{3:1--3:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.3},
  URN =		{urn:nbn:de:0030-drops-138821},
  doi =		{10.4230/LIPIcs.TYPES.2020.3},
  annote =	{Keywords: Android, Permission model, Formal idealized model, Reference monitor, Formal proofs, Certified implementation, Coq}
}

Search Results

Documents authored by De Luca, Guido

Towards a Certified Reference Monitor of the Android 10 Permission System

Abstract

Cite as

Thanks for your feedback!

Could not send message