# Chequered_flag

**short writeup**:

The binary takes an integer through command line and passes it to the 2 functions `check_1` and `check_2`

check_1 - Take each of the digits in number, raise it to No.Of digits, and then take their sum and compare it with the original number

check_2 - Take each of the digits in number, square it, and then take their sum,repeat this operation, if the above transformation yeilds 1 the fn returns True

After finding the number that satisfies check_1 and check_2
We then have a bunch of equations in `func` which can be solved using z3

#### Exploit

brute script - pypy/c can get faster results

Since check_2 uses recursion few values get calculated over and over(like in fibonacci using recursion) so check_2 can be optimized to get faster results

#include <stdio.h>
#include <math.h>
#include <stdbool.h>

bool check_2(int n) 
{
    int d=log10(n)+1;  //log10(n)+1 gives number of digits in n
    int sum=0;

    while(d>0) 
    {
        sum += (n%10)*(n%10);
        n = n/10;
        d--;
    }

    if (sum==1)
        return true;
    else if (sum / 10 == 0)
        return false;

    return check_2(sum);
}

bool check_1(int num)
{
    int original = num;
    int count = log10(num)+1;
    int sum=0;
    while(num)
    {
        sum+=pow(num%10,count);
        num = num/10;
    }

    if (sum^original)
        return false;
    return check_2(original);
}

int main(int argc, char const *argv[])
{
    int i=10;
    while(1)
    {
        if (check_1(i))
        {
            printf("%d\n",i);
            break;

        }
        i++;
    }

    return 0;
}

which yeilds `912985153` as our command line argument
`calculate` uses the above number and assigns few variables which are used in the equations in function `func`

Z3 script

from z3 import *

def calculate(n):
	global red,blue,black,white,pink
	i=0

	while(n>0):
		if ((i%2)==0):
			white*=(n%10)
		else:
			pink*=(n%10)

		red+=(n%10)
		blue|=(n%10)
		black^=(n%10)
		n = (n//10)
		i+=1
		
	white = white//black
	pink = pink//black


key = 912985153
red,blue,black,white,pink=33,47,0,1,1

calculate(key) 

s=Solver()

brr = [BitVec('g%s'%j,32) for j  in range(40) ]

length = 40


s.add(10 * length + brr[38] - (blue & black) == brr[28])
s.add(brr[28] % (10 * length) + 2 * pink + 5 * black / -3 == brr[22])
s.add(brr[38] + 2 * length + (blue ^ white) + 4 == brr[37])
s.add(4 * blue + 2 * brr[38] + 3 * red - blue - 2 * pink == brr[36])
s.add(brr[16] + 2 * length + (red | black) == brr[37])
s.add(brr[26] == brr[37] + 4 * pink + red - 8)
s.add(brr[9] == brr[16] + blue - 1)
s.add(2 * brr[16] - (red ^ white) - 21 == brr[33])
s.add(3 * (brr[39] >> 2) - (blue ^ pink) == brr[33] + 2)
s.add(brr[33] + 4 * length + 3 * (pink & blue) == brr[31])
s.add((blue ^ white) + brr[31] + 15 == brr[34])
s.add(-3 * length + 2 * (brr[19] + 3) == brr[31])
s.add((red & pink) / 2 + (red & blue) + brr[34] + length + (blue & pink) == brr[30])
s.add((black + 1) * brr[2] - (3 % length + black) == brr[34] % (blue * red))
s.add(brr[30] + 3 == (pink ^ blue) + 2 * brr[15])
s.add(2 * (brr[1] + 5 * length) + (blue ^ white) - 2 == brr[30])
s.add(2 * length + brr[1] + 1 == brr[29])
s.add(brr[35] - brr[1] == (white | red) + pink)
s.add(10 * length + brr[29] + 2 - (red & pink) == brr[5])
s.add(brr[28] == 983)
s.add(brr[18] - brr[29] == 32 * (red & black))
s.add(brr[32] - (white ^ pink) == 2 * (red | blue) + brr[5])
s.add(2 * (red ^ white) + brr[13] - 2 + (red | black) == brr[5])
s.add(brr[13] + 1 + (red & pink) == brr[25])
s.add(brr[23] - (brr[13] >> 2) == (black & red) * pink)
s.add(brr[25] + 2 * length + (blue ^ white) + black - 3 == brr[10])
s.add(brr[25] == brr[24] + 8 * length - black + 1)
s.add(brr[7] + (blue | black) + (red ^ white) % length - 1 == brr[10])
s.add(2 * length + brr[10] - 1 == brr[8])
s.add(brr[4] + 2 * length + (blue | black) - 3 == brr[7])
s.add(3 * brr[0] - 2 * length - 6 == brr[7])
s.add(brr[6] == brr[4] + blue - 2)
s.add(brr[27] % length + brr[27] + 2 * length + (red ^ white) + 6 == brr[4])
s.add(brr[27] + length + 4 == brr[3])
s.add(brr[27] == pink + brr[20] + 2 * length - black + 1)
s.add(3 * (brr[3] - length) - (blue ^ white) == brr[11])
s.add(4 * brr[3] - brr[3] % length - 21 == brr[12])
s.add(brr[14] == 980)
s.add(brr[11] == 32 * pink)
s.add((red ^ white ^ 2) + 2 * brr[21] + (blue & white) == brr[11])
s.add(brr[17] == 3 * (brr[21] - pink) + black - 1)


swapped = []

if s.check()==sat:
	b = s.model()
	for i in brr:
		swapped.append(b[i])

# we get the original array from the shuffled values 

even = []
odd = []


for i in range(20):
	odd.append(swapped[20:][i^1])

for i in range(20):
	even.append(swapped[:20][i^2])


new = []
k,l=0,0

for i in range(40):
	if i%2==0:
		new.append(even[k])
		k+=1
	else:
		new.append(odd[l])
		l+=1



inp = [BitVec('inp%s'%j,32) for j  in range(40) ]
s.reset()

j=25

for i in range(40):
	s.add(new[i]==inp[i]*(j/9)^(j+1))
	s.add(inp[i]>31,inp[i]<128)
	j+=3

flag="inctf{"

if s.check()==sat:
	b = s.model()
	for i in inp:
		flag+=chr(int(str(b[i])))


print("Argument: ",key)
print("Flag: ",flag+'}')

Argument:  912985153
Flag:  inctf{1t_15_l1ght5_0ut_4nd_w4y_Z3_g00_366b0c41}