# TCTF

July 6th 2021

TCTF/0CTF Rev Writeups

# Writeups for Some 0CTF Challenges

## vp

Once I opened the binary in ghidra I saw a clone which spawns
a child after setting some seccomp rules and the parent just
waits for that, so I went to the main function of the child and
that just prints the welcome message, reads 0x68 bytes of input
from the user, that gets copied into a global and we call another
function before calling `_exit(2)`

Inside that another function, ghidra removed a few "unreachable"
blocks... Which were reachable, so I right clicked, properties
and unchecked the "eliminate unreachable code" in the Analysis Tab.
Ghidra then decided to load for a moment before revealing a ton of
code which consists of forks, then the child doing stuff in global
memory (And the vforks share that memory space, so it affects the
parent as well), while the parent just waits for it to die. We see
that all the child processes just call `_exit(2)`

at the end.

Then I spent a lot of time figuring out what all the globals do. At first I thought it was some sort of vm, because we first read a byte from an array (I assumed length of code), then we read three more bytes of that in a loop and did stuff with those bytes. As it turned out, that was not a vm, but more like constraints. The first byte was a direction (left, right, up, down). The second was the start position and the last byte was the expected result.

Now what do I mean with start position? Well, the first 100 bytes of the user input were used as a 10x10 grid. Then the direction was just in which direction we should go from our starting position. The starting position then was simply a number from one to ten indicating the row (for left, right) or column (for up, down). We then go through all ten fields in that row/column in the direction indicated by the first byte. While we do that, we check that every number from 1-10 occurs once as well as the number of times we get a new maximum along the way is the same as the third byte we have read from the array earlier.

So the first step was to solve this puzzle. I extracted the array of constants and parsed them, converting the data into data which needs less code to interpret (Starting position as absolute value from 0-100, direction converted to step size). Then I spent some time correctly implementing the constraints in z3. The script takes around 10 seconds, but finds a (i don't know if it's unique) solution to the quiz.

```
from z3 import *
arr = [BitVec(f"byte_{i}", 8) for i in range(100)]
s = Solver()
for i,x in enumerate(arr):
s.add(x >= 0)
s.add(x < 10)
visible = []
for j in range(10):
if j!=i//10: visible.append(arr[(i%10)+j*10])
if j!=i%10: visible.append(arr[(i//10)*10+j])
s.add(And(*[y != x for y in visible]))
s.add(arr[6] == 9)
s.add(arr[89] == 9)
def add_inversion_constraints(start, step, num, prev):
if len(prev) == 10:
return num == 0
if num < 0:
return False
return And(
Implies(
And([arr[start] > x for x in prev]),
add_inversion_constraints(start+step,step,num-1,prev+[arr[start]])
),
Implies(
And(Or([arr[start] < x for x in prev]), len(prev) > 0),
add_inversion_constraints(start+step,step,num,prev+[arr[start]])
)
)
s.add(add_inversion_constraints(8,10,2,[]))
s.add(add_inversion_constraints(2,10,3,[]))
s.add(add_inversion_constraints(5,10,4,[]))
s.add(add_inversion_constraints(4,10,2,[]))
s.add(add_inversion_constraints(90,-10,2,[]))
s.add(add_inversion_constraints(93,-10,2,[]))
s.add(add_inversion_constraints(91,-10,4,[]))
s.add(add_inversion_constraints(97,-10,3,[]))
s.add(add_inversion_constraints(99,-10,2,[]))
s.add(add_inversion_constraints(30,1,2,[]))
s.add(add_inversion_constraints(40,1,2,[]))
s.add(add_inversion_constraints(90,1,3,[]))
s.add(add_inversion_constraints(70,1,3,[]))
s.add(add_inversion_constraints(20,1,2,[]))
s.add(add_inversion_constraints(19,-1,2,[]))
s.add(add_inversion_constraints(69,-1,3,[]))
s.add(add_inversion_constraints(59,-1,2,[]))
s.add(add_inversion_constraints(9,-1,2,[]))
s.add(arr[6] == 9)
s.add(arr[89] == 9)
if s.check() == sat:
m = s.model()
for i in range(10):
for j in range(10):
idx = i*10+j
print(f"\\x0{hex(m[arr[idx]].as_long()+1)[2:]}",end="")
else:
print("OOF")
```

gives us

```
\x08\x04\x01\x03\x09\x02\x0a\x06\x05\x07\x06\x02\x03\x08\x05\x04\x01\x07\x0a\x09\x09\x08\x0a\x06\x02\x05\x03\x01\x07\x04\x05\x01\x02\x04\x03\x0a\x07\x09\x06\x08\x02\x0a\x05\x09\x07\x03\x06\x08\x04\x01\x01\x07\x04\x05\x06\x09\x08\x0a\x02\x03\x0a\x03\x06\x07\x01\x08\x04\x05\x09\x02\x04\x09\x07\x0a\x08\x06\x02\x03\x01\x05\x03\x06\x09\x01\x04\x07\x05\x02\x08\x0a\x07\x05\x08\x02\x0a\x01\x09\x04\x03\x06
```

