Verifying Android applications using Java PathFinder

Botha, Heila-Marié (2017-11-20)

Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences (Computer Science)

Thesis (PhD)--Stellenbosch University, 2017

Thesis

ENGLISH ABSTRACT : Current dynamic analysis tools for Android applications do not achieve acceptable 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 model checking is used to systematically and more effectively explore application execution paths 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 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.

AFRIKAANSE OPSOMMING : Geen Afrikaanse opsomming geskikbaar nie

Please refer to this item in SUNScholar by using the following persistent URL: http://hdl.handle.net/10019.1/102802
This item appears in the following collections: