Mainticore Test 2

solve.py

#!/usr/bin/python

from manticore import Manticore
from manticore.models import strlen

m = Manticore('main-sec-pw')

buffer_addr=0
num_bytes=127

@m.hook(0x4141448e)
def strlen_model(state):
    state.invoke_model(strlen)

@m.hook(0x7ffffffcd264)
def hook(state):
    # Jump to the check
    state.cpu.EIP = 0x41414484

@m.hook(0x4141448b)
def hook(state):
    print('Found initial point')
    solution = state.new_symbolic_buffer(num_bytes)
    state.constrain(solution[0] == ord('C'))
    state.constrain(solution[1] == ord('T'))
    state.constrain(solution[2] == ord('F'))
    state.constrain(solution[3] == ord('{'))
    buffer_addr = state.cpu.read_int(state.cpu.RAX)
    m.context[1] = buffer_addr
    print("Buffer Addr: %08x" %(buffer_addr))
    state.cpu.write_bytes(buffer_addr, solution)

@m.hook(0x41414553)
def hook(state):
    print("Fail...")
    state.abandon()

@m.hook(0x41414540)
def hook(state):
    print("WIN!")
    buffer_addr = m.context[1]
    res = ''.join(map(chr, state.solve_buffer(buffer_addr, num_bytes)))
    print("flag is : %s"%(res))
    m.terminate()

m.verbosity =1
m.run(procs=10)