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

A traditional key-checker

  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);   
    char pass[19] = "\x8b\xce\xb0\x89\x7b\xb0\xb0\xee\xbf\x92\x65\x9d\x9a\x99\x99\x94\xad\xe4\x00";
    
    // 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
    s.add(mat[m/5][m%5] == flag[f])

# conditions on genAuthString
s.add(auth[0] == mat[0][0] + mat[4][4])
s.add(auth[1] == mat[2][1] + mat[0][2])
s.add(auth[2] == mat[4][2] + mat[4][1])
s.add(auth[3] == mat[1][3] + mat[3][1])
s.add(auth[4] == mat[3][4] + mat[1][2])
s.add(auth[5] == mat[1][0] + mat[2][3])
s.add(auth[6] == mat[2][4] + mat[2][0])
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])
s.add(auth[9] == mat[3][3] + mat[2][0])
s.add(auth[10] == mat[4][0] + mat[1][2])
s.add(auth[11] == mat[0][4] + mat[4][1])
s.add(auth[12] == mat[0][3] + mat[0][2])
s.add(auth[13] == mat[3][0] + mat[2][0])
s.add(auth[14] == mat[1][4] + mat[1][2])
s.add(auth[15] == mat[4][3] + mat[2][3])
s.add(auth[16] == mat[2][2] + mat[0][2])
s.add(auth[17] == mat[1][1] + mat[4][1])

passwd = "\x8b\xce\xb0\x89\x7b\xb0\xb0\xee\xbf\x92\x65\x9d\x9a\x99\x99\x94\xad\xe4\x00"

for i in range(18):
    s.add(auth[i] == ord(passwd[i]))

# flag characters are printable
for i in range(len(flag)):
    s.add(flag[i] >= 32)
    s.add(flag[i] <= 126)

# flag starts with TUCTF{
target="TUCTF{"
for i in range(len(target)):
    s.add(flag[i] == ord(target[i]))


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]])
    s.add(Or(block))

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