论文标题
用于正式规格和验证Android权限系统安全属性的框架
A Framework for Formal Specification and Verification of Security Properties of the Android Permissions System
论文作者
论文摘要
Android是一种广泛部署的操作系统，采用了基于许可的访问控制模型。 Android权限系统（APS）负责调解应用程序的资源请求。 APS是Android安全机制的关键组成部分。 AP的设计失败可能会导致漏洞，这些漏洞通过恶意应用程序授予未经授权访问资源的访问。研究人员采用了正式方法来分析AP的安全性。由于Android正在不断发展，我们打算设计和实施一个框架，以正式规范和验证AP的安全属性。特别是，我们打算提出一个AP的行为模型，该模型代表Android 10中引入的非二元，上下文依赖性权限以及Android 11中引入的时间权限。
Android is a widely deployed operating system that employs a permission-based access control model. The Android Permissions System (APS) is responsible for mediating resource requests from applications. APS is a critical component of the Android security mechanism. A failure in the design of APS can potentially lead to vulnerabilities that grant unauthorized access to resources by malicious applications. Researchers have employed formal methods for analyzing the security properties of APS. Since Android is constantly evolving, we intend to design and implement a framework for formal specification and verification of the security properties of APS. In particular, we intend to present a behavioral model of APS that represents the non-binary, context dependent permissions introduced in Android 10 and temporal permissions introduced in Android 11.
