Verifying Android applications using Java PathFinder
Date
2017-11-20
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Stellenbosch : Stellenbosch University
Abstract
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
AFRIKAANSE OPSOMMING : Geen Afrikaanse opsomming geskikbaar nie
Description
Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Division Computer Science.
Thesis (PhD)--Stellenbosch University, 2017
Thesis (PhD)--Stellenbosch University, 2017
Keywords
Android software -- Model checking, Android applications, Java Pathfinder (JPF), Cell phones -- Applications, UCTD