Formalization of Android Activity-Fragment Multitasking Mechanism and Static Analysis of Mobile Apps

The multitasking mechanism between activities and fragments plays a fundamental role in the Android operating system, which involves a wide range of features, including launch modes, intent flags, task affinities, and structured activities containing fragments. All of them are being widely used in Android apps, both open source and commercial ones. In this article, we present a formal semantics of the Android multitasking mechanism between activities and fragments, which accommodates all the important features and gives insofar the most comprehensive and accurate formalization. In particular, our semantics is formulated based on multi-stack systems, and fully captures the behavior of task stacks and activity stacks regarding fragments. Based on the semantics, we provide new static analysis algorithms, which are both multi-stack aware and fragment sensitive, thus achieve more precise static analysis for Android apps. We validate our approach by extensive experiments on both open source and commercial Android apps. The results highlight the benefits of the considering the semantics of the multitasking mechanism between activities and fragments in static analysis, and confirm the efficacy of our approach.