PRIMO

Despite the many techniques devised to increase the precision of static analysis results, the results precision is often not high enough for large scale analysis. This is because the static inference of many properties is undecidable, and others are too computationally expensive. This is especially problematic with the rise of centralized application markets, where market providers may want to verify properties (e.g., security) in their entire corpus. In this case imprecise results are not acceptable.

We explore the use of probabilistic models in order to help sift through large numbers of results and prioritize them by decreasing order of likelihood. We apply this to the computation of links between over 10,000 Android applications with our PRIMO tool. PRIMO is able to compute links between various applications as computed by IC3 (see below). It can also compute the probability that these links are true positives.

For information on PRIMO, please visit siis.cse.psu.edu/primo.

COAL

Many program analyses require statically inferring the possible values of object variables. However, current approaches either do not account for correlations between object fields or do so in an ad hoc manner. The COAL project enables the specification and solution of these problems in a principled way. The project includes a language that is used to describe the classes of the objects whose value should be inferred. It also includes a solver, which computes the object values.

The COAL language allows easy specification of composite constant propagation problems. Our COAL solver takes as inputs a COAL specification and the code that needs to be analyzed and automatically outputs the value of the fields of the requested variables. Note that in programs where there are several possible values for a given object, the COAL solver infers all possible values, taking into account the correlations between the fields on different execution paths.

For information about COAL, please visit siis.cse.psu.edu/coal.

IC3

Many threats present in smartphones are the result of interactions between application components, not just artifacts of single components. For example, information may flow between components in an unsafe manner. A component in an application may retrieve a user's location data or contacts. It may subsequently send the sensitive private information to a component in another application. The receiving component may then leak the sensitive information to the network, to an untrusted third party.

Using COAL, we build IC3, a tool for inferring ICC with significantly better precision than Epicc. Unlike Epicc, it models all ICC primitives.

For information about IC3, please visit siis.cse.psu.edu/ic3.

Epicc

Epicc was our initial tool for inferring ICC in Android applications. It paved the way for the idea of reducing the inference of object values to an Interprocedural Distributive Environment (IDE) data flow problem.

For information regarding obtaining and using Epicc, please visit siis.cse.psu.edu/epicc.

Dare

Dare is a tool that retargets Android applications running on the Dalvik Virtual Machine to traditional Java Virtual Machine .class files. These .class files can then be processed by existing Java tools, including decompilers. Thus, Android applications can be analyzed using a vast range of techniques developed for traditional Java applications. Dare replaces ded as a retargeting tool: it is more accurate, more efficient, more powerful and can even handle cases where the input code is unverifiable.

Dare was awarded the Best Artifact Award at the 20th International Symposium on the Foundations of Software Engineering (FSE), recognizing its value as a significant and high-quality tool. For more information, you can read the paper "Retargeting Android Applications to Java Bytecode" by Octeau et al., published in the proceedings of the 20th International Symposium on the Foundations of Software Engineering (FSE). For downloads, see the Dare page.

ded

Smartphone applications are frequently incompletely vetted, poorly isolated, and installed by users without restraint. Smartphone research frequently needs to understand how these applications behave. ded is a project which aims at decompiling Android applications. The ded tool retargets Android applications in .dex format to traditional .class files. These .class files can then be processed by existing Java tools, including decompilers. Thus, Android applications can be analyzed using a vast range of techniques developed for traditional Java applications.

For information regarding obtaining and using ded, please visit siis.cse.psu.edu/ded.