# 1337UP LIVE CTF 2023
## FlagChecker
> Can you beat this FlagChecker?>> Author: Jopraveen> > [`flagchecker`](https://raw.githubusercontent.com/D13David/ctf-writeups/main/1337uplive/rev/flag_checker/flagchecker), [`source.rs`](https://raw.githubusercontent.com/D13David/ctf-writeups/main/1337uplive/rev/flag_checker/source.rs)
Tags: _rev_
## SolutionWe 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.
```rustflag.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.
```pythonfrom z3 import *
# Create a BitVec array for the flagflag = [BitVec('flag_%d' % i, 8) for i in range(22)]
# Define the conditionsconditions = [    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}`