Zusammenfassung
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.
