Static analysis of Android programs

详细信息    查看全文

• 作者：¨¦tienne Payet ; Fausto Spoto
• 关键词：Program verification ; Static analysis ; Abstract interpretation ; Android
• 刊名：Information and Software Technology
• 出版年：2012
• 出版时间：November, 2012
• 年：2012
• 卷：54
• 期：11
• 页码：1192-1201
• 全文大小：859 K

文摘

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 event-based 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 third-party Android applications, without any user annotation of the code, yielding formally correct results in at most 7 min and on standard hardware. Hence it is ready for a first industrial use.