Working with bitvectors
For this challenge we'll experiment with symbolizing registers and initializing at a different location than the entry point. We'll start by opening the binary and running some analysis.
shell@shell:~/github/r2angr/docs/challenges$ r2 03_angr_symbolic_registers
-- A git pull a day keeps the segfault away
[0x080483f0]> aaa
[x] Analyze all flags starting with sym. and entry0 (aa)
[x] Analyze function calls (aac)
[x] Analyze len bytes of instructions for references (aar)
[x] Check for objc references
[x] Check for vtables
[x] Type matching analysis for all functions (aaft)
[x] Propagate noreturn information
[x] Use -AA or aaaa to perform additional experimental analysis.
[0x080483f0]> s main
[0x080488a6]>Looking at the main function we can see it calls a sym.get_user_input() function, which calls scanf with "%x %x %s". In previous challenges we relied on angr to automatically symbolize stdin, but angr doesn't know how to deal with multiple stdin values automatically. Since the three inputs end up in eax, ebx, and edx, we'll try initializing after the function, symbolizing the registers manually, and then exploring as normal.
First we'll initialize a blank state at 0x80488d1, after the call to sym.get_user_input.
[0x080488a6]> Mi
[R2ANGR] Importing angr
[R2ANGR] Loading r2angr
[R2ANGR] Initialized r2angr at entry point
WARNING | 2020-06-15 17:54:43,382 | angr.sim_state | Unused keyword arguments passed to SimState: args
[0x080488a6]> Mib @ 0x80488d1
[R2ANGR] Initialized r2angr blank state at current address
[0x080488a6]>Then we'll symbolize the three registers with bitvectors using the Mbr command.
And we'll explore to the success branch.
We can list the active states.
Since we only care about the one at 0x8048937, we'll extract it and kill the others using the Mse command and the index.
Finally, we'll solve our bitvectors (which were used to symbolize the registers) using the Mbs command.
If we convert these to hex (since stdin used "%x %x %x"), we get db01abf7, 4930dc79, and d17de5ce. Let's try these as inputs to the binary.
Last updated
Was this helpful?