de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Thesis

Static Analysis of Android Applications

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons188657

Grishchenko,  Ilya
International Max Planck Research School, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

Grishchenko, I. (2014). Static Analysis of Android Applications. Master Thesis, Universität des Saarlandes, Saarbrücken.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0026-C962-6
Abstract
Mobile and portable devices are machines that users carry with them everywhere, they can be seen as constant personal assistants of modern human life. Today the Android operating system for mobile devices is the most popular one and the number of users still grows: as of September 2013, 1 billion devices have been activated [Goob]. This makes the Android market attractive for developers willing to provide new functionality. As a consequence, 48 billion applications ("apps") have been installed from the Google Play store [BBC]. Apps often require user data in order to perform the intended activity. At the same time parts of this data can be treated as sensitive private information, for instance, authentication credentials for accessing the bank account. The most significant built-in security measure in Android, the permission system, provides only little control on how the app is using the supplied data. In order to mitigate the threat mentioned above, the hidden unintended app activity, the recent research goes in three main directions: inline-reference monitoring modifies the app to make it safe according to user defined restrictions, dynamic analysis monitors the app execution in order to prevent undesired activity, and static analysis verifies the app properties from the app code prior to execution. As we want to have provable security guarantees before we execute the app, we focus on static analysis. This thesis presents a novel static analysis technique based on Horn clause resolution. In particular, we propose the small-step concrete semantics for Android apps, we develop a new form of abstraction which is supported by general theorem provers. Additionally, we have proved the soundness of our analysis technique. We have developed a tool that takes the bytecode of the Android app and makes it accessible to the theorem prover. This enables the automated verification of a variety of security properties, for instance, whether a certain functionality is preceded by a particular one, for instance, whether the output of a bank transaction is secured before sending it to the bank, or on which values it operates, for instance, whether the IP-address of the bank is the only possible transaction destination. A case study as well as a performance evaluation of our tool conclude this thesis.