diff --git a/examples/script/introduce_symbolic_bytes.py b/examples/script/introduce_symbolic_bytes.py new file mode 100644 index 0000000..a252290 --- /dev/null +++ b/examples/script/introduce_symbolic_bytes.py @@ -0,0 +1,50 @@ + +import sys +from manticore import Manticore + +''' +Replaces a variable that controls program flow with a symbolic buffer. This +in turn explores all possible states under that variable's influence. + +Usage: + + $ gcc -static -g src/state_explore.c -o state_explore # -static is optional + $ ADDRESS=0x$(objdump -S state_explore | grep -A 1 '((value & 0xff) != 0)' | + tail -n 1 | sed 's|^\s*||g' | cut -f1 -d:) + $ python ./introduce_symbolic_bytes.py state_explore $ADDRESS + +''' + +if __name__ == '__main__': + if len(sys.argv) < 3: + sys.stderr.write("Usage: %s [binary] [address]\n"%(sys.argv[0],)) + sys.exit(2) + + # Passing a parameter to state_explore binary disables reading the value + # from STDIN, and relies on us adding it manually + m = Manticore(sys.argv[1], ['anything']) + + # Uncomment to see debug output + #m.verbosity = 2 + + # Set to the address of the instruction before the first conditional. + introduce_at = int(sys.argv[2], 0) + + @m.hook(introduce_at) + def introduce_sym(state): + # RBP-0xC is the location of the value we're interested in: + # + # if ((value & 0xff) != 0) { + # 400a08: 8b 45 f4 mov -0xc(%rbp),%eax + # 400a0b: 0f b6 c0 movzbl %al,%eax + # 400a0e: 85 c0 test %eax,%eax + # + + print "introducing symbolic value to {:x}".format(state.cpu.RBP-0xc) + + val = state.new_symbolic_buffer(4) + state.cpu.write_bytes(state.cpu.RBP - 0xc, val) + + m.run() + + print 'Analysis finished. See {} for results.'.format(m.workspace) diff --git a/examples/script/state_explore.c b/examples/script/src/state_explore.c similarity index 68% rename from examples/script/state_explore.c rename to examples/script/src/state_explore.c index 2edb99d..09cf630 100644 --- a/examples/script/state_explore.c +++ b/examples/script/src/state_explore.c @@ -1,23 +1,30 @@ #include /** - * Example code for the state abandon example in the Manticore script corpus. + * Example code for the state state_control.py and introduce_symbolic_bytes.py + * examples. * - * # Compile binary - * $ gcc -m32 -static -g state_explore.c -o state_explore - * - * # Pull out the address of the branch we want to ignore - * $ ADDRESS=0x$(objdump -S state_explore | grep -A 1 'value == 0x41' | tail -n 1 | sed 's|^\s*||g' | cut -f1 -d:) - * - * # Run the analysis - * $ python state_explore.py state_explore $ADDRESS + * See scripts for more information. */ + +void +fill_from_stdin(int *value) +{ + read(0, value, sizeof *value); +} + int main(int argc, char *argv[]) { int value; - read(0, &value, sizeof value); + /** + * If we don't receive any arguments, read value from stdin. If we do + * receive an argument, treat `value` as uninitialized. + */ + if (argc < 2) { + fill_from_stdin(&value); + } if ((value & 0xff) != 0) { if (value >= 0x40) { diff --git a/examples/script/state_control.py b/examples/script/state_control.py new file mode 100644 index 0000000..292df7e --- /dev/null +++ b/examples/script/state_control.py @@ -0,0 +1,40 @@ + +import sys +from manticore import Manticore + +''' +Demonstrates the ability to guide Manticore's state exploration. In this case, +abandoning a state we're no longer interested in. + +Usage: + + $ gcc -static -g src/state_explore.c -o state_explore # -static is optional + $ ADDRESS=0x$(objdump -S state_explore | grep -A 1 'value == 0x41' | + tail -n 1 | sed 's|^\s*||g' | cut -f1 -d:) + $ python ./state_control.py state_explore $ADDRESS + +''' + +if __name__ == '__main__': + if len(sys.argv) < 3: + sys.stderr.write("Usage: %s [binary] [address]\n"%(sys.argv[0],)) + sys.exit(2) + + m = Manticore(sys.argv[1]) + + # Uncomment to see debug output + #m.verbosity = 2 + + # Set to the address of the conditional at state_explore.c:38, which will be + # abandoned. If line 36 of this script is commented out, Manticore will + # explore all reachable states. + to_abandon = int(sys.argv[2], 0) + + @m.hook(to_abandon) + def explore(state): + print "Abandoning state at PC: ", hex(state.cpu.PC) + state.abandon() + + print "Adding hook to: {:x}".format(to_abandon) + + m.run() diff --git a/examples/script/state_explore.py b/examples/script/state_explore.py deleted file mode 100644 index 41ce5de..0000000 --- a/examples/script/state_explore.py +++ /dev/null @@ -1,26 +0,0 @@ - -import sys -from manticore import Manticore - -''' -Demonstrates guiding Manticore's state exploration. -''' - -if __name__ == '__main__': - if len(sys.argv) < 3: - sys.stderr.write("Usage: %s [binary] [address]\n"%(sys.argv[0],)) - sys.exit(2) - - m = Manticore(sys.argv[1]) - - # Set to the address of the conditonal checking for the first complex branch - to_abandon = int(sys.argv[2], 0) - - @m.hook(to_abandon) - def explore(state): - print "Abandoning state at PC: ", hex(state.cpu.PC) - state.abandon() - - print "Adding hook to: {:x}".format(to_abandon) - - m.run()