Add manticore-examples to README and remove google challenge (#271)

* add manticore-examples to README and remove google challenge

* re-do usage section and add manticore-examples repo

README.md

@@ -16,6 +16,7 @@ Manticore is a prototyping tool for dynamic binary analysis, with support for sy
 
 Manticore supports binaries of the following formats, operating systems, and
 architectures. It has been primarily used on binaries compiled from C and C++.
+Examples of practical manticore usage are also [on github](https://github.com/trailofbits/manticore-examples).
 
 - OS/Formats: Linux ELF, Windows Minidump
 - Architectures: x86, x86_64, ARMv7 (partial)
@@ -133,5 +134,17 @@ def hook(state):
 m.run()
 ```
 
-See the [wiki](https://github.com/trailofbits/manticore/wiki), [examples](examples) directory, and [API reference](http://manticore.readthedocs.io/en/latest/) for further documentation.
+Further documentation is available in several places:
+
+  * The [wiki](https://github.com/trailofbits/manticore/wiki) contains some
+    basic information about getting started with manticore and contributing
+
+  * The [examples](examples) directory has some very minimal examples that
+    showcase API features
+
+  * The [manticore-examples](https://github.com/trailofbits/manticore-examples)
+    repository has some more involved examples, for instance solving real CTF problems
+
+  * The [API reference](http://manticore.readthedocs.io/en/latest/) has more
+    thorough and in-depth documentation on our API
 

examples/script/google2016_unbreakable/win.py

@@ -1,61 +0,0 @@
-from manticore import Manticore
-
-"""
-Leverages Manticore to solve the Google 2016 challenge: 
-unbreakable-enterprise-product-activation
-
-Author: @ctfhacker
-Binary: https://github.com/ctfs/write-ups-2016/blob/master/google-ctf-2016/reverse/unbreakable-enterprise-product-activation-150/unbreakable-enterprise-product-activation.bz2
-"""
-
-m = Manticore('unbreakable')
-
-"""
-These values can be found at 0x4005b8
-"""
-input_addr = 0x6042c0
-num_bytes = 0x43
-
-# Entry point
-@m.hook(0x400729)
-def hook(state):
-    """ CAUTION: HACK """
-    """ From entry point, jump directly to code performing check """
-
-    # Create a symbolic buffer for our input
-    buffer = state.new_symbolic_buffer(0x43)
-
-    # We are given in the challenge that the flag begins with CTF{
-    # So we can apply constraints to ensure that is true
-    state.constrain(buffer[0] == ord('C'))
-    state.constrain(buffer[1] == ord('T'))
-    state.constrain(buffer[2] == ord('F'))
-    state.constrain(buffer[3] == ord('{'))
-
-    # Store our symbolic input in the global buffer read by the check
-    state.cpu.write_bytes(input_addr, buffer)
-
-    # By default, `hook` doesn't patch the instruction, so we hop over
-    # the hooked strncpy and execute the next instruction
-    state.cpu.EIP = 0x4005bd
-
-# Failure case
-@m.hook(0x400850)
-def hook(state):
-    """ Stop executing paths that reach the `failure` function"""
-    print("Invalid path.. abandoning")
-    state.abandon()
-
-# Success case
-@m.hook(0x400724)
-def hook(state):
-    print("Hit the final state.. solving")
-
-    buffer = state.cpu.read_bytes(input_addr, num_bytes)
-    res = ''.join(chr(state.solve_one(x)) for x in buffer)
-    print(res) # CTF{0The1Quick2Brown3Fox4Jumped5Over6The7Lazy8Fox9}
-
-    # We found the flag, no need to continue execution
-    m.terminate()
-
-m.run(procs=10)