Current dynamic analysis tools for Android applications do not get good code coverage since they can only explore a subset of the behaviors of the applications and do not have full control over the environment in which they execute. In this work we use model checking to systematically explore application paths while reducing the analysis size using state matching and backtracking. In particular, we extend the Java PathFinder (JPF) model checking environment for Android. We describe the difficulties one needs to overcome to make this a reality as well as our current approaches to handling these issues. We obtain significantly higher coverage using shorter event sequences on a representative sample of Android apps, when compared to Dynodroid and Sapienz, the current state-of-the-art dynamic analysis tools for Android applications.
Reference:
Botha, H-M., Tkachuk, O., Van der Merwe, B. et al. 2017. Addressing challenges in obtaining high coverage when model checking android applications. Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 13-14 July 2017, Santa Barbara, California, USA, pp. 31-40
Botha, H., Tkachuk, O., Van der Merwe, B., & Visser, W. (2017). Addressing challenges in obtaining high coverage when model checking android applications. ACM Digital Library. http://hdl.handle.net/10204/9601
Botha, Heila-Marie, O Tkachuk, B Van der Merwe, and W Visser. "Addressing challenges in obtaining high coverage when model checking android applications." (2017): http://hdl.handle.net/10204/9601
Botha H, Tkachuk O, Van der Merwe B, Visser W, Addressing challenges in obtaining high coverage when model checking android applications; ACM Digital Library; 2017. http://hdl.handle.net/10204/9601 .
Copyright: 2017 ACM. Due to copyright restrictions, the attached PDF file only contains the abstract of the full text item. For access to the full text item, kindly consult the publisher's website.
ResearchSpace
