Modeling the Android platform - Université de La Réunion Access content directly
Conference Papers Year : 2013

Modeling the Android platform


Android is currently the world's most popular mobile platform. One of its key features is the possibility for a user to install new applications on a device. Applications can be downloaded from anywhere in the Dalvik bytecode format and they do not have to be digitally signed before installation. As a consequence, reliability has become a major concern for users, as buggy applications can hang the device or malicious code can steal private data. Many analyses have been presented so far for finding bugs or malicious code in Android programs. A few of them rely on formal operational semantics for the Dalvik virtual machine executing the bytecode. But till now, no formal semantics for important specific features of the Android platform, such as the inter-component communication mechanism, has been proposed. In this talk, we review the semantics that have been proposed for Dalvik and we introduce a first attempt at defining an operational semantics for a part of the Android platform encompassing the "activity" component communication mechanism.
bytecode13.pdf (779.25 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-01187209 , version 1 (23-11-2018)


  • HAL Id : hal-01187209 , version 1


Etienne Payet. Modeling the Android platform. 8th International Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'13), Mar 2013, Rome, Italy. pp.en ligne. ⟨hal-01187209⟩
93 View
13 Download


Gmail Mastodon Facebook X LinkedIn More