Details

Crystal Clear was a reversing CTF where we had to reverse a program compiled in Crystal, a completely unknown language to me.

Anyways we find two separate arrays of bytes in memory that are xor’d against our input, byte by byte the result of the xor is stored in some cpu register and if != 0 at the end of the check the “password” was no good

So, we throw those byte arrays into z3 and solve away:

Writeup

solve.py

#!/usr/bin/env python3

from pwn import *
import z3

x1 = [0xb7, 0xe2, 0x3f, 0xd2, 0x34, 0xec, 0x7b, 0xdf, 0x3e, 0x98, 0x32, 0x6f, 0xb4, 0xbf, 0xf2, 0xfd, 0x37, 0xb5, 0xbc, 0xe2, 0x21, 0xc5, 0xc3, 0xb3, 0xcb, 0xa8, 0x1e, 0x11, 0xb7, 0x32, 0x0f, 0x47]
x2 = [0xf1, 0xa4, 0x7c, 0x86, 0x72, 0x97, 0x38, 0xad, 0x67, 0xeb, 0x66, 0x5b, 0xd8, 0xd3, 0xc3, 0x87, 0x04, 0xd1, 0xe3, 0xba, 0x11, 0x97, 0x9c, 0x82, 0xa5, 0xf7, 0x4c, 0x22, 0xc1, 0x13, 0x2e, 0x3a]

s = z3.Solver()
min_v = 0x21
max_v = 0x7e

lst = [z3.BitVec(f"{i}", 8) for i in range(0x20)]
for v in lst:
    s.add(v >= min_v, v <= max_v)

i = 0
while i < 0x20:
    s.add(lst[i] ^ x1[i] ^ x2[i] == 0x0)
    i += 1

if s.check() == z3.sat:
    m = s.model()
    r = [m[v].as_long() for v in lst]
    f = ""
    for v in r:
        f += chr(v)

    print(f)

Details#

Writeup#

Details

Writeup