FLAIR is a novel approach for efficiently and incrementally updating inter-component analysis results to reflect changes to the automatically extracted architectural specifications for Android. FLAIR's update algorithm is based on reducing the space of values to be explored by the SAT-solver underlying the analysis engine. Leveraging the fact that the changes are likely to impact only a small fraction of the prior analysis results, FLAIR recomputes the analysis only where required, thereby greatly improving performance and scalability of the overall analysis. 

Approach Overview

The following diagram shows a schematic view of three different approaches for Android ICC analysis: (a) a pure program analysis approach that performs the analysis on the entire system as a combined program; (b) a hybrid, yet non-incremental approach that combines program analysis with lightweight formal analysis; and (c) FLAIR's incremental analysis approach that combines program analysis with lightweight formal analysis, where the formal analyzer recomputes the ICC analysis results in response to incremental system changes only where required.

Tool

FLAIR is implemented as an extension to the Alloy relational logic analyzer and the COVERT inter-component analysis framework. We extend the latest version of the Alloy Analyzer to realize the incremental analysis algorithms, and incorporate it into the COVERT framework as a substitute for its backend, non-incremental formal analysis engine. FLAIR's formal analyzer is publicly available.

To execute, type java –Xmx8096m –jar Flair.jar 

–f –originfile // Original App Specifications

–u –updatedfile // Updated App Specifications

-p [add or remove operations] 

–o –output // Output file

s –symmetry // A symmetry–breaking predicate size parameter 

For example, java –Xmx8096m –jar EvoAlloyICC.jar –f "ICC1.als" –u "ICC_updated.als" -p add –o "output.txt"

Experimental Evaluation

Our experimental subjects are a set of Android apps drawn from four different app repositories: Google Play, F-Droid, Bazaar and MalGenome. To perform the compositional analysis experiments, we need to simulate configurations of applications installed on a device. To that end, we partition the set of apps under study into 7 app bundles, each containing 50 apps randomly selected from the repositories. We chose this number of apps since it is higher than the average number of apps in a US smartphone, which is 41. These app bundles simulate collections of apps installed on end-user devices, and we use them to perform 7 independent experiments.

The figure above shows the analysis time taken from Covert, DIALDroid, Didfail, Flair, and SEALANT on the Y-Axis vs. the increasing size of the analyzed bundles on the X-Axis as the number of apps increases. Analysis time taken by FLAIR tends to exhibit significantly lower growth rate than the corresponding time taken by other techniques without incremental analysis.

The tool can be downloaded here.

Experimental results can be downloaded from here.