COVA 
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
covacontains the source code of COVA. - The directory
constraintBenchcontains 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.
API Documentation
There is a generated JavaDoc available.
How to Build COVA?
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:
1. Bind Z3 Library
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.
- Windows
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/binto the system variablePATHof 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
- Linux
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
- OSX
You need to add Z3 to DYLD_LIBRARY_PATH (untested)
2.1 Build The Tool With Maven
- Install required local dependencies into your local maven repository with the script
install_local_libs.*in$REPO_LOCATION/cova/localLibs(Windows usinginstall_local_libs.bator Linux usinginstall_local_libs.sh). - Return to project root to run
mvn installto build the tool and run all tests. - If you want to skip tests just run
mvn -DskipTests install
2.2 Build The Tool with Eclipse
- Install required local dependencies into your local maven repository with the script
install_local_libs.*in$REPO_LOCATION/cova/localLibs(Windows usinginstall_local_libs.bator Linux usinginstall_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
3. Running The Command-Line Tool
- 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
-androidto get all options for analyzing an Android application or with the option-javafor 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
Code Style
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