METACTF Quals 24 Rev/Starkore

Hello You.

Let’s get right to solving this challenge

$ file starkore             
starkore: ELF 64-bit LSB pie executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, BuildID[sha1]=b74e95dd371d2e8cf28958feb4afd0cb5fe9a586, for GNU/Linux 3.2.0, not stripped

Executing strings will yield this

^[A-Z0-9]{4}-[A-Z0-9]{4}-[A-Z0-9]{4}-[A-Z0-9]{4}-[A-Z0-9]{4}$
%04X
HELLO, PLEASE ENTER A VALID KEY: 
WELCOME, MR STARK! BOOTING UP...
flag.txt
Couldn't open file
KEY INCORRECT!
SHUTTING DOWN

here we can see regex for something, we don’t know yet what it is, but it super interesting, if you are new to regex you can use regex101 to understand what it is about

Knowing that a possible value that fits this regex would be ASDF-QWER-ZXCV-1234-as12

executing ltrace yields this

$ ltrace ./starkore 
printf("HELLO, PLEASE ENTER A VALID KEY:"...)                                                                                     = 33
fgets(HELLO, PLEASE ENTER A VALID KEY: key
"key\n", 100, 0x7f6e790c1aa0)                                                                                               = 0x7ffd874f51d0
strcspn("key\n", "\n")                                                                                                            = 3
strcpy(0x7ffd874f50d0, "key")                                                                                                     = 0x7ffd874f50d0
regcomp(0x7ffd874f50f0, 0x5601b6ecc008, 1, 0x5601b6ecc008)                                                                        = 0
strtok("key", "-")                                                                                                                = "key"
sprintf("0", "%d", 0)                                                                                                             = 1
strlen("0")                                                                                                                       = 1
sprintf("3653", "%04X", 0x3653)                                                                                                   = 4
strcmp("3653", "key")                                                                                                             = -56
sprintf("1", "%d", 1)                                                                                                             = 1
strlen("1")                                                                                                                       = 1
sprintf("2672", "%04X", 0x2672)                                                                                                   = 4
strcmp("2672", "key")      
...
...                                                                                                       = -57

we’ll get to this later, however

Now let’s start reversing

Here you can use any decompiler you want, I used IDA

main

It is super simple main, it just takes user input then sends it to checkKey and if it’s correct it opens the flag.txt file and print its content, other than that, it will print Incorrect... and exit.

checkKey

IDA did me wrong here and didn’t identify the array, but in line 48 the expression &v6 + k gave me a hint to revisit the block where the v6, v7 ... were initialized, and you can see they are adjacent.

In this function you can see the use of regcomp & strtok. However, in the for loop it takes each part and compares it with a value that gets out of the wired long named function Crc... I didn’t really care what it does but I knew that it is the function that generates the values that I saw from the ltrace output.

So, It comapres the value that gets generated from Crc… to the part of the key and if it is the same it will put the value of the j which goes from 0 to 100 in 1.1 sec lol nvm,,, and breaks out of the loop 5 times

In the last line there is a simple equation, I used z3 to get the values that satisfies the result which is 1337

from z3 import *

v = [Int(f'v{i}') for i in range(6, 11)]

solver = Solver()

solver.add(v[2] + v[1] * v[0] - v[3] + v[4] == 1337)
for var in v:
    solver.add(var >= 0, var <= 100)

if solver.check() == sat:
    model = solver.model()
    solution = [model[var].as_long() for var in v]
    print(f"Solution: {solution}")
else:
    print("No solution found")

As you know z3 won’t give you the best solution but it will give you a solution, and here it doesn’t really matter any solution is good

Solution: [99, 12, 95, 42, 96]

Here I went back to ltrace output, I wrote this line to get the values

$ egrep -io 'strcmp\("(.*)"\,|strlen\("[^"]*"' ltrace.out | egrep -o '[0-9A-Z]{1,4}'

then I wrote another python script:

l = """0
3653
1
2672
2
1611
...
...
97
F9B9
98
0856
99
1877
100
C153"""

l = l.split()
sol = [99, 12, 95, 42, 96]

key = '-'.join([l[l.index(str(i)) + 1] for i in sol])
print(key)

And that’s how I got the flag

$ nc challenges.cscpsut.com 10528
HELLO, PLEASE ENTER A VALID KEY: 1877-20B5-D9FB-DF40-E998
WELCOME, MR STARK! BOOTING UP...

METACTF{31381fe3-7f32-4e72-bb21-1b91da559501}

I hope you enjoyed reading the write up, have a great day cya…