IC3 Project Publications
Damien Octeau, Daniel Luchaup, Matthew Dering, Somesh Jha, and Patrick
Composite Constant Propagation: Application to Android
Inter-Component Communication Analysis.
In Proceedings of the 37th International Conference on Software
Engineering (ICSE), May 2015.
[ bib |
Many program analyses require statically inferring the possible
values of composite types. However, current approaches either do not account
for correlations between object fields or do so in an ad hoc manner. In this
paper, we introduce the problem of composite constant propagation. We develop
the first generic solver that infers all possible values of complex objects in
an interprocedural, flow and context-sensitive manner, taking field
correlations into account. Composite constant propagation problems are
specified using COAL, a declarative language. We apply our COAL solver to the
problem of inferring Android Inter-Component Communication (ICC) values, which
is required to understand how the components of Android applications interact.
Using COAL, we model ICC objects in Android more thoroughly than the
state-of-the-art. We compute ICC values for 460 applications from the Play
store. The ICC values we infer are substantially more precise than previous
work. The analysis is efficient, taking slightly over two minutes per
application on average. While this work can be used as the basis for many
whole-program analyses of Android applications, the COAL solver can also be
used to infer the values of composite objects in many other contexts.