#!/usr/bin/env python2

# Author: David Manouchehri <manouchehri@protonmail.com>
# Google 2016 CTF
# Challenge: Unbreakable Enterprise Product Activation
# Team: hack.carleton (http://hack.carleton.team/)
# Runtime: ~4.5 seconds (single threaded E5-2666 v3 @ 2.90GHz on AWS/EC2)

from pwn import *
import angr
import claripy

def main():
    #fail_addr = [0x001013f1, 0x001013e1, 0x001013cd, 0x001013a0]
    proj = angr.Project('/home/kali/htb/challenges/reversing/Spooky License/rev_spookylicence/spookylicence',main_opts={"base_addr": 0}) # Disabling the automatic library loading saves a few milliseconds.

    input_size = 0x20; # Max length from strncpy, see 0x4005ae.

    argv1 = claripy.BVS("argv1", input_size * 8)

    initial_state = proj.factory.entry_state(args=["/home/kali/htb/challenges/reversing/Spooky License/rev_spookylicence/spookylicence", argv1], remove_options={angr.options.LAZY_SOLVES})
    initial_state.libc.buf_symbolic_bytes=input_size + 1 # Thanks to Christopher Salls (@salls) for pointing this out. By default there's only 60 symbolic bytes, which is too small.

    # For some reason if you constrain too few bytes, the solution isn't found. To be safe, I'm constraining them all.
    for byte in argv1.chop(8):
        initial_state.add_constraints(byte != ord('\x00')) # null
        initial_state.add_constraints(byte >= ord(' ')) # '\x20'
        initial_state.add_constraints(byte <= ord('~')) # '\x7e'
        # Source: https://www.juniper.net/documentation/en_US/idp5.1/topics/reference/general/intrusion-detection-prevention-custom-attack-object-extended-ascii.html
        # Thanks to Tom Ravenscroft (@tomravenscroft) for showing me how to restrict to printable characters.

    # # We're told that every flag is formatted as "CTF{...}", so we might as well use that information to save processing time.
    initial_state.add_constraints(argv1.chop(8)[9] == 'p')
    # initial_state.add_constraints(argv1.chop(8)[1] == 'y')
    # initial_state.add_constraints(argv1.chop(8)[2] == 'b')
    # initial_state.add_constraints(argv1.chop(8)[3] == 'e')
    # initial_state.add_constraints(argv1.chop(8)[2] == 'r')
    # initial_state.add_constraints(argv1.chop(8)[3] == '_')
    # angr will still find the solution without setting these, but it'll take a few seconds more.

    sm = proj.factory.simulation_manager(initial_state)

    sm.explore(find=0x187d, avoid=0x11b8)

    found = sm.found[0] # In our case, there's only one printable solution.
    print(found.posix.dumps(0), found.posix.dumps(1))
    solution = found.solver.eval(argv1)
    print(solution)
    #solution = solution[:solution.find(b"}")+1] # Trim off the null bytes at the end of the flag (if any).
    #print(solution)
    return solution

# def test():
#     assert main() == b'CTF{0The1Quick2Brown3Fox4Jumped5Over6The7Lazy8Fox9}'

if __name__ == '__main__':
    proc = process("/home/kali/htb/challenges/reversing/Spooky License/rev_spookylicence/spookylicence")
    main()