A formal approach for detection of security flaws in the android permission system
A formal approach for detection of security flaws in the android permission system
复制标题
DOI：
10.1007/s00165-017-0445-z
复制
发表时间：
2018-09-01
影响因子：
1
通讯作者：
Jackson, Daniel
中科院分区：
文献类型：
--
作者：
Bagheri, Hamid;Kang, Eunsuk;Jackson, Daniel
移动应用日益扩展到现代生活的几乎方方面面，从银行到医疗系统，这使得它们的安全比以往任何时候都更加重要。现代智能手机操作系统(OS)在很大程度上依赖于基于权限的安全模型来对每个应用程序可以执行的操作实施限制。在本文中，我们对流行的智能手机操作系统Android中实现的许可协议进行了分析。文中提出了一种Android许可协议的形式化模型，并描述了一种识别协议中潜在缺陷的全自动分析。一项对现实世界中Android应用程序的研究证实了我们的发现，即Android权限协议中的缺陷可能会产生严重的安全影响，在某些情况下，允许攻击者完全绕过权限检查。
The ever increasing expansion of mobile applications into nearly every aspect of modern life, from banking to healthcare systems, is making their security more important than ever. Modern smartphone operating systems (OS) rely substantially on the permission-based security model to enforce restrictions on the operations that each application can perform. In this paper, we perform an analysis of the permission protocol implemented in Android, a popular OS for smartphones. We propose a formal model of the Android permission protocol in Alloy, and describe a fully automatic analysis that identifies potential flaws in the protocol. A study of real-world Android applications corroborates our finding that the flaws in the Android permission protocol can have severe security implications, in some cases allowing the attacker to bypass the permission checks entirely.