# future
Full disclosure, the solution I found and talk about in here is an unintended solution (got the intended flag after showing my solution to an admin). If you want the intended solution, look at a different writeup. 
Let's take a look at the binary:
```$	file futurefuture: ELF 32-bit LSB shared object, Intel 80386, version 1 (SYSV), dynamically linked, interpreter /lib/ld-linux.so.2, for GNU/Linux 2.6.32, BuildID[sha1]=d6e528233c162804c1b358c2e15be38eb717c98a, not stripped$	./future What's the flag: TUCTF{heres_a_flag}Try harder.```
So it is a 32 bit binary, and when we run it it prompts us for the flag. Luckily for this one we're given the source code. Let's take a look at it:
```$	cat future.c #include <stdio.h>#include <string.h>#include <stdlib.h>
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;}```
So looking at the source code, we can tell what the program does. It scans in up to 25 bytes of input, checks to make sure that it scanned in 25 bytes. Then it creates a 5 by 5 matrix, and stores the 25 bytes in the matrix in a slightly obscure way. Then it takes the matrix and performs 19 different additions using 2-3 different matrix values for each iteration. It then compares the output of that to a a predefined answer `pass`. If they are the same, then you have the flag.
So first we need to figure out how our input is stored in the matrix. For that, python can help. There are three different values we need to worry about in the `genMatrix` function `f`,  `m/5`, and `m%5`:
```>>> for i in xrange(25):...     print ((i * 2) % 25) / 5... 0001122233444001112233344>>> for i in xrange(25):...     print ((i * 2) % 25) % 5... 0241302413024130241302413>>> for i in xrange(25):...     print ((i * 7) % 25) ... 0714213101724613202916235121918152241118```
Putting it all together, we find that this is how our input is stored in the5 by 5 matrix:
```matrix[0][0] = input[0]matrix[0][2] = input[7]matrix[0][4] = input[14]matrix[1][1] = input[21]matrix[1][3] = input[3]matrix[2][0] = input[10]matrix[2][2] = input[17]matrix[2][4] = input[24]matrix[3][1] = input[6]matrix[3][3] = input[13]matrix[4][0] = input[20]matrix[4][2] = input[2]matrix[4][4] = input[9]matrix[0][1] = input[16]matrix[0][3] = input[23]matrix[1][0] = input[5]matrix[1][2] = input[12]matrix[1][4] = input[19]matrix[2][1] = input[1]matrix[2][3] = input[8]matrix[3][0] = input[15]matrix[3][2] = input[22]matrix[3][4] = input[4]matrix[4][1] = input[11]matrix[4][3] = input[18]```
The mathematical operations done with the matrix is made clear in the source code. So now that we know how our input is scanned in, stored in the matrix, the algorithm the data is ran through, and the desired outpu tit's compared against. We can just write a bit of python code which will use Microsoft's z3 theorem solver to figure out the input we need to get an output:
```#Import z3from z3 import *
#Designate the input z3 will have control ofinp = []for i in xrange(25):	b = BitVec("%s" % i, 8)	inp.append(b)#Store the input from z3 in the matrixh, l = 5, 5;mat = [[0 for x in range(l)] for y in range(h)]mat[0][0] = inp[0]mat[0][2] = inp[7]mat[0][4] = inp[14]mat[1][1] = inp[21]mat[1][3] = inp[3]mat[2][0] = inp[10]mat[2][2] = inp[17]mat[2][4] = inp[24]mat[3][1] = inp[6]mat[3][3] = inp[13]mat[4][0] = inp[20]mat[4][2] = inp[2]mat[4][4] = inp[9]mat[0][1] = inp[16]mat[0][3] = inp[23]mat[1][0] = inp[5]mat[1][2] = inp[12]mat[1][4] = inp[19]mat[2][1] = inp[1]mat[2][3] = inp[8]mat[3][0] = inp[15]mat[3][2] = inp[22]mat[3][4] = inp[4]mat[4][1] = inp[11]mat[4][3] = inp[18]#print mat
#Perform the 19 math operations with the matrixauth = [0]*19auth[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]	#print auth
#Create the solver, and the desired outputz = Solver()enc = [0x8b, 0xce, 0xb0, 0x89, 0x7b, 0xb0, 0xb0, 0xee, 0xbf, 0x92, 0x65, 0x9d, 0x9a, 0x99, 0x99, 0x94, 0xad, 0xe4]
#Create the z3 constraints for what the output should be:#equal to it's corresponding enc value#an ascii character to make it easier to input into the programfor i in xrange(len(enc)):#	print enc[i]	z.add(auth[i] == enc[i])for i in xrange(25):	z.add(inp[i] > 32)	z.add(inp[i] < 127)
#Check if z3 can solve it, and if it can print out the solutionif z.check() == sat:#	print z	print "Condition is satisfied, would still recommend crying: " + str(z.check())	solution = z.model()	print solution
#Check if z3 can't solve itif z.check() == unsat:	print "Condition is not satisfied, would recommend crying: " + str(z.check())```
when we run it:
```python solve.py Condition is satisfied, would still recommend crying: sat[13 = 62, 15 = 69, 21 = 118, 8 = 85, 2 = 66, 6 = 99, 19 = 116, 16 = 80, 20 = 64, 3 = 38, 10 = 84, 14 = 47, 18 = 63, 7 = 96, 9 = 64, 4 = 86, 23 = 58, 5 = 91, 1 = 110, 17 = 77, 22 = 118, 0 = 75, 12 = 37, 24 = 92, 11 = 110]```
and when we take the solution z3 gave us, reorganize it in a sequential order and convert it to ascii we get the string ``KnB&V[c`U@Tn%>/EPM?t@vv:\`` . When we try it:
```$	./future What's the flag: KnB&V[c`U@Tn%>/EPM?t@vv:\Yup thats the flag!```
after talking to an admin about my solution, he gave me the real flag which is `TUCTF{5y573m5_0f_4_d0wn!}`.
Just like that, we captured the flag using an unintended solution!