Android is a main actor in the operating system market for mobile and em- bedded devices such as mobile phones, tablets and televisions. It is an operating system for such devices, whose upper layers are written in a programming language, also called Android.
As a language, Android is Java with an extended library for mobile and interactive applications, and hence is based on an event-driven architecture. Any Java compiler can compile Android applications, but the resulting Java bytecode must be translated into a final, very optimized, Dalvik bytecode to be run on the device.
Static analysis of Android applications is important because quality and reliability are keys to success on the Android market. Buggy applications get a negative feedback and are immediately discarded by their potential users. Hence Android programmers want to ensure that their programs are bug-free, for instance that they do not throw any unexpected exception and do not hang the device. But Android applications are also increasingly deployed in critical contexts, even in military scenarios, where security and reliability are of the utmost importance.
For such reasons, an industrial actor such as Klocwork has already extended its static analysis tools from Java to Android, obtaining the only static analysis for Android that we are aware of. It is relatively limited in power, as far as we can infer from their web page. We could not get a free evaluation license.
A tool such as Klocwork is based on syntactical checks. This means that bugs are identified by looking for typical syntactical patterns of code that often contain a bug. The use of syntactical checks leads to very fast and practical analyses. However, it fails to recognize bugs when the buggy code does not follow the predefined patterns known by the analyzer.
The situation is the opposite for semantical tools such as Julia, where bugs are found where the artificial intelligence of the tool, based on formal methods, has not been able to prove that a program fragment does not contain a bug.
This second scenario is much more complex and computationally expensive, but provides a guarantee of soundness for the results: if no potential bug (of some class) is found, then there is no bug of that class in the code. In other terms, syntactical tools are fast but unsound. Both approaches signal false alarms, that is, potential bugs that are actually not a real bug. Precision (i.e., the amount of real bugs w.r.t. the number of warnings) is the key issue here, since the number of false alarms should not overwhelm the user of the tool.
This is acknowledged by most developers of static analysis tools. For instance, we can quote the web page of Coverity: “By providing the industry’s most accurate analysis solution and the lowest false positive rate, you can focus on the real and relevant defects instead of wasting development cycles ”.
Hence, most of the effort of the developer of a static analyzer is towards the reduction of the number of false positives. This is much more difficult for sound analyzers, since they cannot just throw away warnings and nevertheless stay sound. In any case, the presence of a company such as Klocwork on this market shows that industry recognizes the importance of the static analysis of Android code.
As described in this paper our goal is to extend the Julia static analyzer, based on abstract interpretation, to perform formally correct analyses of Android programs. This paper is an in-depth description of such an extension, of the difficulties that we faced and of the results that we obtained.
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.
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.
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 minutes and on standard hardware. Hence it is ready for a first industrial use.
To read this external content in full, download the complete paper from the author archives online at Reunion University.