Unit:
Department of Informatics and TelecommunicationsΠληροφορική
Supervisors info:
Γιάννης Σμαραγδάκης, Καθηγητής, Τμήμα Πληροφορικής και Τηλεπικοινωνιών, ΕΚΠΑ
Original Title:
Declarative type inference and SSA transformation of Android applications
Translated title:
Declarative type inference and SSA transformation of Android applications
Summary:
Android is everywhere: from mobile devices and TVs to more recently automobile infotainment systems. This widespread use of the Android OS makes application analysis ever so important, in order to optimize the application performance and system resource usage.
Static Single Assignment (SSA) is a convenient normalized program representation that
can simplify several static analyses. However, the underlying DEX bytecode of an Anrdroid
application does not have the SSA property, and further processing of the program must
be done in order to obtain it. Moreover, DEX bytecode provides almost no explicit type information for the program’s variables, limiting the accuracy of the analyses.
In this thesis, we develop a Datalog program that transforms an Android application into
SSA form, effectively extending the functionality of the DEX fact generation front end of
the Doop framework. Additionally, we present a type inference algorithm, to resolve the types of the variables that the SSA transformation produced.
Main subject category:
Technology - Computer science
Keywords:
static program analysis, program transformation, dex bytecode, type inference
