Eventually Sound Points-To Analysis with Missing Code

TL;DR

This paper introduces Optix, a points-to analysis for Android apps with missing framework code, which guarantees eventual soundness through runtime checks with low overhead, improving malware detection.

Contribution

It presents a novel approach that combines static analysis with runtime checks to achieve eventual soundness in the presence of missing code.

Findings

Optix incurs low runtime overhead on real Android apps.

It guarantees soundness after finite counterexamples.

Improves malware detection accuracy in Android applications.

Abstract

Static analyses make the increasingly tenuous assumption that all source code is available for analysis; for example, large libraries often call into native code that cannot be analyzed. We propose a points-to analysis that initially makes optimistic assumptions about missing code, and then inserts runtime checks that report counterexamples to these assumptions that occur during execution. Our approach guarantees eventual soundness, i.e., the static analysis is sound for the available code after some finite number of counterexamples. We implement Optix, an eventually sound points-to analysis for Android apps, where the Android framework is missing. We show that the runtime checks added by Optix incur low overhead on real programs, and demonstrate how Optix improves a client information flow analysis for detecting Android malware.