COVA is a static analysis tool to compute path constraints based on user-defined APIs. COVA was created for our paper (ASE 2019) A Qualitative Analysis of Android Taint-Analysis Results.

• The Android apps we evaluated in the paper can be found on kaggle.com (click to download)
• The directory cova contains the source code of COVA.
• The directory constraintBench contains the micro-benchmark used for COVA.
• The lists of constraint-APIs can be found in directory cova/config/: click to see UICallback-related APIs, Configuration-related APIs and IO-related APIs
• The tests for running constraintBench for COVA can be found in directory cova/src/test/java/constraintBenchTestSuite/
• For more detailed description of COVA's underlying analysis, a long version of the paper can be found here (click to download)
• The COVA IDE support is included in the develop branch.

There is a generated JavaDoc available.

COVA is implemented as a maven project. However, since some dependencies COVA uses do not have public maven repositories, to build COVA you need to follow the steps below:

COVA uses Z3 for STM-Solving and you need at first to bind Z3 for running the tool or use a docker image (tested on Linux). You can find Z3-4.5.0 in the local directory $REPO_LOCATION/cova/localLibs/ or downloand it from the GitHub repostiory of Z3.

Currently, the repository only includes Z3 for Windows 64bit. There are two choices for you to bind z3:

• Userwide via OS: Add $REPO_LOCATION/cova/localLibs/z3-4.5.0-x64-win/bin to the system variable PATH of your operating system (How do I set or change the PATH system variable?). You may need to restart your OS.

• Projectwide in Eclipse: After importing COVA as maven project, you can specify the environment variable:

Eclipse > Run > Run Configurations > Environment > New
Name: PATH
Value: $REPO_LOCATION/cova/localLibs/z3-4.5.0-x64-win/bin

Currently, the repository only includes Z3 for Ubuntu and Debian-8.5 64bit.

• via OS:

Ubuntu based distributions:

Execute the following command in yout command line: (you can set LD_LIBRARY_PATH otherwise only in an interactive shell since Ubuntu 9.04) REPO_LOCATION=$("pwd") && echo "$REPO_LOCATION/cova/localLibs/z3-4.5.0-x64-ubuntu/bin" | sudo tee /etc/ld.so.conf.d/cova.conf && sudo ldconfig

Other:

Add the LD_LIBRARY_PATH Variable to ~/.profile( or ~/.xprofile): cd into Repository: REPO_LOCATION=$("pwd") && echo "export LD_LIBRARY_PATH=\"\$LD_LIBRARY_PATH:$REPO_LOCATION/cova/localLibs/z3-4.5.0-x64-ubuntu/bin\"" >> ~/.profile; Load the edited file to your current environment (e.g. source ~/.profile or restart your user session).

• Projectwide in Eclipse for Ubuntu64:
  After importing COVA as maven project, you can specify the environment variable (change $REPO_LOCATION according to the location of the repository):

Eclipse > Run > Run Configurations > Environment > New
Name: LD_LIBRARY_PATH
Value: $REPO_LOCATION/cova/localLibs/z3-4.5.0-x64-ubuntu/bin

• Projectwide in IntelliJ Set [java.library.path] in the VM options input field in the Run/Debug Configurations dialog. $REPO_LOCATION/cova/localLibs/z3-4.5.0-x64-ubuntu/bin

You need to add Z3 to DYLD_LIBRARY_PATH (untested)

• Install required local dependencies into your local maven repository with the script install_local_libs.* in $REPO_LOCATION/cova/localLibs (Windows using install_local_libs.bat or Linux using install_local_libs.sh).
• Return to project root to run mvn install to build the tool and run all tests.
• If you want to skip tests just run mvn -DskipTests install

• Install required local dependencies into your local maven repository with the script install_local_libs.* in $REPO_LOCATION/cova/localLibs (Windows using install_local_libs.bat or Linux using install_local_libs.sh).
• Simply import the project as maven project. Maven should take care of all reqired dependences.

Eclipse> File> Import > Maven > Existing Maven Projects > Enter the path to your local repository > Finish

• Make sure you have JAVA 8 installed and bound Z3.
• Run the executable jar (found in [$REPO_LOCATION/cova/targets/] with JAVA: java -jar cova.jar .
• You can run COVA with the option -android to get all options for analyzing an Android application or with the option -java for normal Java application.
• Here is an example explained step by step:

(1) Together with FlowDroid (Default):

You can use COVA combined with FLowDroid to get the constraints under which a leak reported by FlowDroid may happen.

Run cova with the following options (put after java -jar cova.jar):

-android -config <config files path> -p <android platform path> -apk <apk file>

for testing this you can find:

• config files:$REPO_LOCATION/cova/config
• android platforms (API 26-27): $REPO_LOCATION/cova/src/test/resources/androidPlatforms
• an example apk:$REPO_LOCATION/constraintBench/androidApps/apks/Callbacks1.apk

The results are in JSON files located in $WORKING_DIRECTORY/covaOutput/jsonOutput

(2) Standalone:

You can run COVA in standalone mode with the option s. In this mode a constraint map will be computed. If you have the java source code of your application, you can get the constraint map printed next to each line of code in HTML sites with the option -output_html.

Run cova with the following options:

-android -config <config files path> -p <android platform path> -apk <apk file> -s "true" -output_html <source code path>

for testing this you can find:

• config files:$REPO_LOCATION/cova/config
• android platforms (API 26-27): $REPO_LOCATION/cova/src/test/resources/androidPlatforms
• an example apk:$REPO_LOCATION/constraintBench/androidApps/apks/Callbacks1.apk
• source code of this apk: $REPO_LOCATION/constraintBench/androidApps/sourceCode/Callbacks1

The results are in HTML files located in $WORKING_DIRECTORY/covaOutput/htmlOutput

The submodule cova follows Google's code styleguide. We use fmt-maven-plugin to format the code.
Execute this before making your pull request mvn com.coveo:fmt-maven-plugin:format