README.md

1337UP LIVE CTF 2023

FlagChecker

Can you beat this FlagChecker?

Author: Jopraveen

flagchecker, source.rs

Tags: rev

Solution

We get a rust source file and the compiled binary for this challenge. Inspecting the rust code, we see the flag checker basically checks for a lot of constraints.

flag.as_bytes()[18] as i32 * flag.as_bytes()[7] as i32 & flag.as_bytes()[12] as i32 ^ flag.as_bytes()[2] as i32 == 36 &&
flag.as_bytes()[1] as i32 % flag.as_bytes()[14] as i32 - flag.as_bytes()[21] as i32 % flag.as_bytes()[15] as i32 == -3 &&
flag.as_bytes()[10] as i32 + flag.as_bytes()[4] as i32 * flag.as_bytes()[11] as i32 - flag.as_bytes()[20] as i32 == 5141 &&
flag.as_bytes()[19] as i32 + flag.as_bytes()[12] as i32 * flag.as_bytes()[0] as i32 ^ flag.as_bytes()[16] as i32 == 8332 &&
flag.as_bytes()[9] as i32 ^ flag.as_byte...

This of course calls for z3. Writing a solver script gives us the flag.

from z3 import *

# Create a BitVec array for the flag
flag = [BitVec('flag_%d' % i, 8) for i in range(22)]

# Define the conditions
conditions = [
    flag[18] * flag[7] & flag[12] ^ flag[2] == 36,
    flag[1] % flag[14] - flag[21] % flag[15] == -3,
    flag[10] + flag[4] * flag[11] - flag[20] == 5141,
    flag[19] + flag[12] * flag[0] ^ flag[16] == 8332,
    flag[9] ^ flag[13] * flag[8] & flag[16] == 113,
    flag[3] * flag[17] + flag[5] + flag[6] == 7090,
    flag[21] * flag[2] ^ flag[3] ^ flag[19] == 10521,
    flag[11] ^ flag[20] * flag[1] + flag[6] == 6787,
    flag[7] + flag[5] - flag[18] & flag[9] == 96,
    flag[12] * flag[8] - flag[10] + flag[4] == 8277,
    flag[16] ^ flag[17] * flag[13] + flag[14] == 4986,
    flag[0] * flag[15] + flag[3] == 7008,
    flag[13] + flag[18] * flag[2] & flag[5] ^ flag[10] == 118,
    flag[0] % flag[12] - flag[19] % flag[7] == 73,
    flag[14] + flag[21] * flag[16] - flag[8] == 11228,
    flag[3] + flag[17] * flag[9] ^ flag[11] == 11686,
    flag[15] ^ flag[4] * flag[20] & flag[1] == 95,
    flag[6] * flag[12] + flag[19] + flag[2] == 8490,
    flag[7] * flag[5] ^ flag[10] ^ flag[0] == 6869,
    flag[21] ^ flag[13] * flag[15] + flag[11] == 4936,
    flag[16] + flag[20] - flag[3] & flag[9] == 104,
    flag[18] * flag[1] - flag[4] + flag[14] == 5440,
    flag[8] ^ flag[6] * flag[17] + flag[12] == 7104,
    flag[11] * flag[2] + flag[15] == 6143
]

solver = Solver()
solver.add(conditions)

while solver.check() == sat:
    model = solver.model()
    result = [chr(model[flag[i]].as_long()) for i in range(22)]
    print("Flag:", ''.join(result))
    #solver.add(Or(flag[i] != model[flag[i]] for i in range(22)))

Flag INTIGRITI{tHr33_Z_FTW}