Interestingly enough, this sometimes produced Error sometimes Correct, I don't know why, I suspect some bad interleaving though.

So we solved the puzzle and can continue in our code.
(Because if it wasn't correct, we just print "Error :("
and `_exit(2)`

). The rest of the code was pretty small,
still took quite some time to figure out that it just
takes the four extra bytes we sent (0x68 == 104), splits
them into to shorts, takes one as an offset into the array
(Which coincidentally is right before the stack). So we
only have to overwrite the return address to jump to the win
function which reads the flag file (After doing some xoring
to obfuscate the string "flag"). This function has the low two
bytes of `0x0cc8`

, so we get `\xc8\x0c`

as value to write
(Little endian) and we just have to get the correct offset into
the stack. During the clone call in the main function, we set
the stack to be at address 0x30c0c0, while the array starts
at address 0x304020. That means that our stack is at most at
offset 0x80a0. So I tried a few different addresses from there
on down in increments of 8. On my local machine the address
0x8008 always worked, on the remote it worked in like 1 out of
30 tries. But it worked and we got the flag by doing the thing
in a while loop lol

`while true; do echo -e "\x08\x04\x01\x03\x09\x02\x0a\x06\x05\x07\x06\x02\x03\x08\x05\x04\x01\x07\x0a\x09\x09\x08\x0a\x06\x02\x05\x03\x01\x07\x04\x05\x01\x02\x04\x03\x0a\x07\x09\x06\x08\x02\x0a\x05\x09\x07\x03\x06\x08\x04\x01\x01\x07\x04\x05\x06\x09\x08\x0a\x02\x03\x0a\x03\x06\x07\x01\x08\x04\x05\x09\x02\x04\x09\x07\x0a\x08\x06\x02\x03\x01\x05\x03\x06\x09\x01\x04\x07\x05\x02\x08\x0a\x07\x05\x08\x02\x0a\x01\x09\x04\x03\x06\xc8\x0c\x08\x80"|nc 111.186.59.32 20217 ; done`

eventually gave us

`flag{vvvvvfork_is_good_to_play_a_skycraper^.^}`

## FA51R_re

The gist of this challenge was that each function was in it's own
file. So I just sorted the files by size and started reversing.
Sometimes I decided to use the help of gdb to do some dynamic testing.
For that I set a breakpoint in `dyn_call`

and looked at the stack.
Then I just continued until the correct function-name was there.

Well, anyway the smaller functions were pretty easy to reverse, so I just commented on their functionality in a file

