1

I have a binary that scanfs and then does some checks and returns either FAIL or SUCCESS that has SUCCESS for multiple inputs. Although only one of the inputs has only printable characters. How do I restrict angr to work with only printable characters entered into the scanf?

import angr

def main():
    proj = angr.Project('a.out')
    init_state = proj.factory.entry_state()
    simulation = proj.factory.simgr(init_state)
    simulation.explore(find=lambda s: b"SUCCESS\n" in s.posix.dumps(1))
    
    for solution in simulation.found:
        print(solution.posix.dumps(0), solution.posix.dumps(1))

if __name__ == '__main__':
    main()

This gives me an output containing a lot of unprintable \xDD where DD is a hex number. Can I restrict angr to use only printable characters when exploring and how; or how do I prevent angr from stopping after it finds one solution to get to the SUCCESS message. Currently although there are multiple solutions it finds one and only ONE.

0

Providing you know the length of the flag (obtain for example from RE) you can modify your code in the following way:

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

That will create an array with 15 (in this example) bit vectors of the size of 8-bits. And on the following line we will concatenate them (+ new line value) to obtain one value that we can operate on.

Next, we pass the flag to create our state.

 init_state = proj.factory.entry_state(stdin=flag)

Having the init state, we can restrict the flag:

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

The rest stays the same.

Full program:

import angr
import claripy

def main():
    proj = angr.Project('a.out')
    flag_chars = [claripy.BVS('flag_%d' % i, 8) for i in range(15)]
    flag = claripy.Concat(*flag_chars+[claripy.BVV(b'\n')])

    init_state = proj.factory.entry_state(stdin=flag)

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

    simulation = proj.factory.simgr(init_state)
    simulation.explore(find=lambda s: b"SUCCESS\n" in s.posix.dumps(1))

    for solution in simulation.found:
        print(solution.posix.dumps(0), solution.posix.dumps(1))


if __name__ == '__main__':
    main()
| improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.