Logic-Oriented Opaque Predicate Detection in Obfuscated Binary Code
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
batteries
doc
libasmir
libtracewrap
m4 init commit Jul 21, 2015
ocaml-proj.example
ocaml
ocamlgraph
opq-testcases
ounit
pcre-ocaml
pintraces
piqi-files
solvers
tests-proj.example
tests
utils-proj.example
utils
vagrant
zarith
AUTHORS
ChangeLog
INSTALL
LICENSE.GPL
LICENSE.MIT
Makefile.am
NEWS
README
STYLE.C
STYLE.ocaml
TODO
Vagrantfile
autogen.sh
configure.ac
gpl-2.0.txt

README

LOOP is a logic oriented opaque predicate checker. It is able 
to detect the following opaque predicates in binary code:

1. Invariant opaque predicate
2. Contextual opaque predicate
3. Dynamic opaque predicate

LOOP is developed based on BAP.

BAP: The Binary Analysis Platform. For more information see the
project webpage at http://bap.ece.cmu.edu

BAP is released under MIT license and the GPL license; see the
appropriate LICENSE.{MIT,GPL}.

How to use:

1. Use Pin to generate a execution trace. It also needs a lib called gentrace. The command is like:
   LOOPDIR/pin/pin -t LOOPDIR/pintraces/obj-ia32/gentrace.so -taint_args -- yourprogram yourargs

2. Convert trace into concrete trace:
   LOOPDIR/utils/iltrans -trace tracename -trace-concrete -pp-ast tracename.con.il

3. Preprocess the trace:
   LOOPDIR/utils/pre_process.pl tracename.con.il

4. Symbolic execute the trace:
   LOOPDIR/utils/iltrans -il tracename.con.il -il-formula tracename.stp

5. Solve the formula with STP. You will need a STP solver installed.
   stp tracename.stp