Toward Automated Verification of Static Analysis Results of Android Applications
This program is tentative and subject to change.
Static analysis techniques are widely employed to detect security vulnerabilities in Android applications. However, because static analysis approximates program execution, it can produce false positives by reporting cases in which no actual privacy leak occurs. Therefore, verification of analysis results is necessary. In Android’s event-driven execution model, certain leaks occur only under specific event sequences, making it difficult to determine whether a reported leak is feasible. This paper proposes a technique for automatically generating and testing event sequences necessary to validate the results of static analysis tools. The proposed method first analyzes the pre-conditions that must be satisfied before a callback function causing a leak can execute. It then iteratively searches for other callback functions whose post-conditions satisfy these pre-conditions, constructing an event execution sequence that leads to the leak. For future work, we plan to enable automatic verification of static analysis results through automated testing based on the generated event sequences. We hope that our approach can significantly reduce the time spent for verifying the results of existing Android static analyzers.