[SOLVED] angr and claripy: defining non-contiguos constraints

angr and claripy: defining non-contiguos constraints

I'm playing with angr and I'm trying to constraint my input to printable chars. I did it in the "well-known" way like this:

import angr
import claripy

base_addr = 0x800000 
proj = angr.Project("binary", main_opts={'base_addr': base_addr})

flag_chars = [claripy.BVS('%d' % i, 8) for i in range(16)]
flag = claripy.Concat( *flag_chars + [claripy.BVV(b'\n')]) 

state = proj.factory.full_init_state(
        args=['binary'],
        add_options=angr.options.unicorn,
        stdin=flag,
)

for k in flag_chars:
     init_state.solver.add(k <= 0x7f)
     init_state.solver.add(k >= 0x20)

simgr = proj.factory.simulation_manager(state)
find_addr  = 0x807bf5 
avoid_addr = 0x807c55 
simgr.explore(find=find_addr, avoid=avoid_addr)

if (len(simgr.found) > 0):
    for found in simgr.found:
        print(found.posix.dumps(0))

So far, so good, this is working. But now I need to do something different: my input should be constrained only to letters and numbers. This is not going to work obviously, because in this interval we have also other chars (slash, backslash, dot, etc).

I'm struggling in getting this working. I tried something like

init_state.solver.add(Or(And(k >= ord('A'),k <= ord('Z')),And(k >= ord('a'),k <= ord('z'))))

and several other variations, but no luck. Any suggestion on this?

Thanks!

Solution

OK, I found the solution:

  for byte in flag.chop(8):
    initial_state.solver.add(And(byte >= ord('A'), byte <= ord('Z')) | \
                             And(byte >= ord('a'), byte <= ord('z')) )

A small change to the script is required, this

flag_chars = [claripy.BVS('%d' % i, 8) for i in range(16)]
flag = claripy.Concat( *flag_chars + [claripy.BVV(b'\n')])

must be replaced with

flag = claripy.BVS("flag", 16 * 8)