#!/usr/bin/env python

# Given binary runs loop and in every iteration it expects consecutive numbers from 0 up to 10^19.
# check_flag(number) is executed for each passed number to validate if this number is an actual flag.
# Due to very big numbers, bruteforce is not the proper way.
# check_flag() function was quite complicated and I did not want to reverse it.
# Finally, I decided to solve this using angr:

import angr, claripy

p = angr.Project('i_can_count', auto_load_libs=False)

g = dict()
g['flag_buf'] = p.loader.find_symbol('flag_buf').rebased_addr
g['entry'] = p.loader.find_symbol('check_flag').rebased_addr
g['find'] = 0x0F9A + p.loader.main_object.min_addr
g['avoid'] = 0x0FB6 + p.loader.main_object.min_addr

state = p.factory.blank_state(addr=g['entry'])

bvs_flag = claripy.BVS('sim_flag', 8*19)
for c in bvs_flag.chop(8):
	state.solver.add(state.solver.And(c <= '9', c >= '0'))

state.memory.store(g['flag_buf'], bvs_flag)

sim = p.factory.simulation_manager(state)
print('[*] running simulation')
sim.use_technique(angr.exploration_techniques.Explorer(find=g['find'], avoid=g['avoid']))
print(sim.run())

flag_int = sim.found[0].solver.eval(bvs_flag)
print('[*] flag: PCTF{{{}}}'.format(bytes.fromhex(hex(flag_int)[2:]).decode('utf-8')))
