Tags: rev z3 rust
Rating:
# 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_
## 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.
```rust
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.
```python
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}`