```
06b9d99befb919c2d9733cbf17b5d07a is help ==> just a bunch of puts() calls
0bd3c50f774fd998f9c6c816fa0a491b password_check();
188db852f6f3d80d36827185ec74a052 return (shm[0x120] = shm[0x120] * 0x41c64e6d + 0x3039 & 0x7FFFFFFF); // bitwise after addition/mult
1ee3b21edb88d9a3185690f021d94fa1 syscall, 1 argument (apart from number, sysnum in rdi, arg in rsi)
2184489db56112d2c0d8b7536abb075f prints the hello message (Just a wrapper for print)
2b438a4058cb3aa000bf20f133c51c75 wrapper for 1ee3b21edb88d9a3185690f021d94fa1(3, arg1) ==> close(fd)
2d725268ae170f36d65ca2c69b5fea31 syscall --> arguments are like this: rax=rdi, rdi=rsi, rsi=rdx, rdx=rcx (so just shift them)
2eef166f46bca4162fab0bf36f0e54d2 arg<<4 | arg >> 0xC ==> swap nibbles?
2aabc9ada0855def47eba259d9020d52 wrapper for 62e9 ==> syscall 2, arg1, arg2 ==> open(arg1, flags)
30cfeac00d70d975707889bcc2f53614 strcpy(arg1, arg2) == strcpy(dst, src)
31a8b2bbee5727f68282385e41119172 check if arg not in range(14, 32) ==> return arg == 32 || arg<14 ==> whitespace characters?
3445b01dfb9386195e8e3a07d49a3867 admin's menu option ==> same loop as before, but we don't have the binaries for those...
34ce68911ae2209b5eb82a272b56cdb3 3ab0(read_line(local_buf, 0x14));
3ab0ab6471f17f872b75a4da8235765b strtol (string to int conversion), arg1 buf, arg2 len, returns int
3e11029d5ac2211c31bdae5124c9795a move bits through array? ==> see code transcript below
508e799d314a8da19f966ca4936db71c strlen(char*src) -> int
5d8e3f065e0567b793b94e97a6633be6 is admin's password option
5f66dd0c765a66986c7ceb1acffb1371 return 0x96 < shm[4] (shm is a ushort*)
62e9418f31fac6ed6c736fa0fc47334c syscall, 2 extra args
632a2fa60bed84ae2a77d6bfbf6159dc is_digit(char num) -> bool ==> return param-0x10<10
6adf580f39636131583b54beeb6a9e9b weird bit checks?
6e88d889ecde3b574e5514c14d620a19 ret (... the file is two bytes, what did you expect?)
79482f2d1a19a683aa67b0e811f8f8bc print_menu(); // just a bunch of puts
79e908c9a12f9967a29d5be3e15bdb29 write(1, arg1, strlen(arg1)); // puts?
7e697c09cb0fcb076e2c59ddf9adb741 get_flag
8faae97b2c3830dddaf06f50b8bae7b6 2d72(0, arg1, arg2, arg3) ==> read(arg1, arg2, arg3) # fd, buf, num
90c588d11ce8422619c08eaaaf858c8b int_to_str (buf, num) --> ptr into buf, where num_str begins
92e99fe82dd7f91fa63c479d584b95ad int x = 188d(); return c8ec(x&0xF,x>>4);
93446c33d25b35ed390f2a8b9a5ea6a4 syscall (but no arguments apart from the syscall number; syscall number in rdi)
9e6c47893f0b949110f9c3a19e7e436f main_loop
d7075998ed4eb4e6c0d8692c05d08f6b ??? first in check_password ==> print timestamp & write that to global 0x120 ==> short index 0x90
b7679436c55a717ca2f2576f096e6084 exit(arg1), another wrapper
b8f1ef9d5ae177738dae64e46bccb3d1 login ==> if 0bd3(arg1, arg2) {print("yay"); return 1;} else {print("nay"); return 0;}
b9496737e1ed90fcd78b3be3806a7344 time (2d725268ae170f36d65ca2c69b5fea31(0xc9, 0, 0, 0) --> syscall time())
c05e47ecac8145772622412db0bb039e read_line(buf, max_len) // reads max_len or until null or newline
c7d66329b9e4428c8805c6d450bc9f8a shm[0x120] = param (DWORD)
c8ec4eba51c1a351c5d526b1175e2455 return (arg1 << (4 * arg3)) | ((short*)rodata)[arg2] << arg4 // i actually don't know if this is correct...
b0b68c5b3c9a52cfe072fd15b8437bb6 syscall (6 extra parameters?)
d8ecc9210b3d09343275867753028433 2d72(1, arg1, arg2, arg3) ==> write(arg1, arg2, arg3) # fd, buf, num
f018622565f4d85326122027e5bff1a5 syscall with more args (8 xmmwords on the stack, but only if al!=0)
f40f375263a5a4b078473cadc2746631 wrapper for syscall 0x3c ==> exit(arg1)
```

The main program also provides some rodata at address 0x600000000 and a shared memory space at address 0x700000000. After looking long enough that seemed to be a bunch of shorts at offset 0x1a8. As well as an int at offset 0x120. When we selected the login option from the menu, that was initialized to the timestamp and then used as seed for a basic prng.

Going through the binaries in order of their size made it really easy, because either we only do basic stuff or stuff that's already reversed or it's a wrapper for a bigger file, which is also quite easy.

For some of the files I wrote some pseudo C to better understand them:

```
code_3e11029d5ac2211c31bdae5124c9795a:
extern short *shm; // shared memory
for(int i = arg1; arg1 > 0; arg1--) {
shm[0xd4 + i] & ~arg2;
shm[0xd4 + i] |= (shm[0xd3 + i] & arg2);
}
code_6adf580f39636131583b54beeb6a9e9b:
extern short *shm; // shared memory
for(int i = 0; i < 4; i++) {
if(shm[0xd5 + i] & arg1) {
shm[0xd4 + i] |= arg1;
return;
}
}
shm[0xd8] |= arg1;
code_e40365731e828164ae4153f8cc3c7dc7:
short x = arg1;
for(int i = 0; i < 4; i++) {
if(arg2 >> (i + 4)) x = x>>4 | x<<0xc;
}
for(int i = 0; i < 4; i++) {
if(arg2 >> i) x = (x>>3 & 0x1111) | (x<<1 & 0xeeee);
}
return x;
code_30e23ac2f4b46087f0a0d2cb92a5de4f:
int i = 4;
while(i) {
bool x = false; // needs to be false to go to next index
ushort loc = shm[0xd4+i];
for(int j = 0; j < 4; j++) {
if((loc >> (j*4)) & 0xF == 0xF) {
x = true;
shm[4]++;
code_3e11(i, 0xF << (4 * j));
loc = shm[0xd4+i];
}
}
for(int j = 0; j < 4; j++) {
if(loc & (0x1111 << j) == (0x1111 << j)) {
x = true;
shm[4]++;
code_3e11(i, 0x1111 << j);
loc = shm[0xd4+i];
}
}
if(!x) i--;
}
code_41c24acbb388171678325e74b5837664:
int loc = 0;
while(loc < arg2 && shm[4] <= 0x96) {
int x = arg1[loc];
int y = code_92e9(); // int x = 188d(); return c8ec(x&0xF,x>>4);
957f(x, y);
loc++;
}
return 0;
code_957fd0e74de00cde1c7d052bd68b4a64:
short var1 = e403(arg2, arg1);
code_6adf(var1);
code_a113();
code_30e2();
return 0;
code_d7075998ed4eb4e6c0d8692c05d08f6b: // init_timestamp()
int t = time(arg1, arg2);
puts("Timestamp: ");
puts(int_to_str(t));
puts("\n");
code_c7d6(t);
code_0bd3c50f774fd998f9c6c816fa0a491b: // password_check
code_d707(arg1, arg2); // init_timestamp();
puts("input> ");
read_line(loc_418, 1000);
int len = strlen(loc_418);
code_41c2(loc_418, len); // actual password check here
return shm[4] > 0x96; // all characters passed the checks?
```

