A Sound Flow-Sensitive Heap Abstraction for the Static Analysis of Android Applications

TL;DR

This paper introduces a sound, flow-sensitive heap abstraction for static analysis of Android apps, enhancing precision in information flow analysis while maintaining soundness and scalability.

Contribution

It presents a novel flow-sensitive heap abstraction formalized with Horn clauses, integrated into HornDroid, improving analysis precision without losing soundness.

Findings

Improved analysis precision on DroidBench

Maintained soundness guarantees

Moderate efficiency cost

Abstract

The present paper proposes the first static analysis for Android applications which is both flow-sensitive on the heap abstraction and provably sound with respect to a rich formal model of the Android platform. We formulate the analysis as a set of Horn clauses defining a sound over-approximation of the semantics of the Android application to analyse, borrowing ideas from recency abstraction and extending them to our concurrent setting. Moreover, we implement the analysis in HornDroid, a state-of-the-art information flow analyser for Android applications. Our extension allows HornDroid to perform strong updates on heap-allocated data structures, thus significantly increasing its precision, without sacrificing its soundness guarantees. We test our implementation on DroidBench, a popular benchmark of Android applications developed by the research community, and we show that our changes to HornDroid lead to an improvement in the precision of the tool, while having only a moderate cost in terms of efficiency. Finally, we assess the scalability of our tool to the analysis of real applications.