diff --git a/.gitignore b/.gitignore index db4561e..65de70a 100644 --- a/.gitignore +++ b/.gitignore @@ -52,3 +52,11 @@ docs/_build/ # PyBuilder target/ + +.debian.stamp +z3 +capstone +reil +smt +pyroot +concolica_pyroot diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..21c0cce --- /dev/null +++ b/Makefile @@ -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 + diff --git a/README.md b/README.md index bcd6596..ac3a55b 100644 --- a/README.md +++ b/README.md @@ -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 ----- @@ -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 diff --git a/concolica b/concolica new file mode 120000 index 0000000..945c9b4 --- /dev/null +++ b/concolica @@ -0,0 +1 @@ +. \ No newline at end of file diff --git a/concolica_pyroot.in b/concolica_pyroot.in new file mode 100644 index 0000000..734f1b0 --- /dev/null +++ b/concolica_pyroot.in @@ -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