Verification Of The Correctness Of Static Taint Analysis For Privacy Leakage Of Android Application

With the popularity of smart phones,mobile Internet has become an indispensable part of people's life.Android attracts a large number of application developers and mobile phone users with its open features,and is also the mobile operating system with the highest market share.Meanwhile,Android apps are facing more and more security threats.User privacy leakage is the most common and major security problem in Android apps,and also a research hotspot in the field of Android security.Taint analysis is one of the main methods to detect privacy leakage.Taint analysis can be divided into dynamic,static and mixed analysis.Static analysis refers to scanning the code without actually running the code,extracting its lexical,grammatical and semantic,and further realizing control flow analysis and data flow analysis,so as to help developers find structural errors and security vulnerabilities in the program.Dynamic analysis is to obtain the control flow and data flow of the program by executing the program on the real or virtual processor,monitoring the program execution,and using the method of instrument during the execution process,and to discover the errors or potential vulnerability attacks during the program execution.Static analysis code has high coverage rate and low false positive rate,but the context information of program running cannot be obtained,resulting in high false negative rate.While dynamic analysis can accurately identify program vulnerabilities or verify static code analysis results,but the code coverage is low.This paper propose a method for automatically verifying the correctness of taint analysis results.First,instrument and run the APP to obtain a seed trace covering the Source and Sink,and then perform taint analysis to determine whether there is a taint propagation path in the trace.This indicates that the analysis result is correct,otherwise the conditional constraints and taint information of the Trace are collected,and the live variable information is combined.Analyze and program transformation methods,design constraint selection strategy,pruning and traversing the executable path set to determine whether there is a taint propagation path,and then verify whether the analysis result is false.Based on the FlowDroid framework to implement the prototype system,the experimental results of DroidBench and real APK show that the method is effective.