论文标题
迈向Android 10许可系统的认证参考监视器
Towards a certified reference monitor of the Android 10 permission system
论文作者
论文摘要
Android是移动设备的平台，可捕获总市场份额的85％以上。目前，移动设备允许人们在不同领域开发多个任务。遗憾的是，使用移动设备的好处通过增加安全风险来抵消。这些系统的重要和关键作用使它们成为正式验证的主要目标。在我们以前的工作（LNCS 10855，https://doi.org/10.1007/978-3-319-94460-9_16）中，我们对Android的版本\ texttt {6}版本的许可模型进行了理想化的配方。在本文中，我们在证明辅助的COQ中介绍了该模型的增强版本，包括有关在牛轧糖，奥利奥，派和10版中引入的权限系统的最相关的更改。我们先前证明的安全模型已证明的属性已被重新验证或驳斥，并已制定和证明。此外，我们对Android最新版本的安全性进行了观察。使用COQ的编程语言，我们开发了参考验证机制的功能实现，并证明了其正确性。正式的开发约为COQ的23K LOC，包括证明。
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 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.
