Journal of Computer Applications ›› 2019, Vol. 39 ›› Issue (10): 3018-3027.DOI: 10.11772/j.issn.1001-9081.2019040644

• Computer software technology • Previous Articles     Next Articles

Correctness verification of static taint analysis results for Android application

QIN Biao1, GUO Fan1, TU Fengtao2   

  1. 1. College of Computer Information Engineering, Jiangxi Normal University, Nanchang Jiangxi 330022, China;
    2. Department of Computer Science, Yuzhang Normal University, Nanchang Jiangxi 330103, China
  • Received:2019-04-17 Revised:2019-06-06 Online:2019-08-21 Published:2019-10-10
  • Supported by:
    This work is partially supported by the National Natural Science Foundation of China (61562040, 61762049), the Science-Technology Project of Education Bureau of Jiangxi Province(GJJ161305, GJJ151330).


秦彪1, 郭帆1, 涂风涛2   

  1. 1. 江西师范大学 计算机信息工程学院, 南昌 330022;
    2. 豫章师范学院 计算机系, 南昌 330103
  • 通讯作者: 郭帆
  • 作者简介:秦彪(1993-),男,江西南昌人,硕士研究生,主要研究方向:信息安全、程序验证;郭帆(1977-),男,江西南昌人,副教授,博士,主要研究方向:网络安全、程序安全;涂风涛(1976-),男,江西南昌人,讲师,硕士,主要研究方向:网络安全。
  • 基金资助:

Abstract: Many false positives are generated when an Android application is detected by static taint analysis to discover potential privacy-leak bugs. For that, a context-sensitive, path-sensitive and field-sensitive semi-auto analysis method was proposed to verify if a potential bug is a true positive by only traversing a few executable paths. Firstly, a seed Trace covering both Source and Sink was obtained manually by running the instrumented application. Then, a Trace-based taint analysis method was used to verify if there was a taint propagating path in the Trace. If there was a taint propagating path, it meaned a real privacy leak bug existed. If not, the conditioin set and taint information of the Trace were further collected, and by combining the live-variable analysis and the program transformation approach based on conditional inversion, a constraint selection policy was designed to prune most executable paths irrelevant to taint propagation. Finally, remaining executable paths were traversed and corresponding Traces were analyzed to verify if the bug is a false positive. Seventy-five applications of DroidBench and ten real applications were tested by a prototype system implemented on FlowDroid. Results show that only 15.09% paths traversed averagely in each application, the false positive rate decreases 58.17% averagely. Experimental results demonstrate the analysis can effectively reduce the false positives generated by static taint analysis.

Key words: program verification, taint analysis, live-variable analysis, program transformation, path sensitive

摘要: 应用静态污点分析检测Android应用的隐私泄露漏洞会产生许多虚警,为此提出一种上下文敏感、路径敏感和域敏感的半自动程序分析方法,仅需遍历少量执行路径即可判定漏洞是否虚警。首先,运行插桩后的应用来获得一条覆盖Source和Sink的种子Trace。然后,应用基于Trace的污点分析方法来验证Trace中是否存在污点传播路径,是则表明漏洞真实存在;否则进一步收集Trace的条件集合和污点信息,结合活变量分析和基于条件反转的程序变换方法设计约束选择策略,以删除大部分与污点传播无关的可执行路径。最后,遍历剩余执行路径并分析相应Trace来验证漏洞是否虚警。基于FlowDroid实现原型系统,对DroidBench的75个应用和10个真实应用进行验证,每个应用平均仅需遍历15.09%的路径,虚警率平均降低58.17%。实验结果表明该方法可以较高效地减少静态分析结果的虚警。

关键词: 程序验证, 污点分析, 活变量分析, 程序变换, 路径敏感

CLC Number: