Formalisation and analysis of Dalvik bytecode

Erik Ramsgaard Wognsen, Henrik Søndberg Karlsen, Mads Chr. Olesen, Rene Rydhof Hansen

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

25 Citationer (Scopus)

Abstrakt

With the large, and rapidly increasing, number of smartphones based on the Android platform, combined with the open nature of the platform that allows “apps” to be downloaded and executed on the smartphone, misbehaving and malicious (malware) apps are set to become a serious problem. To counter this problem, automated tools for analysing and verifying apps are essential. Furthermore, to ensure high-fidelity of such tools, it is essential to formally specify both semantics and analyses.

In this paper we present, to the best of our knowledge, the first formalisation of the complete Dalvik bytecode language including reflection features and the first formally specified control flow analysis for the language, including advanced control flow features such as dynamic dispatch, exceptions, and reflection. To determine which features to include in the formalisation and analysis, 1700 Android apps from the Google Play app market (formerly known as Android Market) were downloaded and examined.
OriginalsprogEngelsk
TidsskriftScience of Computer Programming
Vol/bind92
Udgave nummerPart A
Sider (fra-til)25-55
Antal sider31
ISSN0167-6423
DOI
StatusUdgivet - 15 okt. 2014

Fingeraftryk

Dyk ned i forskningsemnerne om 'Formalisation and analysis of Dalvik bytecode'. Sammen danner de et unikt fingeraftryk.

Citationsformater