Modeling the Android platform

Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

http://hal.univ-reunion.fr/hal-01187209
Contributor : Nicolas Alarcon <>
Submitted on : Friday, November 23, 2018 - 6:50:03 AM
Last modification on : Thursday, March 28, 2019 - 11:24:10 AM

Identifiers

  • HAL Id : hal-01187209, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

81

Files downloads

2