A type and effect system for activation flow of components in Android programs

•We design a formal semantics for a core of featherweight Android/Java.•We design a type and effect system for activation flow analysis in Android programs.•We prove the soundness of our system with respect to the formal semantics.•Our system is a static verification of faithful implementations for UI flow design.•Activation flow is important for analysis of data flow or secure information flow.

This paper proposes a type and effect system for analyzing activation flow between components through intents in Android programs. The activation flow information is necessary for all Android analyses such as a secure information flow analysis for Android programs. We first design a formal semantics for a core of featherweight Android/Java, which can address interaction between components through intents. Based on the formal semantics, we design a type and effect system for analyzing activation flow between components and demonstrate the soundness of the system.