跟着白泽读论文丨Flaws in Security-Focused Static Analysis*

跟着白泽读论文丨Flaws in Security-Focused Static Analysis*

转载请注明出处,侵权必究。

Flaws in Security-Focused Static Analysis Tools for Android using Systematic Mutation

本文发表于USENIX Security 2018,作者均来自美国著名公立大学威廉玛丽学院。

1. 主要内容

近年来,在安卓静态污点分析方面的研究越来越多,产生了许多的分析工具。为了验证工具的实践性和正确性,对于分析工具进行系统性的性能评估和漏洞发现也成为了当下研究的重要方向。发表于ESEC/FSE 2018的论文《Do Android Taint Analysis Tools Keep their Promises》,其主要内容是验证分析工具是否达到了它们在各自论文中宣称的性能水平。而本篇论文重点则是发现分析工具是否存在未被记录或未被发现的漏洞 。这些漏洞与以往的认知不同,是指分析工具在实践中不能处理但未被记录的情况,即后文所说的unsound decision。记录这些漏洞的存在有利于在之后的研究工作中合理地利用这些工具。

2. 背景介绍

一般研究认为静态分析工具都是健壮(soundy)的,即在unsound decision的范围之外静态分析工具拥有实践上可行的分析能力。这里所指的unsound decision是指该分析工具宣称其不处理或无法处理的方面,例如大多数的静态分析工具不处理有关java reflection的情况,这就属于一个unsound decision。在unsound decision范围之外的部分定义为sound core,即分析工具能够处理的范畴。sound core与unsound decision的关系如下图1所示。扩大sound core的范围,等同于增强工具的健壮性,这是显而易见的。

Figure 1 unsound decision与sound core

实践中发现,有些静态分析工具不能处理的情况却未被记录到unsound decision中,因此会产生不可预知的错误。本文主要目标就是发现更多unsound decision,从而扩大sound core的范围,增强工具的健壮性。

本文设计并实现了基于突变的健壮性评估框架(简称μSE),该框架可以用于发现分析工具存在的漏洞(指静态分析工具不能处理的情况却未被记录到unsound decision)。

μSE主要利用了软件工程中突变分析的方法。将已有的APK文件结合突变因子作为输入,在Mutation Engine模块进行突变。产生的突变APK则作为新的测试套件用于评估。其主要流程如下图2所示。

Figure 2 突变分析流程

3. 框架设计

基于上述流程,μSE的实现框架如下图3所示。

Figure 3 μSE框架

μSE利用其定义的Security operator和Mutation scheme来对已有的APK进行突变,将产生的突变体用于静态分析工具进行测试。对于那些未被工具识别出的突变体,进一步进行人工分析,最后扩大sound core的范围,实现对工具的提升。

突变过程中使用的Security operator和Mutation scheme两者相结合即为对APK产生突变的规则。前者用于确定在app中插入怎样的突变,而后者则决定了这些突变插入的位置。

Security operator由静态分析工具的安全目标决定,本文主要分析以数据泄露检测为安全目标的工具,因此Security operator就是data leak detection。如下图4是Security operator的一个实例。

Figure 4 Security operator实例

Mutation scheme由三条规则决定。

第一条规则是代码可达性分析,在每个函数的开头都插入operator用来分析即可实现。

第二条规则是Android Abstraction,针对的是安卓APP的语言特性,主要包括Activity与Fragment生命周期、回调函数、Intent messages和安卓资源文件等四个方面。在对应的代码片段插入operator即可检测工具能否正确处理有关android语言特性的相关情况。

第三条规则是Security goal,这里主要包括两种情况:第一种情况,对于污点分析工具,检测其是否能够解决回调函数异步执行。实现方法是将数据泄露的source和sink分别置于不同的回调函数中,若工具仍能够检测到这种泄露的存在,则证明工具具有处理回调函数异步执行情况的能力。第二种情况,静态分析工具在分析call graph时有时跳了任意步后会自动停止,为了验证这种情况是否能被解决,实现方法是将source和sink之间的路径尽可能复杂,从而验证工具对复杂路径的处理能力。

4. 框架实现

基于以上的设计思想,最终μSE的实现如下图5所示。首先利用Security operator和Mutation scheme对已有APK进行突变,对于产生的mutated APK放入Execution Engine以检测APK能够被正确执行,过滤掉不能执行的突变体,将剩余突变体交给分析工具进行测试。最后对于那些不能被识别的突变体进行人工分析,最终记录漏洞或者对漏洞打补丁。

Figure 5 框架实现

5. 评估

本文对于多个安卓静态分析工具进行了测试,部分测试结果如下图6所示。可见每个测试工具都有检测不到的突变体,因此可以确定它们都存在未被记录的漏洞。

Figure 6 测试结果1

对于测试出的未被记录的漏洞,本文将其分为4类,如下图7所示。

Figure 7 测试结果2

本文对于漏洞的传播进行了进一步的检测,即一个存在漏洞的分析工具被后续工作使用时,其漏洞在后续工作中可能仍然存在。这里主要观察的工具是FlowDroid,检查的目标分为四类,第一是FlowDroid不同版本之间的漏洞传播,第二是将FlowDroid作为黑盒利用的工具,第三是受FlowDroid启发的工具,第四是实现了其单独的设计的工具。其实验结果如下图8所示。

实验表明,工具的漏洞确实会在后续的工作中传播。尤其当FlowDroid作为黑盒使用时,所有的漏洞都会被传递到之后的工作中。

Figure 8 测试结果3

6. 缺陷

μSE虽然在实验中颇有成效,但是仍存在不足之处。第一,μSE不能代替formal verification。μSE只能尽可能发现更多的unsound decision,从而扩大sound core的范围,因此不能宣称通过μSE测试的工具就是sound的。第二,μSE仍需要一些人力工作,当mutated APK不能被工具识别时需要进行人工分析,无法做到完全自动化检测。第三,μSE在Execution Engine方面可能存在问题,例如有些APP可能需要特定环境才可以运行,因此过滤掉的样本可能过多,从而使得一些漏洞仍无法被检测到。


文 章 | Wisher, LKK, DR.XX

排 版 | Amber

编辑于 2019-07-17 13:02