On The Unsoundness of Static Analysis for Android GUIs
Android software presents exciting new challenges for the static analysis community. However, static analyses for Android are typ- ically unsound. This is due to the lack of specification of the An- droid framework, the continuous evolution of framework features and behavior, and the absence of soundness arguments and stud- ies by program analysis researchers. Our goal is to investigate one important aspect of this problem: the static modeling of con- trol/data flow due to interactions of the user with the application’s GUI. We compare the solutions of three existing static analyses— FlowDroid, IccTA, and GATOR—with the actual run-time behav- ior. Specifically, we observe the run-time sequences of callbacks and their parameters, and match them against the static abstractions provided by these analyses. This study provides new insights into the unsoundness of existing analysis techniques. We conclude with open questions and action items for program analysis researchers working in this increasingly important area.
Tue 14 JunDisplayed time zone: Tijuana, Baja California change
13:30 - 15:00
|Invited Talk: Machine-code analysis and transformation at GrammaTech|
Matt Noonan GrammaTech, Inc
|On The Unsoundness of Static Analysis for Android GUIs|
|Verifying Precise Floating-Point Optimizations in LLVM|