一种针对Android权限模型的已认证引用验证机制
编程语言
2017-09-13 v1 密码学与安全
摘要
Android在操作系统和应用程序层面都体现了安全机制。在该平台上，应用安全主要构建于一套权限系统之上，这些权限规定了对特定进程可执行操作的限制。这些安全机制的关键作用使其成为（形式化）验证的主要目标。我们提出了Android 6（及更高版本）新机制的参考监视器的理想化模型，其中可以在运行时授予权限。利用证明辅助工具Coq的编程语言，我们开发了参考验证机制的函数式实现，并针对指定的参考监视器证明了其正确性。关于Android 6权限模型及其安全机制的若干性质已被形式化表述并证明。应用Coq提供的程序提取机制，我们还推导出了参考验证机制的已认证Haskell原型。
引用
@article{arxiv.1709.03652,
title = {A certified reference validation mechanism for the permission model of Android},
author = {Gustavo Betarte and Juan Campo and Felipe Gorostiaga and Carlos Luna},
journal= {arXiv preprint arXiv:1709.03652},
year = {2017}
}
备注
Pre-proceedings paper presented at the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017), Namur, Belgium, 10-12 October 2017 (arXiv:1708.07854)