面向 Android 10 权限系统的认证参考监视器
密码学与安全
2020-11-03 v1
摘要
Android 是一个占据超过 85% 总市场份额的移动设备平台。当前，移动设备允许人们在多个不同领域执行多种任务。遗憾的是，使用移动设备带来的便利被日益增长的安全风险所抵消。这些系统的重要与关键作用使其成为形式化验证的主要目标。在我们先前的工作（LNCS 10855, https://doi.org/10.1007/978-3-319-94460-9_16）中，我们展示了 Android 第 6 版权限模型理想化表述的形式化规范。在本文中，我们在证明辅助工具 Coq 中提出了该模型的增强版本，包含了 Nougat、Oreo、Pie 和 10 版本中引入的关于权限系统的最相关变更。我们早先针对安全模型证明的性质已被重新验证或反驳，并且新的性质已被提出并证明。此外，我们对最新版本 Android 的安全性做出了观察。利用 Coq 的编程语言，我们开发了参考验证机制的函数式实现并认证了其正确性。该形式化开发约为 23k 行 Coq 代码，包含证明。
引用
@article{arxiv.2011.00720,
title = {Towards a certified reference monitor of the Android 10 permission system},
author = {Guido De Luca and Carlos Luna},
journal= {arXiv preprint arXiv:2011.00720},
year = {2020}
}
备注
arXiv admin note: substantial text overlap with arXiv:1709.03652