Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -52,3 +52,11 @@ docs/_build/

# PyBuilder
target/

.debian.stamp
z3
capstone
reil
smt
pyroot
concolica_pyroot
107 changes: 107 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,107 @@
#
# Makefile to build prerequisites for concolica for a user without requiring superuser privileges.
#
# sudo is still needed to install packages - this skip can be stepped using SKIP_APT=1
#

APT ?= apt-get --no-install-recommends --no-upgrade
SUDO ?= sudo
PYROOT := $(shell pwd)/pyroot

# Note: this will probably fail if your `pwd` has spaces in it.

# Generate a sourceable script

all: prereq virtualenv
@sed -e 's!@PYROOT@!$(PYROOT)!g' -e 's!@PWD@!'`pwd`'!g' < concolica_pyroot.in > concolica_pyroot
@echo "Now run the following to use concolica (or put it into your profile or bashrc):"
@echo " source concolica_pyroot"

prereq: | .debian.stamp reil smt capstone termcolor z3

virtualenv: | $(PYROOT)

$(PYROOT):
@test -d $(PYROOT) || virtualenv $(PYROOT)

#
# TODO:
#
# 1. detect if not a Debian/ubuntu system and skip this bit, use other methods to detect prerequisites
# and print a warning accordingly
# 2. If debian, allow user to override this step if they have satisified these dependencies in other ways
# 3. The apt-get command will fail if you have a complex dependency setup (like I do), so again we need a way to avoid this step
#
# `make SKIP_APT=1` will do this for all the above cases
#
.debian.stamp:
ifeq ($(SKIP_APT),)
$(SUDO) $(APT) install asciidoc build-essential git python-pip python-dev python-virtualenv
endif
@touch .debian.stamp

termcolor: | $(PYROOT)
@{ . $(PYROOT)/bin/activate ; pip -q install termcolor ; }

reil: | $(PYROOT)
test -d reil || git clone https://github.com/c01db33f/reil.git $(PYROOT)/lib/python2.6/site-packages/reil

smt:
test -d smt || git clone https://github.com/c01db33f/smt.git

capstone: | $(PYROOT)
test -d capstone || git clone https://github.com/aquynh/capstone.git
export DESTDIR=$(PYROOT) && cd capstone && MAKEFLAGS=-j ./make.sh install
{ . $(PYROOT)/bin/activate ; cd capstone/bindings/python && python setup.py install ; }

#
# NOTE
#
# z3 is hosted on codeplex which seems to have a completely different git+TLS setup from the rest of the planet
# So in most cases except for very bleeding edge installations of git, git clone fails with the following message:
#
# error: RPC failed; result=56, HTTP code = 200
#
# So we have to workaround by using git fetch instead
#
# See: http://z3.codeplex.com/wikipage?title=Git%20HTTPS%20cloning%20errors
# See: https://bugs.launchpad.net/ubuntu/+source/gnutls26/+bug/1111882
#
# The alternative solution is to rebuild git from source against libcurl4-openssl-dev but not everyone wants to do that
#
z3: | $(PYROOT)
test -d z3 || { mkdir z3 && cd z3 && git init && { git remote add -f origin https://git01.codeplex.com/z3 ; git fetch && git checkout -B master origin/master ; } ; }
cd z3 && autoconf && ./configure --prefix=$(PYROOT)
{ . "$(PYROOT)/bin/activate" ; cd z3 && python scripts/mk_make.py ; }
cd z3/build && $(MAKE) && $(MAKE) install

clean: prereq-clean virtualenv-clean

virtualenv-clean:
@-rm -rf $(PYROOT)

prereq-clean:
@-rm -rf .debian.stamp reil smt capstone z3

help:
@echo "Recommended usage:"
@echo
@echo " make -jX"
@echo
@echo "where X is the number of CPU/cores available for use by make."
@echo
@echo "Primary targets:"
@echo
@echo " all clean"
@echo
@echo "This makefile constructs a python virtual environment at $(PYROOT)"
@echo "To use the python virtual environment for concolic analysis do:"
@echo
@echo " source concolica_pyroot"
@echo
@echo "If your system is not based on Debian, skip the package prerequisites using 'make SKIP_APT=1'"
@echo "The following source prerequisites are downloaded and built once: reil smt capstone z3"
@echo "To recompile a previously built prerequisite use (for example) 'make -B capstone'"

.PHONY: help clean virtualenv virtualenv-clean prereq-clean

77 changes: 21 additions & 56 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,46 +10,11 @@ concolica has a handful of dependencies - the reil translation code requires
capstone to provide disassembly support, the smt code currently supports only
the Microsoft Z3 solver as a backend.

The following should work on Debian based systems:
The installer has been mostly automated and can be invoked simply as `make`; only package prerequisites now require sudo.

`sudo apt-get install asciidoc build-essential gettext git libcurl4-openssl-dev python-pip python-dev zlib1g-dev

git clone https://github.com/git/git.git
cd git
make configure
./configure --prefix=/usr
make all
sudo make install
cd ../

git clone https://github.com/c01db33f/reil.git
git clone https://github.com/c01db33f/smt.git

git clone https://github.com/aquynh/capstone.git
cd capstone
./make.sh
sudo ./make.sh install
cd bindings/python
sudo python ./setup.py install
cd ../../../

sudo pip install termcolor

git clone https://git01.codeplex.com/z3
cd z3
autoconf
./configure
python scripts/mk_make.py
cd build
make -j 8
sudo make install
cd ../../`

Then add the following to your .bash_aliases

`export PYTHONPATH=$PYTHONPATH:/path/to/concolica/smt/and/reil
export VDB_EXT_DIR=/path/to/conolica/vdb`
make -j

This creates a file `concolica_pyroot` which you can then source so the correct Python and library paths are set.

Usage
-----
Expand All @@ -58,28 +23,28 @@ All depends what you want to use it for... See the examples directory for some
completely undocumented example code. run_state.py is used with a process dump
made using vdb; something like

`c01db33f@ctf$ vdb
vdb> exec my_program
vdb> bp program.main
vdb> go
vdb> dump_state -a=x86_64 -f=dump.cc
vdb> quit

c01db33f@ctf$ ./run_state.py`
c01db33f@ctf$ vdb
vdb> exec my_program
vdb> bp program.main
vdb> go
vdb> dump_state -a=x86_64 -f=dump.cc
vdb> quit
c01db33f@ctf$ ./run_state.py

test_trace.py is used to validate the REIL translation code against an execution
trace made using vdb; something like

`c01db33f@ctf$ vdb
vdb> exec my_program
vdb> bp my_program.main
vdb> go
vdb> save_trace -a=x86_64 -f=output.trace
^C
vdb> quit

c01db33f@ctf$ ./test_trace.py -f=output.trace`

c01db33f@ctf$ vdb
vdb> exec my_program
vdb> bp my_program.main
vdb> go
vdb> save_trace -a=x86_64 -f=output.trace
^C
vdb> quit

c01db33f@ctf$ ./test_trace.py -f=output.trace`


For more information about the Python-hosted debugger vdb, see http://visi.kenshoto.com/viki/Vdb

1 change: 1 addition & 0 deletions concolica
5 changes: 5 additions & 0 deletions concolica_pyroot.in
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
source @PYROOT@/bin/activate
export PYTHONPATH=$PYTHONPATH:@PWD@:@PWD@/smt:@PWD@/reil
export VDB_EXT_DIR=@PWD@/vdb
# The following line may vary on some systems. TBH I am a little surprised that virtualenv doesnt add it in for 64-bit Debian
export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:@PYROOT@/usr/lib64