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.