An interactive approach to mobile app verification.

ABSTRACT Static explicit information flow analysis can help human auditors find malware. We propose a process for eliminating false positive flows due to imprecision in the reachability analysis: the developer provides tests cases, and only tested code is analyzed. Then, the app is instrumented so that executing untested code terminates the app. We use abductive inference to minimize the instrumentation, and interact with the developer to ensure that only unreachable code is instrumented. Our verification process successfully discharges 11 out of the 12 false positives in a corpus of 77 Android apps.