I also looked at the admin pw and flag options, but since I needed to login to access those I decided to not look into them further (I mean they probably just read the corresponding file and print the contents).

So I started in the login function, that just gets the time, prints that and sets the seed in the shared memory. Then I continued into the actual "password" check. I quickly realized that the login is not really a password since we never check anything about that without introducing some random into it.

So I started taking notes what actually was checked.
since `code_6adf580f39636131583b54beeb6a9e9b`

is called
with every of our inputs we see that the array is slowly
growing downards (if the numbers share the same bits).
And we had to prevent this array to grow more than 4
places down.

Next I looked at `code_3e11029d5ac2211c31bdae5124c9795a`

that moves the bits downards and clears the ones in
the short at offset `start`

.

Next `code_30e23ac2f4b46087f0a0d2cb92a5de4f`

does checks
on all the shorts in the array, those checks being
if either all bits in a nibble are 1 or if in all four
nibbles in the short the same bit is set. If that is the
case then we call the function to clear the bits.

After that I spent too much time implementing the code in python to simulate the game... twice. Luckily I did it twice as obviously there were some minor bugs.

First I implemented the piece generation which takes a random value and generates a piece based on a constant from rodata shifted by an amount and oring some other part of the random value.

```
data = [
0x0000,
0x0001,
0x0010,
0x0011,
0x0100,
0x0101,
0x0110,
0x0111,
0x1000,
0x1001,
0x1010,
0x1011,
0x1100,
0x1101,
0x1110,
0x1111
]
def transform_value(a, b, c, d):
return (a << (c << 2)) | (data[b] << d)
def transform_random_value(x):
# random value ==> takes nibbles and third nibble in two two-bit values and gives that to transform_values
return transform_value(x & 0xf, (x >> 4) & 0xf, (x >> 8 & 3), ((x >> 8) & 0xf) >> 2)
seed = 0x60e14dee # testing seed, change later
def rand(): # PRNG seeded by the timestamp
global seed
seed = (seed * 0x41c64e6d + 0x3039) & 0x7FFFFFFF
return seed
def mutate_char_based_on_random_variable(x, y):
for i in range(4):
if (y >> (i + 4)) & 1 == 1:
x = (x>>4 | x<<0xc) & 0xFFFF
for i in range(4):
if (y >> i) & 1 == 1:
x = ((x>>3 & 0x1111) | (x<<1 & 0xeeee)) & 0xFFFF
return x
```

now by calling `mutate_char_based_on_random_variable(transform_random_value(rand()), user_input)`

I could get the correct output...

