Points: 250

Solves: 166

Description:

Future me gave me this and told me to add it to TUCTF. I dunno, he sounded crazy. Anyway, Let’s see what’s so special about it.

NOTE: If you find a solution that was not intended, then msg me on Discord @scrub

`future - md5: 30a6b3fe92a65271bac7c4b83b303b55`

flag format: TUCTF{…}

Given:

`future.c`

`future`

# Solution:

(by L0rdComm4nder)

### TLDR

1. Encode everything in Z3
2. Search for the flags that start with `TUCTF{`

## Description

The goal of this ask is to provide a 25 byte string as input that after processed by `genMatrix` and `genAuthString` should match `pass`.

``````void genMatrix(char mat[5][5], char str[]) {
for (int i = 0; i < 25; i++) {
int m = (i * 2) % 25;
int f = (i * 7) % 25;
mat[m/5][m%5] = str[f];
}
}

void genAuthString(char mat[5][5], char auth[]) {
auth[0] = mat[0][0] + mat[4][4];
auth[1] = mat[2][1] + mat[0][2];
auth[2] = mat[4][2] + mat[4][1];
auth[3] = mat[1][3] + mat[3][1];
auth[4] = mat[3][4] + mat[1][2];
auth[5] = mat[1][0] + mat[2][3];
auth[6] = mat[2][4] + mat[2][0];
auth[7] = mat[3][3] + mat[3][2] + mat[0][3];
auth[8] = mat[0][4] + mat[4][0] + mat[0][1];
auth[9] = mat[3][3] + mat[2][0];
auth[10] = mat[4][0] + mat[1][2];
auth[11] = mat[0][4] + mat[4][1];
auth[12] = mat[0][3] + mat[0][2];
auth[13] = mat[3][0] + mat[2][0];
auth[14] = mat[1][4] + mat[1][2];
auth[15] = mat[4][3] + mat[2][3];
auth[16] = mat[2][2] + mat[0][2];
auth[17] = mat[1][1] + mat[4][1];
}

int main() {
char flag[26];
printf("What's the flag: ");
scanf("%25s", flag);
flag[25] = 0;

if (strlen(flag) != 25) {
puts("Try harder.");
return 0;
}

// Setup matrix
char mat[5][5];// Matrix for a jumbled string
genMatrix(mat, flag);
// Generate auth string
char auth[19]; // The auth string they generate
auth[18] = 0; // null byte
genAuthString(mat, auth);

// Check the input
if (!strcmp(pass, auth)) {
puts("Yup thats the flag!");
} else {
puts("Nope. Try again.");
}

return 0;
}
``````

Since the conditions associated with `genMatrix` and `genAuthString` are pretty simple, we can just encode everything in Z3 and check for the viable solutions

``````#!/usr/bin/env python3
from z3 import *

s = Solver()
flag = [BitVec('flag_%d' % i, 8) for i in range(25)]
mat = [ [BitVec('mx_%d_%d' % (i,j), 8) for j in range(5)] for i in range(5) ]
auth = [BitVec('auth_%d' % i, 8) for i in range(18)]

# conditions on genMatrix
for i in range(25):
m = (i * 2) % 25
f = (i * 7) % 25

# conditions on genAuthString
s.add(auth[7] == mat[3][3] + mat[3][2] + mat[0][3])
s.add(auth[8] == mat[0][4] + mat[4][0] + mat[0][1])

for i in range(18):

# flag characters are printable
for i in range(len(flag)):

# flag starts with TUCTF{
target="TUCTF{"
for i in range(len(target)):

rounds=0
while z3.sat == s.check():
rounds += 1
m = s.model()
plaint = "".join([ chr(int(repr(m[flag[i]]))) for i in range(len(flag)) ])
print plaint
block = []
for i in range(len(flag)):
block.append( flag[i] != m[flag[i]])
``````

After running all the possible results

``````TUCTF{5y579m5Y0`_4_d0wt!w
TUCTF{5y57@m5R0Y_4_d0w{!p
TUCTF{5y57Bm5P0W_4_d0w}!n
TUCTF{5y57Am5Q0X_4_d0w|!o
TUCTF{5y572m5`0g_4_d0wm!~
TUCTF{5y574m5^0e_4_d0wo!|
TUCTF{5y573m5_0f_4_d0wn!}
TUCTF{5y57Cm5O0V_4_d0w~!m
TUCTF{5y57;m5W0^_4_d0wv!u
TUCTF{5y57<m5V0]_4_d0ww!t
TUCTF{5y57>m5T0[_4_d0wy!r
TUCTF{5y57=m5U0\_4_d0wx!s
TUCTF{5y576m5\0c_4_d0wq!z
TUCTF{5y575m5]0d_4_d0wp!{
TUCTF{5y57?m5S0Z_4_d0wz!q
TUCTF{5y57:m5X0__4_d0wu!v
TUCTF{5y578m5Z0a_4_d0ws!x
TUCTF{5y577m5[0b_4_d0wr!y
``````

Voilà the correct one was `TUCTF{5y573m5_0f_4_d0wn!}`.