Static analysis of Android programs

Abstract : Context: Android is a programming language based on Java and an operating system for embedded and mobile devices, whose upper layers are written in the Android language itself. As a language, it features an extended eventbased library and dynamic inflation of graphical views from declarative XML layout files. A static analyzer for Android programs must consider such features, for correctness and precision. Objective: Our goal is to extend the Julia static analyzer, based on abstract interpretation, to perform formally correct analyses of Android programs. This article is an in-depth description of such an extension, of the difficulties that we faced and of the results that we obtained. Method: We have extended the class analysis of the Julia analyzer, which lies at the heart of many other analyses, by considering some Android key specific features such as the potential existence of many entry points to a program and the inflation of graphical views from XML through reflection. We also have significantly improved the precision of the nullness analysis on Android programs. Results: We have analyzed with Julia most of the Android sample applications by Google and a few larger open-source programs. We have applied tens of static analyses, including classcast, dead code, nullness and termination analysis. Julia has found, automatically, bugs, flaws and inefficiencies both in the Google samples and in the open-source applications. Conclusion: Julia is the first sound static analyzer for Android programs, based on a formal basis such as abstract interpretation. Our results show that it can analyze real thirdparty Android applications, without any user annotation of the code, yielding formally correct results in at most 7 minutes and on standard hardware. Hence it is ready for a first industrial use
Type de document :
Article dans une revue
Information & Software Technology, 2012, 54 (11), pp.1192-1201
Liste complète des métadonnées

http://hal.univ-reunion.fr/hal-01186147
Contributeur : Nicolas Alarcon <>
Soumis le : vendredi 9 novembre 2018 - 07:42:46
Dernière modification le : vendredi 23 novembre 2018 - 07:27:18

Identifiants

  • HAL Id : hal-01186147, version 1

Collections

Citation

Etienne Payet, Fausto Spoto. Static analysis of Android programs. Information & Software Technology, 2012, 54 (11), pp.1192-1201. 〈hal-01186147〉

Partager

Métriques

Consultations de la notice

82

Téléchargements de fichiers

5