October 2018 – youremindmeofmymother

Intro

This post tries to demonstrate the awesome power of using symbolic execution, SMT SAT solvers, all easily accessible through a framework called Angr.

I won’t go into too much detail about Angr but rest assured that the contributors of Angr are doing a great job documenting its features, and many posts have been written demonstrating Angr being used for ctf challenges.

This simple ctf challenge is taken from http://pwnable.kr/ collision challenge. Nothing difficult that can’t be solved mentally, but why use a flint when you can use a knife.

My personal goal is to become more familiar with Angr, so I will try to avoid looking at the challenge binary’s source code, and gather the minimal amount of information of the binary’s internal logic, but just enough to get Angr to come up with a solution.

The following is the plan of action we’ll take

Determine the goal of the challenge, through static and dynamic analysis
Configure Angr to obtain solution

The challenge

Let’s login to the hosting server and run the binary.

$ ssh col@pwnable.kr -p2222
col@pwnable.kr’s password:
____ __ __ ____ ____ ____ _ ___ __ _ ____
| \| |__| || \ / || \ | | / _] | |/ ]| \
| o ) | | || _ || o || o )| | / [_ | ‘ / | D )
| _/| | | || | || || || |___ | _] | \ | /
| | | ` ‘ || | || _ || O || || [_ __ | \| \
| | \ / | | || | || || || || || . || . \
|__| \_/\_/ |__|__||__|__||_____||_____||_____||__||__|\_||__|\_|

– Site admin : daehee87.kr@gmail.com
– IRC : irc.netgarage.org:6667 / #pwnable.kr
– Simply type “irssi” command to join IRC now
– files under /tmp can be erased anytime. make your directory under /tmp
– to use peda, issue `source /usr/share/peda/peda.py` in gdb terminal
Last login: Thu Oct 11 20:56:27 2018 from 47.37.48.199
col@ubuntu:~$ ./col
usage : ./col [passcode]
col@ubuntu:~$ ./col A
passcode length should be 20 bytes

So we need to provide some command line argument of 20 bytes in length.

Lets’s take a look at the binary in Binary Ninja and gather some info on the program’s logic.

We can see the first branch from 0x11be checks to see if an argument has been passed. 0x11f9 then checks if the argument is 20 bytes long. The third block calls the function check_password(), compares the result and issues a system call to run ‘/bin/cat flag’

So if the supplied argument matches some value then the binary will display the contents of the flag file.

Does the binary contain a hardcoded value that the argument must match?

There doesn’t appear to be any obvious hardcoded check in check_password(). However, back in main() at 0x1125 we see that a return value from check_password() in moved into rdx and a symbol called hashcode is moved into rda. At 0x122f a comparison is made between rda and rdx which results in our cat flag.

At first, one might assume that entering the hashcode value (0x21dd09ec) as user input would be the solution. Well it doesn’t meet the program’s input length requirement.

So, some kind of manipulation on the user input is taking place in check_password().

We could look into how the user input is manipulated and compared to hashcode, and figure out what the correct input should be. But hey, we have angr at hand.

The solution

Now, Angr is pretty powerful and has many options to help you achieve your goal. I’m still discovering some of Angr’s features.

I do know that to get Angr towards a solution, we’ll need to feed its solver some basic information, which are the following:

Start address within the binary
A list of addresses which the symbolic execution should avoid, to help reduce the time to solve
A final address, which when reached, guarantees that the problem has been solved and the solution (modified user input matches the hashcode) is obtainable from Angr’s virtual machine.

We feed the binaries main() address as Angr’s initial state
During the analysis phase we identified branch points which would divert away from the cat flag system call. These branch off points will be fed into Angr as avoid parameters.
We know that if angr returns a solution that reaches the cat flag system call, then the input supplied to check_password() should be somewhere in memory. After running the program through gdb, I identified that rdi register contained the address pointing to the unmodified user input.

The angr script below is the solution.

#!/usr/bin/python2
# coding: utf-8
”’
Use this script to solve the collision challenge on http://pwnable.kr/play.php.
”’
import angr #the main framework
import claripy #the solver engine
import signal
import logging

logging.getLogger(‘angr.manager’).setLevel(logging.DEBUG)

def killmyself():
os.system(‘kill %d’ % os.getpid())
def sigint_handler(signum, frame):
print ‘Stopping Execution for Debug. If you want to kill the programm issue: killmyself()’
if not “IPython” in sys.modules:
import IPython
IPython.embed()

signal.signal(signal.SIGINT, sigint_handler)

# col-dyn-32 is a locally compiled version of the binary on the server.
proj = angr.Project(“/mnt/hgfs/Dropbox/Dev/ctf/col-dyn”, auto_load_libs=False)

”’
At this point rdi will contain user input that satifies SMT
”’
find_addr = 0x401234

”’
These avoid addresses were obtained after disassembling binary in binja
”’
avoid_addr = [0x40124c, 0x4011c4, 0x4011ff]

main=0x4011af # entry point

state = proj.factory.blank_state(addr=main,add_options={angr.options.LAZY_SOLVES})
simgr = proj.factory.simulation_manager(state)

simgr.explore(find=find_addr,avoid=avoid_addr)

”’
found will contain a successful simulation object that will contain a user input
that satisfies the check_password function.
”’
found = simgr.found[0]

”’
When observing the binary running in gdb, it becomes apparent that the user input
can be obtained through a pointer in rdi register.
”’
chunk1 = found.mem[found.regs.rdi].deref
# 0x9539ef802c6dc9c9
chunk2 = found.mem[found.regs.rdi+8].deref
# 0x5990224028afaea0
chunk2 = found.mem[found.regs.rdi+8+8].deref
# 0xddf57fc3

”’
Reverse order the bytes based on memory boundary (64bit = 8 byte)
”’
print chunk1[::-1].encode(‘hex’)
# c9c96d2c80ef3995

print chunk2[::-1].encode(‘hex’)
# a0aeaf2840229059

print chunk3[::-1].encode(‘hex’)
# c37ff5dd

# \xc9\xc9\x6d\x2c\x80\xef\x39\x95\xa0\xae\xaf\x28\x40\x22\x90\x59\xc3\x7f\xf5\xdd

”’
Now we submit the challenge to obtain the flag.

$ ssh col@pwnable.kr -p2222
The authenticity of host ‘[pwnable.kr]:2222 ([143.248.249.64]:2222)’ can’t be established.
ECDSA key fingerprint is SHA256:kWTx0QCL5U5VbUkQa1x5/dw8hJ6DS5CR0KilMRJnUYY.
Are you sure you want to continue connecting (yes/no)? yes
Warning: Permanently added ‘[pwnable.kr]:2222,[143.248.249.64]:2222’ (ECDSA) to the list of known hosts.
col@pwnable.kr’s password:
____ __ __ ____ ____ ____ _ ___ __ _ ____
| \| |__| || \ / || \ | | / _] | |/ ]| \
| o ) | | || _ || o || o )| | / [_ | ‘ / | D )
| _/| | | || | || || || |___ | _] | \ | /
| | | ` ‘ || | || _ || O || || [_ __ | \| \
| | \ / | | || | || || || || || . || . \
|__| \_/\_/ |__|__||__|__||_____||_____||_____||__||__|\_||__|\_|

– Site admin : daehee87.kr@gmail.com
– IRC : irc.netgarage.org:6667 / #pwnable.kr
– Simply type “irssi” command to join IRC now
– files under /tmp can be erased anytime. make your directory under /tmp
– to use peda, issue `source /usr/share/peda/peda.py` in gdb terminal
Last login: Thu Oct 11 20:45:35 2018 from 207.148.113.134
col@ubuntu:~$ ./col $(perl -e ‘printf “\xc9\xc9\x6d\x2c\x80\xef\x39\x95\xa0\xae\xaf\x28\x40\x22\x90\x59\xc3\x7f\xf5\xdd”‘)
daddy! I just managed to create a hash collision :)
”’

https://github.com/muttiopenbts/pwnable.kr/blob/master/angr-session1.py

Note: The memory addresses fed into Angr have a slightly different offset to those from binary ninja.