COVERT: Compositional Analysis of Android Inter-App Permission Leakage
COVERT: Compositional Analysis of Android Inter-App Permission Leakage
复制标题
DOI：
10.1109/tse.2015.2419611
复制
发表时间：
2015-09-01
影响因子：
7.4
通讯作者：
Malek, Sam
中科院分区：
文献类型：
--
作者：
Bagheri, Hamid;Sadeghi, Alireza;Malek, Sam
Android是移动的设备最流行的平台。它使用丰富的应用程序间通信系统促进应用程序之间的数据和服务共享。虽然Android权限系统可以控制对资源的访问，但强制执行权限并不足以防止安全违规，因为权限可能会被有意或无意地管理不当。Android在单个应用级别强制执行权限，从而允许多个恶意应用串通并联合收割机合并其权限，或欺骗易受攻击的应用代表它们执行超出其个人权限的操作。在本文中，我们提出了COVERT，Android应用程序间漏洞的组成分析工具。COVERT的分析是模块化的，可以在安装、更新和删除应用程序时对其进行增量分析。它静态分析每个应用程序的反向工程源代码，并以适合正式验证的格式提取相关的安全规范。给定以这种方式提取的规范的集合，形式分析引擎（例如，模型检查器）然后被用于验证对于一起安装的应用程序的组合（持有某些许可并且可能彼此交互）是否安全。我们使用COVERT检查500多个真实世界应用程序的经验证实了它在市场上一些最受欢迎的应用程序中找到应用程序间漏洞的能力。
Android is the most popular platform for mobile devices. It facilitates sharing of data and services among applications using a rich inter-app communication system. While access to resources can be controlled by the Android permission system, enforcing permissions is not sufficient to prevent security violations, as permissions may be mismanaged, intentionally or unintentionally. Android's enforcement of the permissions is at the level of individual apps, allowing multiple malicious apps to collude and combine their permissions or to trick vulnerable apps to perform actions on their behalf that are beyond their individual privileges. In this paper, we present COVERT, a tool for compositional analysis of Android inter-app vulnerabilities. COVERT's analysis is modular to enable incremental analysis of applications as they are installed, updated, and removed. It statically analyzes the reverse engineered source code of each individual app, and extracts relevant security specifications in a format suitable for formal verification. Given a collection of specifications extracted in this way, a formal analysis engine (e.g., model checker) is then used to verify whether it is safe for a combination of applications-holding certain permissions and potentially interacting with each other-to be installed together. Our experience with using COVERT to examine over 500 real-world apps corroborates its ability to find inter-app vulnerabilities in bundles of some of the most popular apps on the market.