majestyhao / condroid

Symbolic/concolic execution of Android apps

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

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>