CrashSafe: a formal model for proving crash-safety of Android applications

Each software application running on Android powered devices consists of application components that communicate with each other to support application's functionality for enhanced user experience of mobile computing. Application components inside Android system communicate with each other using inter-component communication mechanism based on messages called intents. An android application crashes if it invokes an intent that can not be received by (or resolved to) any application on the device. Application crashes represent a severe fault that relates to compromised users' experience, consequently resulting in decreased ratings, usage trends and revenues for such applications. To address this issue--by formally proving crash-safety property of Android applications--we have defined a formal model of Android inter-component communication using Coq theorem prover. The mathematical model defined in theorem prover allows one to prove the properties of inter-component communication system and check the correctness of the proof in an automated way. To demonstrate the significance of the formal model developed, we carried proof of crash-safety of Android applications using Coq tool. The proposed solution named CrashSafe supports a formal approach that enables one to (i) check the correctness of inter-component communication in Android systems and (ii) establish a formal foundation for other tools to assess Android applications' reliability and safety.