面向Android应用的静态污点分析结果的正确性验证

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

Correctness verification of static taint analysis results for Android application

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.