期刊文献+

面向Android应用的静态污点分析结果的正确性验证 被引量:1

Correctness verification of static taint analysis results for Android application
下载PDF
导出
摘要 应用静态污点分析检测Android应用的隐私泄露漏洞会产生许多虚警,为此提出一种上下文敏感、路径敏感和域敏感的半自动程序分析方法,仅需遍历少量执行路径即可判定漏洞是否虚警。首先,运行插桩后的应用来获得一条覆盖Source和Sink的种子Trace。然后,应用基于Trace的污点分析方法来验证Trace中是否存在污点传播路径,是则表明漏洞真实存在;否则进一步收集Trace的条件集合和污点信息,结合活变量分析和基于条件反转的程序变换方法设计约束选择策略,以删除大部分与污点传播无关的可执行路径。最后,遍历剩余执行路径并分析相应Trace来验证漏洞是否虚警。基于FlowDroid实现原型系统,对DroidBench的75个应用和10个真实应用进行验证,每个应用平均仅需遍历15.09%的路径,虚警率平均降低58.17%。实验结果表明该方法可以较高效地减少静态分析结果的虚警。 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 only15.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.
作者 秦彪 郭帆 涂风涛 QIN Biao;GUO Fan;TU Fengtao(College of Computer Information Engineering, Jiangxi Normal University,Nanchang Jiangxi 330022, China;Department of Computer Science, Yuzhang Normal University, Nanchang Jiangxi 330103,China)
出处 《计算机应用》 CSCD 北大核心 2019年第10期3018-3027,共10页 journal of Computer Applications
基金 国家自然科学基金资助项目(61562040,61762049) 江西省教育厅科技项目(GJJ161305,GJJ151330)~~
关键词 程序验证 污点分析 活变量分析 程序变换 路径敏感 program verification taintanalysis live-variable analysis programtransformation path sensitive
  • 相关文献

参考文献4

二级参考文献30

  • 1景涛,江昌海,胡德斌,白成刚,蔡开元.软件关联缺陷的一种检测方法[J].软件学报,2005,16(1):17-28. 被引量:23
  • 2Binkley D. Source code analysis: A road map I-C] //Proc of the Future of Software Engineering. Piscataway, NJ: IEEE, 2007: 104-119.
  • 3Rice H. Classes of recursively enumerable sets and their decision problems [J]. Transactions of the American Mathematical Society, 1953, 74(2): 358-366.
  • 4Le W, Soffa M L. Path-based fault correlations [C]//International Symp on Foundations of Software Engineering. New Yorkz ACM, 2010:307-316.
  • 5Clarke E, Grumberg O, Jha S, et al. Counter example- guided abstraction refinement [C]//Proe of the 12th International Conf on Computer Aided Verification. Berlin: Springer, 2000:154-169.
  • 6Weiser M. Program slicing [C] //Proc of Int Conf on Software Engineering. Piscataway, NJ: IEEE, 1981:439- 449.
  • 7Silva J. A vocabulary of program slicing-based techniques [OL]. [2012-03-19]. http://users, dsic. upv. es/- jsilva/ papers/Vocabulary, pdf.
  • 8Jeannet B, Mine A. Apron: A library of numerical abstract domains for static analysis [C] //Proc of the 21st Int Conf on Computer Aided Verification. Berlin Springer, 2009: 661- 667.
  • 9Mine A. The octagon abstract domain [J]. Higher-Order and Symbolic Computation, 2006, 19(1): 31-100.
  • 10King J. Symbolic execution and program testing [J]. Communications of the ACM, 1976, 19(7):385-394.

共引文献61

同被引文献14

引证文献1

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部