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.
Type de document :
Communication dans un congrès
8th International Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'13), Mar 2013, Rome, Italy. pp.en ligne, 2013
Liste complète des métadonnées

http://hal.univ-reunion.fr/hal-01187209
Contributeur : Nicolas Alarcon <>
Soumis le : mercredi 26 août 2015 - 12:39:58
Dernière modification le : mercredi 7 février 2018 - 08:12:02

Identifiants

  • 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, 2013. 〈hal-01187209〉

Partager

Métriques

Consultations de la notice

38