IMPRS Masters Student

AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

Public Audience

English

120 Minutes

Saarbrücken

Android has the biggest market share among the operating systems for mobile devices. This makes it very attractive for developers and consequently a big part of Android's functionality is not provided by the OS itself but rather by third-party applications. Unfortunately, lots of them process sensitive data which could be potentially leaked. In order to prevent this, we need a mechanism that enforces fine-grained security properties (e.g. banking transaction data is encrypted before it is sent via Internet). The standard Android permission system does not suffice to do that. Static analysis of program code seems to be an ideal candidate: it can prove that certain security properties hold at runtime without executing the application. In addition it has zero run-time overhead (e.g., as opposed to dynamic monitoring), before its usage there is no need to root the firmware or rewrite the application, and it gives formal guarantees for its results. In our framework static analysis is used to have provable answers for queries about security relevant properties of the code. In particular, we generate Horn clauses that soundly capture the semantics of third-party applications. Then the state of the art theorem prover Microsoft Z3 is used for resolution. In the talk I will present ongoing work on the aforementioned approach, discussing its expressiveness and efficiency.

Aaron Alsancak

0681932511800

--email hidden

passcode not visible

logged in users only