So I wrote a simple bot which does not always work (It hangs itself because it can't find any good moves anymore). But it succeeds sometimes. It worked on both my implementations in python, but not on the binary.

It's always the dumb mistakes. And for this I made the beginning at the
very beginning. In `code_e40365731e828164ae4153f8cc3c7dc7`

during the first
loop I swapped the `>>`

and the `<<`

(it actually calls
`2eef166f46bca4162fab0bf36f0e54d2`

for which I actually have the right code
written right next to it.. But for some reason I failed to copy that down)

Anyhow, after fixing that my bot also worked correctly on the binary, so all I had to do was to run it on the remote. Once it found a solution I was able to get the flag and the admin password (Which was ultimately not used in our team).

Here the full solve script:

```
data = [
0x0000,
0x0001,
0x0010,
0x0011,
0x0100,
0x0101,
0x0110,
0x0111,
0x1000,
0x1001,
0x1010,
0x1011,
0x1100,
0x1101,
0x1110,
0x1111
]
seed = 0x60e14dee
shm = [0 for i in range(0x100)] # short array
def rand(): # PRNG seeded by the timestamp
global seed
seed = (seed * 0x41c64e6d + 0x3039) & 0x7FFFFFFF
return seed
def mutate_char_based_on_random_variable(x, y):
for i in range(4):
if (y >> (i + 4)) & 1 == 1:
x = (x<<4 | x>>0xc) & 0xFFFF;
for i in range(4):
if (y >> i) & 1 == 1:
x = ((x>>3 & 0x1111) | (x<<1 & 0xeeee)) & 0xFFFF;
return x
def mutate_state(value):
global shm
for i in range(4):
if(shm[0xd5 + i] & value) != 0:
shm[0xd4 + i] |= value
return
shm[0xd8] |= value
def check_cond():
global shm
if shm[0xd4] != 0:
return False
return True
def code_3e11(start, value):
global shm
for i in range(start,0,-1):
shm[0xd4 + i] &= (~value)
shm[0xd4 + i] |= (shm[0xd3 + i] & value)
def do_stuff_based_on_state():
i = 4
while i > 0:
x = False
loc = (shm[0xd4+i] & 0xFFFF)
for j in range(4):
if (loc >> (j*4)) & 0xF == 0xF:
x = True
shm[4] += 1
code_3e11(i, (0xF << (4 * j)) & 0xFFFF)
loc = shm[0xd4+i]
for j in range(4):
if loc & (0x1111 << j) == (0x1111 << j):
x = True
shm[4] += 1
code_3e11(i, (0x1111 << j) & 0xFFFF)
loc = shm[0xd4+i]
if not x:
i -= 1
xx = 0
def check_stuff(x, y):
global xx
var1 = mutate_char_based_on_random_variable(y, x)
#print(f"{var1 = } ({xx}. char)")
print(var1,end=",")
xx += 1
mutate_state(var1)
if not check_cond(): return False
do_stuff_based_on_state()
return True
def check_stuff_with_mutated_value(var1):
mutate_state(var1)
if not check_cond(): return False
do_stuff_based_on_state()
return True
def transform_value(a, b, c, d):
return (a << (c << 2)) | (data[b] << d);
def transform_random_value(x):
# random value ==> takes nibbles and third nibble in two two-bit values and gives that to transform_values
return transform_value(x & 0xf, (x >> 4) & 0xf, (x >> 8 & 3), ((x >> 8) & 0xf) >> 2)
def check_password(password):
global shm
for i in range(len(password)):
x = (password[i])
y = transform_random_value(rand())
if not check_stuff(x,y):
for i in range(5):
print(f"{i} ==> {hex(shm[0xd4+i])}")
print(f"Failed at character {i} == {(password[i])}")
return i
if shm[0x4] > 0x96:
print("GOT IT")
print(password)
break
print(shm[4])
return len(password)
"""
check_stuff_with_mutated_value(0b000000000001001)
check_stuff_with_mutated_value(0b000000000001011)
for i in range(5):
print(f"{i} ==> {shm[0xd4+i]}")
check_stuff_with_mutated_value(0b0000000000000001)
for i in range(5):
print(f"{i} ==> {shm[0xd4+i]}")
check_stuff_with_mutated_value(0b0000000000000110)
for i in range(5):
print(f"{i} ==> {shm[0xd4+i]}")
"""
def undo():
r = transform_random_value(rand()) # get random value for current char
vals = set()
for j in range(256):
x = r&0xFFFF
for i in range(4):
if (j >> (i + 4)) & 1 == 1:
x = (x<<4 | x>>0xc) & 0xFFFF
for i in range(4):
if (j >> i) & 1 == 1:
x = ((x>>3 & 0x1111) | (x<<1 & 0xeeee)) & 0xFFFF
"""
for i in range(4):
if (0xF<<(4*i))&x == (0xF<<(4*i)):
x &= ~(0xF<<(4*i))
for i in range(4):
if (0x1111 << i) & x == (0x1111<<i):
x &= (~(0x1111<<i))
"""
vals.add((r,x))
return sorted(list(vals))
def brute(r, y):
for j in range(256):
x = r&0xFFFF
for i in range(4):
if (j >> (i + 4)) & 1 == 1:
x = (x<<4 | x>>0xc) & 0xFFFF
for i in range(4):
if (j >> i) & 1 == 1:
x = ((x>>3 & 0x1111) | (x<<1 & 0xeeee)) & 0xFFFF
"""
for i in range(4):
if (0xF<<(4*i))&x == (0xF<<(4*i)):
x &= ~(0xF<<(4*i))
for i in range(4):
if (0x1111 << i) & x == (0x1111<<i):
x &= (~(0x1111<<i))
"""
if x == y:
return [j]
print("Not found")
exit(101)
from pwn import remote, process, gdb
rem = remote("111.186.58.164", 30333)
#rem = process("./main")
#rem = gdb.debug(["./main"])
x = rem.recvuntil("name:")
rem.sendline("admin")
rem.recvuntil("choice: ")
rem.sendline("1")
rem.recvuntil("Timestamp: ")
timestamp = int(rem.recvline().strip())
seed = timestamp
#seed = 1625387938
state = [0 for i in range(5)]
p = [undo() for i in range(1000)]
def evaluate_move(value, simulate=True):
global state
st = state.copy()
placed = False
for i in range(4):
if(st[i+1] & value) != 0:
st[i] |= value
placed = True
break
if not placed:
st[4] |= value
removed_pieces = 0
i = 4
while i > 0:
x = False
loc = st[i] & 0xFFFF
for j in range(4):
value = 0xF<<(j*4)
if loc & value == value:
x = True
removed_pieces += 1
for k in range(i,0,-1):
st[k] &= (~value)
st[k] |= (st[k-1] & value)
loc = st[i]
for j in range(4):
value = (0x1111 << j)
if loc & value == value:
x = True
removed_pieces += 1
for k in range(i,0,-1):
st[k] &= (~value)
st[k] |= (st[k-1] & value)
loc = st[i]
if not x:
i -= 1
zb = sum([1 if x == 0 else 0 for x in state])
za = sum([1 if x == 0 else 0 for x in st])
if not simulate:
state = st
return removed_pieces
return removed_pieces + (za-zb)
bias = 5
score = 0
inp = []
vals = []
for idx,v in enumerate(p):
moves = [[] for i in range(10)]
maxval = 0
for r,x in v:
val = evaluate_move(x)+bias
moves[val].append((r,x))
maxval = max(maxval, val)
making_move = moves[maxval][0]
score += evaluate_move(making_move[1], False)
inp += brute(making_move[0], making_move[1])
vals.append(making_move[1])
print(hex(making_move[1])[2:].rjust(4,'0'),end=" ==> ")
print([hex(x)[2:].rjust(4,'0') for x in state])
if score > 160:
ii = inp
inp = []
for x in ii:
if x == 0:
x = 0xF0
elif x == 10:
x = 5
inp.append(x)
print(inp)
print(timestamp)
print(vals)
seed = timestamp
check_password(bytes(inp))
with open("testinput", "wb") as f:
f.write(bytes(inp))
rem.sendline(bytes(inp))
rem.interactive()
exit(0)
```

Gives us the flag `flag{0ops! Dock menu overflow detected!afb11f59398789a08a3e5e60690d6726e5c5c1e1}`

which seems like a weird flag to me, maybe it's a hint for the pwn part.

## future (Leo did all the important work lol)

This binary used intel's new extension AMX which will be released on some server CPUs this year. Neither ghidra, binary ninja, nor IDA could reverse those instructions, luckily enough objdump could "correctly" translate the instructions. It failed at the arguments as we later learned however (mixing up stride and size with an offset)

At least IDA/Ghidra could decompile some functions, which were used to check the output of the computation. Namely the function at 0x4010960, which just compares 64 bytes, 0x4019d0 which checks that two float arrays are the same (each having 64 entries) and 0x401a80 doing the same but with unsigned int arrays. And 0x401b10 doing the same but comparing a float array with a 16 bit float array (16 bit like the ones used by the intel spec which are just 32 bit floats but only 7 bits mantissa, so much less precision)

Then we had to look at the main function located at 0x401bb0. We could look at the parts between the AMX instructions in ghidra/IDA to get a better understanding of them. Those pretty much just convert from a 32 bit integer array to a 16 bit float array. And then it nulls out the second part of the 256 bytes (so setting the floats to zero basically)

```
if (0 < height) {
iVar3 = 0;
iVar4 = 0;
iVar2 = 0;
do {
if (0 < width_in_bytes) {
lVar1 = 0;
do {
// not sure about indices but I guess it just converts all the input at param_2 to floats and stores them at short_arr
short_arr[2*iVar4 + lVar1/2] = (short)((uint)(float)*(int *)(param_2[lVar1 + iVar3/4]) >> 0x10); // store every second float
lVar1 = lVar1 + 4;
} while (lVar1 < width_in_bytes);
iVar4 = iVar4 + (width_in_bytes - 1U >> 2) + 1; // += 0x10, width_in_bytes is 0x20
}
iVar2 = iVar2 + 1;
iVar3 = iVar3 + width_in_bytes;
} while (height != iVar2);
}
// Clear out where we got our data from
for (lVar1 = 0x80; lVar1 != 0; lVar1 = lVar1 + -1) {
*param_2 = 0;
param_2 = param_2 + 1;
}
```

After manually decoding the tile config, we saw that only tile two was a 8 by 8 32-bit integer matrix which just contains the bits when unhexing the first 16 chars of our input. All other tiles are just 1x8 vectors.

This matrix then gets multiplied by the unit vector, that vector gets multiplied by tile two and added to the data already there, so basically we have

`tmp += tmp * (BM + I)`

Where BM is our input Bitmatrix and I is the identity 8x8 matrix. This gets repeated 4 times, after every time the data gets converted to floats and stored somewhere in memory. Then at address 0x4020d0 this process is over and we have the first few rows, the rest then gets filled up with the same as the 5th row (so row 5 through 8 all contain the same data). Then we load some constants, do one last matrix multiplication with floats this time and call the comparing function. So clearly we just have to find a matrix for which this check will succeed.

So we first dumbed all the constants (Which were luckily all formatted the
same way, with the movabs instruction) with a quick
`grep movabs future.s | cut -d" " -f3 | cut -d"," -f2`

on the objdump
code. Then we used

```
f16arr = []
for i in values[32:]:
print(hex(i))
for j in range(4):
print((i >> (16 * j)) & 0xFFFF)
v = unpack("f", b"\x00\x00"+pack("H", (i >> (16 * j)) & 0xFFFF))[0]
f16arr.append(v)
f32arr = []
for i in values[:32]:
hi = i>>32
lo = i&(1<<32)-1
hi = unpack("f", pack("I", hi))[0]
lo = unpack("f", pack("I", lo))[0]
f32arr.append(lo)
f32arr.append(hi)
```

to convert the values to the required formats. So we had 64 32-bit floats and 128 16-bit floats, which were stored in pairs of 2, so we had to get the two submatrices, one of which is multiplied by zero. The other is multiplied by our Result matrix built from the tmp results, the two results are then added, which means we don't have to worry about half of the constants (Every second will suffice)

So we can write this script to get the expected resulting matrix:

```
s=[0.099609375, 1.796875, 3.5, 5.1875, 6.875, 8.5625, 10.25, 12.0, 13.6875, 15.375, 17.0, 18.75, 20.5, 22.125, 23.875, 25.5, 0.3984375, 2.09375, 3.796875, 5.5, 7.1875, 8.875, 10.5625, 12.25, 14.0, 15.6875, 17.375, 19.0, 20.75, 22.5, 24.125, 25.875, 0.69921875, 2.390625, 4.09375, 5.78125, 7.5, 9.1875, 10.875, 12.5625, 14.25, 16.0, 17.625, 19.375, 21.0, 22.75, 24.5, 26.125, 1.0, 2.6875, 4.375, 6.09375, 7.78125, 9.5, 11.1875, 12.875, 14.5625, 16.25, 18.0, 19.625, 21.375, 23.0, 24.75, 26.5, 1.296875, 3.0, 4.6875, 6.375, 8.0625, 9.75, 11.5, 13.1875, 14.875, 16.5, 18.25, 20.0, 21.625, 23.375, 25.0, 26.75, 1.59375, 3.296875, 5.0, 6.6875, 8.375, 10.0625, 11.75, 13.5, 15.1875, 16.875, 18.5, 20.25, 22.0, 23.625, 25.375, 27.0, 1.8984375, 3.59375, 5.28125, 7.0, 8.6875, 10.375, 12.0625, 13.75, 15.5, 17.125, 18.875, 20.5, 22.25, 24.0, 25.625, 27.375, 2.1875, 3.890625, 5.59375, 7.28125, 9.0, 10.6875, 12.375, 14.0625, 15.75, 17.5, 19.125, 20.875, 22.5, 24.25, 26.0, 27.625]
e=[5483.724609375, 8271.57421875, 6230.849609375, 6473.162109375, 7995.32421875, 8923.44921875, 7128.099609375, 8612.724609375, 5574.630859375, 8408.357421875, 6333.333984375, 6579.833984375, 8128.279296875, 9071.591796875, 7244.537109375, 8755.193359375, 5661.162109375, 8538.517578125, 6430.818359375, 6681.318359375, 8254.861328125, 9212.611328125, 7355.224609375, 8890.787109375, 5760.662109375, 8688.287109375, 6543.162109375, 6798.193359375, 8400.287109375, 9374.693359375, 7483.037109375, 9046.787109375, 5842.724609375, 8811.583984375, 6635.537109375, 6894.349609375, 8520.271484375, 9508.333984375, 7587.849609375, 9175.349609375, 5941.224609375, 8960.068359375, 6746.849609375, 7010.162109375, 8664.318359375, 9668.943359375, 7714.599609375, 9329.724609375, 6032.099609375, 9096.841796875, 6849.318359375, 7116.818359375, 8797.248046875, 9817.060546875, 7831.037109375, 9472.162109375, 6118.662109375, 9227.005859375, 6946.818359375, 7218.318359375, 8923.849609375, 9958.099609375, 7941.724609375, 9607.787109375]
s1=s[0::2]
s2=s[1::2]
s1=[s1[i*8:i*8+8] for i in range(8)]
s2=[s2[i*8:i*8+8] for i in range(8)]
e=[e[i*8:i*8+8] for i in range(8)]
s1=Matrix(s1).transpose()
s2=Matrix(s2).transpose()
e=Matrix(e).transpose()
# x * s1 == e
# ==> e * s1.inverse() == x
r = flatten([[(y) for y in x] for x in (e*s1.inverse())])
print(r)
```

Now just a quick z3 script to get the correct input we need to have:

```
from z3 import *
def mult(d, x, y):
for i in range(8):
for k in range(8):
d[i] += x[k] * y[k*8+i]
R = [
0, 1, 0, 0, 1, 1, 0, 0,
2, 1, 1, 1, 2, 2, 0, 2,
4, 8, 4, 5, 8, 9, 4, 6,
19,25,19,20,27,29,19,30,
70,106,80,83,102,114,92,110,
70,106,80,83,102,114,92,110,
70,106,80,83,102,114,92,110,
70,106,80,83,102,114,92,110,
]
s = Solver()
y = [Int(f"{i}") for i in range(64)]
for i, x in enumerate(y):
s.assert_and_track(Or(x == 0, x == 1), f"{i}_one_zero")
x = [0 if i > 0 else 1 for i in range(8)]
t = [0 for i in range(8)]
for j in range(5):
mult(t, x, y)
tmp = x
x = t
t = tmp
for i in range(8):
s.assert_and_track(x[i] == R[i+j*8], f"{i}_{j}_R")
if s.check() == sat:
m = s.model()
vals="".join([str(m[x].as_long()) for x in y])
print(vals)
else:
print("OOF")
```

Then we only had to combine the bits, remember the endianess and get `328059c335ba44ee`

.

For the second part we simply had to extract the constants which were already captured by the grep earlier, then had to interpret them as floats. The second part was pretty easy as all it did was load the rest of the flag, unhexes them, each byte being one entry in a matrix. Then we do a packed dot product with constants, and each byte being quadrupled. This also needed to result in a constant matrix, so we could pretty easily reverse that:

```
s=[
0x792d,
0x57e4,
0x5557,
0x4d46,
0x213f,
0x42e7,
0x35ce,
0x4387,
0x7270,
0x5084,
0x5b24,
0x466c,
0x2729,
0x3472,
0x3a6e,
0x4c62,
0x581b,
0x44a2,
0x426e,
0x3d9a,
0x1493,
0x3632,
0x3032,
0x2f30,
0x7684,
0x4b5a,
0x4731,
0x4361,
0x206a,
0x3f34,
0x3953,
0x4814,
0x6d16,
0x3ffe,
0x4b08,
0x40c7,
0x1f09,
0x334b,
0x3af5,
0x47a0,
0x683b,
0x549e,
0x504d,
0x453b,
0x1ea6,
0x3c19,
0x35aa,
0x3c18,
0x68e6,
0x4abd,
0x4ded,
0x4169,
0x1c3a,
0x374a,
0x359f,
0x4102,
0x6e85,
0x4e31,
0x4924,
0x3f49,
0x219d,
0x394a,
0x308a,
0x44c8
]
r=[143742850,
1500679553,
1213089849,
2371309128,
1259016573,
520656013,
1149119617,
2350613097,
2469235085,
1059140166,
1115291789,
2055836527,
2303167263,
607136286,
224233739,
593263665,
306389906,
2503681068,
1394641664,
289080374,
823868953,
1763860601,
2440656165,
857621294,
1582268986,
930304874,
1886357596,
2186617869,
1125732242,
740190819,
1174611273,
1352020864,
2204250751,
2467299341,
831750976,
1849887034,
1999338643,
258539567,
723225355,
1262439038,
2090227780,
2085843224,
931013460,
1847889741,
17236616,
2037847101,
1754286365,
705512785,
2452696378,
1245857567,
1902850600,
1732658203,
1041465451,
2241020698,
460524438,
627463481,
327683886,
2187220237,
1868895109,
1818457928,
2454593061,
2049339708,
409810433,
1680381313]
s=[[j for j in s[i*8:i*8+8]] for i in range(8)] # make it 8x8
r=[[(j&0xFF) + ((j>>8) & 0xFF) + ((j>>16) & 0xFF) + ((j>>24) & 0xFF) for j in r[i*8:i*8+8]] for i in range(8)] # add the bytes, because each int is actually a pair of 4 bytes
s=Matrix(s)
r=Matrix(r)
print("".join(flatten([[hex(int(y))[2:] for y in x] for x in (r.inverse()*s)])))
```

now we only had to combine them to get the full flag of
`flag{328059c335ba44eef6bc269996101901bb046bd87fe49118d0e2308ecda708487bee2790f11c2506)`

< Slimes | DH MITM >