本文是来自University of California, Irvine的Alireza Sadeghi发表在ICSE ‘18的工作。

Abstract: Permission-induced attacks, i.e., security breaches enabled by permission misuse, are among the most critical and frequent issues threatening the security of Android devices. By ignoring the temporal aspects of an attack during the analysis and enforcement, the state-of-the-art approaches aimed at protecting the users against such attacks are prone to have low-coverage in detection and high-disruption in prevention of permission-induced attacks. To address this shortcomings, we present Terminator, a temporal permission analysis and enforcement framework for Android. Leveraging temporal logic model checking,Terminator’s analyzer identifies permission-induced threats with respect to dynamic permission states of the apps. At runtime, Terminator’s enforcer selectively leases (i.e., temporarily grants) permissions to apps when the system is in a safe state, and revokes the permissions when the system moves to an unsafe state realizing the identified threats. The results of our experiments, conducted over thousands of apps, indicate that Terminator is able to provide an effective, yet non-disruptive defense against permission-induced attacks. We also show that our approach, which does not require modification to the Android framework or apps’ implementation logic, is highly reliable and widely applicable.

Entry：Zotero link URL link

Motivation and Problem Formulation

• What is the high-level problem?
  • 特权升级
    • 借用有相应权限的中间应用进行攻击（串通攻击）
    • 要求两个或多个同时运行，且中间应用需要被授权
  • PendingIntent泄露
    • PendingIntent允许应用在未来执行Intent，但需要发送权限和UID等信息
    • 甚至不要求中间应用运行，中间应用权限被撤销也行
  • 相同名称的自定义权限
    • 不同应用如果申明了相同名称的自定义权限，会导致泄露
  • 被动数据泄露
    • 应用程序没有正确保护包含敏感数据的内部数据库
• What is missing from previous works?
  • 分析和执行过程中忽略了攻击的时间特性，导致检测覆盖率低、防御效果差的问题
  • Android系统的高度动态性，现有的防御技术会产生大量的误报，影响用户的正常使用
• 为了解决现有方法的不足，本文提出了TERMINATOR框架
  • 通过引入时间逻辑模型检查，能够在运行时动态地授予和撤销应用程序的权限，从而提供一种有效且不会干扰用户正常使用的防御方法。

Design

• 形式化建模
  • 首先只考虑权限和App两者进行形式化描述给出Kripke结构图
  • 
  • 然后对安全规则进行线性时间时态逻辑定义
  • 
  • 可以发现授权是关键路径，所以可以考虑当从应用程序接收到权限请求时，只有在授予请求的权限不违反任何安全规则的情况下，TERMINATOR才会将该权限暂时授予给请求者。一旦系统状态的变化可能导致违反安全规则，就会自动撤销租用的权限。
• 框架模型
  • 
  • 分析阶段
    • 使用TLA (Temporal Logic of Actions)及其扩展TLA+编写的公式
    • 在发现违规的情况下，它会报告从导致不安全状态的初始状态开始的最小长度跟踪。这些不安全的跟踪信息被存储在Android设备的不安全跟踪数据库中。
  • 执行阶段
    • 使用Xpose作为数据监控，监控事件的示例包括但不限于:通过权限请求对话框授予/撤销权限，通过系统设置授予/撤销权限，运行或终止应用程序。
    • 追踪到不安全的Trace时，Model Checker会进行风险打分
    • 使用安卓的API动态限制高风险权限
  • 本文介绍了对真实Android应用程序进行的实验，以评估TERMINATOR框架的有效性。实验结果表明，TERMINATOR在防止权限引发的攻击方面比其他技术成功率高达68％，同时发出的虚警数量显著较少。它还对权限保护的应用程序功能的可用性造成的干扰较小。

Evaluations

• Environment
  • 分析阶段：PC，执行阶段：Android 6.0
• How they evaluate their method?
  • 性能、可靠性、准确度、对使用的破坏性、覆盖率
  • 实验结果显示，TERMINATOR能够防止所有攻击场景，没有漏报。其他技术在防止权限引发的攻击方面的成功率在31.7％到65.9％之间。大部分未能检测到的攻击是需要进行时间分析才能检测到的。例如，攻击场景＃36涉及恶意应用程序访问存储在易受攻击应用程序中的敏感信息，只有在恶意软件在受害者应用程序之前安装时才能利用。因此，先前的非时间方法无法检测到此类攻击。

Pros / Cons

• Pros:
  • 论文逻辑非常清晰，从建模中发现解决问题的关键，然后依靠它设计了一套机制
  • 考虑攻击的时间特性，区别于之前的所有工作
  • 工作很完善，实验数据和对比分析详实

Last modified on 2023-05-17