An operational semantics for Android activities
Résumé
We define an operational semantics for a large part of the Android platform, encompassing the Dalvik bytecode but also, and more importantly, the inter-component communication mechanism used inside Android applications. This semantics is intended to provide a formal basis for the development of static analyses that consider the complex flow of information exposed by the cooperating com- ponents of Android applications.
Mots clés
Android
Operational Semantics
Static Analysis
F31 [Logics and Mean-ings of Programs]: Specifying and Verifying and Reasoning about Programs-Mechanical Verification
F32 [Logics and Meanings of Programs]: Semantics of Programming Languages-Operational semantics
Program analysis General Terms Languages
Theory
Verification Keywords Operational Semantics
Dalvik
Static Anal-ysis
Domaines
Informatique [cs]
Fichier principal
An_operational_semantics_for_android_activities.pdf (545.91 Ko)
Télécharger le fichier
Loading...