Symbolic/concolic execution of Android apps
Java Other
Switch branches/tags
Nothing to show
Clone or download
Latest commit b93ed7c Mar 8, 2016
Permalink
Failed to load latest commit information.
.settings/gradle gitignore, eclipse launch configs Jan 21, 2016
acteve-util-jimple Instrumentation works. Loading all acteve.symbolic.* classes, includi… Aug 2, 2014
eclipse Update to apktool 2.0.3, fix for possible NPE, removed absolute path Mar 6, 2016
jars Refactoring: Moved to single src folder Mar 26, 2015
libs Update to apktool 2.0.3, fix for possible NPE, removed absolute path Mar 6, 2016
mymodels/src/models On the fly creation of modelled classes Nov 6, 2014
out Refactoring: Moved to single src folder Mar 26, 2015
src Update to apktool 2.0.3, fix for possible NPE, removed absolute path Mar 6, 2016
.classpath mvn/gradle-like project layout Jan 21, 2016
.gitignore gitignore, eclipse launch configs Jan 21, 2016
.project Cleanup, support for generic (i.e. String or primitive) modeled fields Nov 6, 2014
.travis.yml Travis-CI yml Nov 18, 2014
AndroidCallbacks.txt Entry point injection, workaround for G.reset()-bug in infoflow, clea… Aug 4, 2014
LICENSE_BSD licenses Aug 16, 2014
LICENSE_LGPL licenses Aug 16, 2014
README.md README Mar 8, 2016
Z3-str_20140720.zip Added Z3-str binary (unpack to /opt/) and a model for TelephonyManager Nov 6, 2014
a3t-app.xml initial commit Aug 2, 2014
a3t-sdk.xml initial commit Aug 2, 2014
a3t.sdk.properties initial commit Aug 2, 2014
build.xml mvn/gradle-like project layout Jan 21, 2016
config.properties.sample Configurable usage of monkey script, moved Acteve path exploration to Feb 4, 2015
fieldsToModel.txt Injection of field values Nov 6, 2014
inputs.dat Dynamic injection of Z3 solution values. Solutions are pushed to /sdc… Aug 2, 2014
models.dat Compute sub-CG between entrypoints and goals Aug 12, 2014
monkey_script.txt Run config for executor Aug 4, 2014
postsdkbuild Added required a3t libraries, adjusted configs Aug 2, 2014

README.md

ConDroid

This project is a fork and extension of the Acteve project on concolic execution for Android (https://code.google.com/p/acteve/) [1]

ConDroid performs concolic execution of Android apps - a combination of pure symbolic and concrete execution of a program which has first been described in [2] for C programs. The goal of ConDroid is to drive execution of Android app to specific code locations without requiring any manual interaction with the app. This allows to observe "interesting" behavior in a dynamic analysis, such as network traffic or dynamic code loading.

Some details on the extensions have been published in [3].

[1] Saswat Anand, Mayur Naik, Hongseok Yang, Mary Jean Harrold. Automated Concolic Testing of Smartphone Apps. In ACM International Symposium on Foundations of Software Engineering (FSE), 2012.

[2] Koushik Sen, Darko Marinov, Gul Agha. CUTE: A concolic unit testing engine for C. In Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, 2005

[3] Julian Schütte, Rafael Fedler, Dennis Titze. ConDroid: Targeted Dynamic Analysis of Android Applications. In IEEE Conference on Advanced Information Networking and Applications (AINA), 2015

Bitdeli Badge Coverity Scan Build Status

Getting Started

Prerequisites

  • Android SDK
  • Z3 solver, including the string extensions from this project

Clone

git clone https://github.com/JulianSchuette/ConDroid.git

Install Z3-str

Unzip Z3 solver with added supported for String operations (equals, concat, etc.)

unzip Z3-str_20140720.zip /opt/
mv /opt/Z3-str_20140720 /opt/z3

Set up configuration

mv config.properties.sample config.properties

Set up eclipse

  • Import project into eclipse

Launch

  • Launch an android emulator
  • Launch run configuration from eclipse The app under test is given as argument to the program

java -jar condroid.jar <apk>